Tools on Rewriting
-
The Tyrolean Complexity Tool (TCT) is a tool for automatically proving (low) upper bounds on the derivational complexity and runtime complexity of terminating term rewriting systems. Whereas Version 1.0 is strongly based on the automatic termination prover TTT2, Version 2.0 is rewritten from scratch in the purely functional programming language Haskell.
-
The Tyrolean Termination Tool 2 (TTT2) is a tool for automatically proving (and disproving) termination of rewrite systems. It is the completely redesigned successor of TTT. Current (non-)termination techniques include approximated dependency graph, argument filtering, bounds, dependency pair method, Knuth-Bendix order, lexicographic path order, loop detection, matrix interpretation, polynomial interpretation, predictive labeling, recursive SCC, root labeling, semantic labeling, simple projection and subterm criterion, uncurrying, usable rules.
The current version is 1.08. Get recent versions. ... * May 25 2012: Version 1.08 released (PicoSat binding added)...
-
MiniSmt is a simple SMT solver for non-linear arithmetic based on MiniSat and Yices. It accepts the SMT-LIB format as input, is efficient on small domains, supports reasoning about non-rational real numbers, and is able to output models.
The current stable version is 0.4. Get recent versions and view the ... May 25, 2012: version 0.4 released (compile w/ and w/o yices)...
-
SPIKE is an automated theorem prover based on 'Descente Infinie' induction.
used to certify the validation proof of a conformance algorithm for the ABR protocol....
-
Saigawa is an automatic confluence tool for first-order term rewrite systems. It supports the next confluence criteria: Knuth and Bendix' criterion, decreasing confluence, and rule-labeling
Saigawa 1.4 released. This version participates in the 1st Confluence Competition (CoCo 2012) ... The tool requires termination tools and a QF-NIA SMT solver. In the default setting it uses: *...
-
CeTA is a tool that certifies termination analysis (in terms of a termination proof) provided by a termination tool.
+ Confluence and non-confluence: ... o Weak orthogonality o Non-joinable forks using tcap ... The current version is 2.5. To access previous versions of CeTA and see...
-
ACP is an automated confluence prover for term rewriting systems (TRSs). A distinct feature of ACP is incorporation of several divide-and-conquer criteria such as those for commutative (Toyama,1988), layer-preserving (Ohlebusch,1994) and persistent (Aoto and Toyama, 1997) combinations. For a TRS to which direct confluence criteria do not apply, the prover decomposes it into components and tries to apply direct confluence criteria to each component. Then the prover combines these results to infer the (non-)confluence of the whole system.
Version Heap image OS (Arch) Version of SML/NJ 0.31 acp.x86-linux Linux (i386) 110.74 0.30 acp.x86-darwin Mac OS X (intel) 110.74...
-
CSI is an automatic confluence prover for first-order rewrite systems. It is based on the Tyrolean Termination Tool 2 (TTT2).
* May 2012: Version 0.2 released. ... You can also download the source. The current version is 0.2. To ... * type ./csi.sh <file>...
-
Isabelle is a generic proof assistant. It allows mathematical formulas to be expressed in a formal language and provides tools for proving those formulas in a logical calculus. The main application is the formalization of mathematical proofs and in particular formal verification, which includes proving the correctness of computer hardware or software and proving properties of computer languages and protocols.
* Installation ... * Download for 32-bit Linux * Download for 64-bit Linux * Download for Mac OS X * Download for Windows ... Some highlights: * Improved Isabelle/jEdit Prover IDE (PID...
-
Agda is a dependently typed functional programming language. It has inductive families, i.e., data types which depend on values, such as the type of vectors of a given length. It also has parametrised modules, mixfix operators, Unicode characters, and an interactive Emacs interface which can assist the programmer in writing the program. Agda is a proof assistant. It is an interactive system for writing and checking proofs. Agda is based on intuitionistic type theory.
* (2012/05/19) AIM XVI will be held in Copenhagen 3-9 October 2012. Mark your calendar! ... Page last modified on May 19, 2012, at 10:59 AM...
-
A Coq library on rewriting and termination with tactics for automatically checking the conditions of termination theorems.
statcounter Valid XHTML 1.1 Last updated on 18 May 2012. Come back to...
-
SML# is a new programming language in the Standard ML family being developed at RIEC (Research Institute of Electrical Communication), Tohoku University jointly with Sanpu Koubou Inc. Its design goal is to provide a moderate but practically important extensions (see features of SML#) while maintaining the compatibility of the Definition of Standard ML.
* Version 1.0.2 has been released. ... Last modified:2012/05/14 18:58:41 ... + SML# 1.0.2 has been released (May 14th, 2012)....
-
Z3 is a high-performance theorem prover being developed at Microsoft Research. Z3 supports linear real and integer arithmetic, fixed-size bit-vectors, extensional arrays, uninterpreted functions, and quantifiers. Z3 is integrated with a number of program analysis, testing, and verification tools from Microsoft Research. These include: Spec#/Boogie, Pex, Yogi, Vigilante, SLAM, F7, SAGE, VS3, FORMULA, and HAVOC. It can read problems in SMT-LIB and Simplify formats.
Last modified Fri May 11 15:37:50 2012...
-
The HOL System is an environment for interactive theorem proving in a higher-order logic. Its most outstanding feature is its high degree of programmability through the meta-language ML. The system has a wide variety of uses from formalizing pure mathematics to verification of industrial hardware.
Last modified on Wed May 9 23:10:47 BST 2012 by ns441 | Privacy policy...
-
Yices is an efficient SMT solver that decides the satisfiability of arbitrary formulas containing uninterpreted function symbols with equality, linear real and integer arithmetic, scalar types, recursive datatypes, tuples, records, extensional arrays, fixed-size bit-vectors, quantifiers, and lambda expressions. Yices also does MaxSMT (and, dually, unsat cores) and is competitive as an ordinary SAT and MaxSAT solver.
You can download Yices 1, our full-featured SMT solver, or our new Yices 2 solver. ... * Download Yices 2 (Updated April 26, 2012) ... Last modified: Thu 26 Apr 2012 14:52 PDT...
-
CafeOBJ is a new generation algebraic specification and programming language. As a direct successor of OBJ, it inherits all its features (flexible mix-fix syntax, powerful typing system with sub-types, and sophisticated module composition system featuring various kinds of imports, parameterised modules, views for instantiating the parameters, module expressions, etc.) but it also implements new paradigms such as rewriting logic and hidden algebra, as well as their combination.
-
GURU is a pure functional programming language, which is similar in some ways to Caml and Haskell. But GURU also contains a language for writing formal proofs demonstrating the properties of programs. So there are really two languages: the language of programs, and the language of proofs. When the compiler checks a program, it computes a type for it, just as compilers for other languages like JAVA do. But in GURU, such types can be significantly richer than in mainstream or even most research programming languages. These types are called dependent types, and they can express non-trivial semantic properties of data and functions. Analogously, when the compiler checks a proof, it computes a formula for it, namely the formula the proof proves. So we really have four kinds of expressions in GURU: programs (which we also call terms) and their types; proofs and their formulas.
Terms - Privacy - Project Hosting Help...
-
Anagopos is an open source tool for visualizing reduction graphs of terms in lambda calculus and term rewriting. Anagopos allows step-by-step generation of reduction graphs under six different drawing algorithms.
Terms - Privacy - Project Hosting Help...
-
QEPCAD is an implementation of quantifier elimination by partial cylindrical algebraic decomposition due originally to Hoon Hong, and subsequently added on to by many others. It is an interactive command-line program written in C, and based on the SACLIB library of computer algebra functions. Presented here is QEPCAD B version 1, the B designating a substantial departure from the original QEPCAD and distinguishing it from any development of the original that may proceed in a different direction.
The current version of QEPCADB is Version B 1.69, 16 March 2012....
-
An automatic termination of narrowing prover.
#Narradar » Feed Narradar » Comments Feed Narradar » Home Comments Feed Contact Documentation ... * Home * Web interface * References * Documentation * Download * Contact ... ___...
-
REPIUS (REwrite-Program Inversion and Unraveling System) is a tool that (fully or partially) inverts a constructor TRS written in a .trs file and unravels the resulting inverse CTRS. The prototype (Ver. 0.x) was developed following the approach in (Nishida et al., RTA'05) and employs a variant of Ohlebusch's unraveling transformation. The current version was wholly implemented, introducing a new approach to tail-recursive functions into the previous approach to full inversion (Nishida et al., IEICE'05). The unraveling step will be implemented as an option of postprocess of inversion, and the partial inversion approach will be also implemented as an extension. The current implementation is based on the technique in (Nishida and Vidal, RTA'11).
Updated: Mar 09, 2012 ... March 9, 2012 MSV is beeing developed now and the correctness is not guaranteed! __________________________________________________________________...
-
Q is an interpreted, dynamically typed functional programming language based on term rewriting which allows you to define functions using symbolic equations. It works on Linux, OS X, Unix and Windows, and comes with a bunch of useful libraries which turn it into a practical programming tool. The Q programming system is free software distributed under the GPL.
Please note that Q has been superseded by the Pure programming language, so please head over to the new website and download the latest version of the Q successor today! ... This website remains o...
-
ACL2 is a very large, multipurpose system. You can use it as a programming language, a specification language, a modeling language, a formal mathematical logic, or a semi-automatic theorem prover, just to name its most common uses.
Bob Boyer, Warren A. Hunt, Jr., Jared Davis, and Sol Swords...
-
Vampire is a theorem prover, that is, a system able to prove theorems. More precisely, it proves theorems in first-order logic.
Vinter...
-
Frama-C is a tool consisting of several static analysis techniques for the programming language C.
16 Feb. 2012 Commercial support and license available . 27 Jan. 2012 Training courses on Frama-C are proposed by Atos Formation (in French). 5 Jan. 2012 Release of Plug-in WP 0.5 for Nitrogen-20...
-
Stratego/XT is a language and toolset for program transformation. The Stratego language provides rewrite rules for expressing basic transformations, programmable rewriting strategies for controlling the application of rules, concrete syntax for expressing the patterns of rules in the syntax of the object language, and dynamic rewrite rules for expressing context-sensitive transformations, thus supporting the development of transformation components at a high level of abstraction.
Today we're releasing a minor maintenance release of Spoofax, version 1.0.2. This release fixes a memory leak that was introduced in the 1.0 release. There are no new features in this release, tho...
-
μ-Term is a tool which can be used to verify a number of termination properties of Term Rewriting Systems via different reduction relations which can be associated to them: termination of rewriting, termination of innermost rewriting, termination of context-sensitive rewriting, and termination of innermost context-sensitive rewriting.
rewriting and the third most powerful tool for proving termination of ... FEDER MINECO MICINN GVA UPV DSIC "Una manera de hacer Europa"...
-
GHC is a state-of-the-art, open source, compiler and interactive environment for the functional language Haskell. Highlights: * GHC supports the entire Haskell 98 language plus a wide variety of extensions. * GHC has particularly good support for concurrency and parallelism, including support for Software Transactional Memory (STM). * GHC generates fast code, particularly for concurrent programs. Take a look at GHC's performance on The Computer Language Benchmarks Game, and some comments on Haskell by the current organiser of the shootout, Brent Fulgham.
2 February 2012 GHC 7.4.1 Released! [download]...
-
A termination tool for C programs.
Lecture Notes in Computer Science 7152, pages 261-277, 2012....
-
Soot is a Java optimization framework. It provides four intermediate representations for analyzing and transforming Java bytecode: 1. Baf: a streamlined representation of bytecode which is simple to manipulate. 2. Jimple: a typed 3-address intermediate representation suitable for optimization. 3. Shimple: an SSA variation of Jimple. 4. Grimp: an aggregated version of Jimple suitable for decompilation and code inspection. Soot can be used as a stand alone tool to optimize or inspect class files, as well as a framework to develop optimizations or transformations on Java bytecode.
International Workshop on the State Of the Art in Java Program Analysis ... Co-located with PLDI, June 2012 in Beijing, China. Submissions by March 28th, 2012. More information...
-
Timbuk is a collection of tools for achieving proofs of reachability over Term Rewriting Systems and for manipulating Tree Automata (bottom-up non-deterministic finite tree automata). Timbuk and reachability analysis can be used for program verification.
library is necessary before compiling TimbukCEGAR.The archive also contains several simple test examples as well as a Term Rewriting System produced from a Java program using Copster....
-
A SAT solver.
-
Coq is a formal proof management system. It provides a formal language to write mathematical definitions, executable algorithms and theorems together with an environment for semi-interactive development of machine-checked proofs.
* Beta-release of Coq 8.4 12-27-11 * Coq 8.3pl3 is out 12-27-11...
-
Tom is a language extension designed to manipulate tree structures and XML documents. It provides pattern matching facilities to inspect objects and retrieve values, and can be used with C, Java, Python, C++, C#, etc.
* This page has been accessed 78,644 times....
-
Sugar is a SAT-based constraint solver based on a SAT-encoding method, named order encoding.
-
Why is a software verification platform.
The Why platform is not any longer under active development. Our effort has moved to the development of Why3. ... Why is still maintained, in particular to provide the Jessie plug-i...
-
Objective Caml is the most popular variant of the Caml language. From a language standpoint, it extends the core Caml language with a fully-fledged object-oriented layer, as well as a powerful module system, all connected by a sound, polymorphic type system featuring type inference. The Objective Caml system is an industrial-strength implementation of this language, featuring a high-performance native-code compiler (ocamlopt) for 9 processor architectures (IA32, PowerPC, AMD64, Alpha, Sparc, Mips, IA64, HPPA, StrongArm), as well as a bytecode compiler (ocamlc) and an interactive read-eval-print loop (ocaml) for quick development and portability.
-
FAST is an efficient decision procedure for deduction and static equivalence.
-
Autograph is a project carried out at the LaBRI (Laboratoire Bordelais de Recherche en Informatique) at the University of Bordeaux. Autograph is an experimental tool written in Common Lisp for verifying properties of graphs of bounded clique-width. It is written in Steele Bank Common Lisp (SBCL). It uses the Autowrite library which provides the operations needed to create and manipulate automata. The following famous theorem connects the problem of verifying graph properties with term automata: Monadic second-order model checking is for tree-width [Courcelle (1990)] and clique-width [Courcelle, Makowski, Rotics (2001)]. Tree-width and clique-width are graph complexity measures based on graph decompositions. A decomposition produces a term representation of the graph. For a graph property expressed in monadic second order logic (MSO), the algorithm verifying the property takes the form of a term automaton which recognizes the terms denoting graphs satisfying the property.
-
Autowrite is a project carried out at the LaBRI (Laboratoire Bordelais de Recherche en Informatique) at the University of Bordeaux. Autowrite is an experimental tool written in Common Lisp for checking properties of term rewrite systems and handling bottom-up term (tree) automata. It is written in Steele Bank Common Lisp (SBCL). It was initially designed to check call-by-need (CBN) properties of TRSs. For this purpose, it also implements the main operations on term automata constructions (determinization, minimization, union, intersection, emptiness, ...) and many operations on terms. Recently, fly-automata have been added to the implementation. The transition function of a fly-automaton is a (Lisp) transition function instead of a table of transitions. Fly-automata may be used when the transition table is too big to be stored and can also be infinite in two ways (infinite signature, infinite number of states). A graphical interface interface written using FreeCLIM, the free implementation of the CLIM specification frees the user from any Lisp knowledge. From this interface, one can handle term rewrite systems, term automata and build many term automata related to TRSs and graphs represented as terms; one can check membership to call-by-need classes for the different considered approximations of a given system.
-
A SAT solver that predicts learnt-clause usefulness.
[Glue-Clauses-rot-small.jpg] [Medailles-2011-header-small.jpg] ... A SAT Solver by G. Audemard and L. Simon The solver that looks for glue clauses. ____________________________________________...
-
This tool is a termination tool for higher-order rewrite systems, which implements dependency pairs, argument filterings and a variant of HORPO. It employs a SAT-solver to resolve dependencies.
external HORPO-tool (built on the previous version of WANDA; the code has been included as the file horpocode.zip for compilation purposes, but is a bit of a mess)....
-
The CRSX project aims at implementing a generic higher-order rewrite engine based on the Combinatory Reduction Systems (CRS) formalism.
Eclipse plug-in for CRSX ... Tutorial for eclipse plug-in for CRSX Development guide for eclipse plug-in for CRSX...
-
E is a a purely equational theorem prover for full first-order logic. That means it is a program that you can stuff a mathematical specification (in first-order format) and a hypothesis into, and which will then run forever, using up all of your machines resources. Very occasionally it will find a proof for the hypothesis and tell you so...
-
AProVE is a system for automated termination and innermost termination proofs of term rewrite systems (TRSs). Moreover, AProVE also handles several other formalisms, e.g., logic programs (Prolog), functional programs (Haskell 98), conditional TRSs, TRSs modulo AC, context-sensitive TRSs, etc. The power of AProVE is demonstrated in the annual International Competition of Termination Tools, where AProVE was the most powerful tool for termination of TRSs in 2004, 2005, 2006, 2007, and 2008.
in 2004, 2005, 2006, 2007, 2008, 2009, 2010 and 2011. ... variety of different termination proof techniques. AProVE offers a "fully automatic" mode where suitable termination techniques ar...
-
CaT is a powerful analyzer for the complexity of term rewrite systems. It is based on the fast and powerful termination analyzer TTT2. In 2008 and 2009, CaT won all categories in the international termination competition related to complexity in which it participated.
2010, and 2011 in the international termination competition....
-
A tool for first-order unification on terms represented by Singleton Tree Grammars.
-
CiME 3 is a rewriting toolbox that provides Coq certificates for termination proofs (standard rewriting) obtained using various criteria: Dependency pairs (plain/marks, graphs refinements with or without sub-term criterion), as well as various orderings (polynomial interpretations, matrix interpretations, full RPO with status, with AFS refinements).
+ Release CiME 3 binaries for i686 64 bits linux: [static](Bugfix 2011/05/26) [dynamic] (Bugfix 2011/04/01)...
-
mkbTT is a tool for performing Knuth-Bendix completion with automatic termination tools. It is based on two ingredients: (1) the inference system for completion with multiple reduction orderings introduced by Kurihara and Kondo (1999) and (2) the inference system for completion with external termination provers proposed by Wehrman, Stump and Westbrook (2006). The tool can be used with any termination tool that satisfies certain minimal requirements.
Home Download Usage Web Interface Experiments...
-
Maxcomp is an automatic completion tool for first-order equational systems. Given an equational system, the tool outputs a corresponding complete (i.e. confluent and terminating) term rewrite system.
* System Description (RTA 2011) (.pdf; typo fixed version)...
-
PVS is a verification system: that is, a specification language integrated with support tools and a theorem prover. It is intended to capture the state-of-the-art in mechanized formal methods and to be sufficiently rugged that it can be used for significant applications. PVS is a research prototype: it evolves and improves as we develop or apply new capabilities, and as the stress of real use exposes new requirements.
*NEW* PVS 5.0 is now available - see the download page for details. ... PVS 5.0 is the current version. It is open source (under the GPL ... (commercial), SBCL and CMU Lisp (open source) for Linux and...
-
MINLOG is an interactive proof system developed by Helmut Schwichtenberg and members of the logic group at the University of Munich. MINLOG is based on first order natural deduction calculus. It is intended to reason about computable functionals, using minimal rather than classical or intuitionistic logic. The main motivation behind MINLOG is to exploit the proofs-as-programs paradigm for program development and program verification. Proofs are in fact treated as first class objects which can be normalized. If a formula is existential then its proof can be used for reading off an instance of it, or changed appropriately for program development by proof transformation. To this end MINLOG is equipped with tools to extract functional programs directly from proof terms. This also applies to non-constructive proofs, using a refined A-translation. The system is supported by automatic proof search and normalization by evaluation as an efficient term rewriting device.
-
THOR is an automatic tool for proving Termination of Higher-Order Rewriting. It ranked first in the last International Termination Competition (termComp) in the Higher-Order category.
* THOR. Developed by Cristina Borralleras and Albert Rubio. THOR is an automatic tool for proving Termination of Higher-Order Rewriting. It ranked first in the last International Ter...
-
TERMPTATION (TERMination Proof Techniques automATION) is a fully automated system for proving termination (and innermost termination) of term rewrite systems (developed by C. Borralleras and A. Rubio).
* THOR. Developed by Cristina Borralleras and Albert Rubio. THOR is an automatic tool for proving Termination of Higher-Order Rewriting. It ranked first in the last International Ter...
-
Prover9 is an automated theorem prover for first-order and equational logic, and Mace4 searches for finite models and counterexamples. Prover9 is the successor of the Otter prover.
* Help! If you have questions about Prover9/Mace4/LADR, e-mail the author....
-
iProver is an instantiation-based theorem prover which is based on Inst-Gen calculus, complete for first-order logic. One of the distinctive features of iProver is a modular combination of instantiation and propositional reasoning. In particular, any state-of-the art SAT solver can be integrated into our framework. iProver incorporates state-of-the-art implementation techniques such as indexing, redundancy elimination, semantic selection and saturation algorithms. Redundancy elimination implemented in iProver include: dismatching constraints, blocking non-proper instantiations and propositional-based simplifications. In addition to instantiation, iProver implements ordered resolution calculus and a combination of instantiation and ordered resolution.
-
This tool proves non-termination of string rewriting, by searching for patterns in derivations and can handle non-looping non-termination.
Apache/2.2.16 (Debian) Server at dfa.imn.htwk-leipzig.de Port 80...
-
RAPT (Rewriting-based Automated Program Transformation system) is a program transformation system using transformation templates, which implements a framework of program transformation. RAPT transforms many-sorted TRSs according to input correct templates with verification of its correctness.
-
A SAT solver.
-
StreamBox: A Tool for Proving Stream Equality.
-
TrafO, Transformation of Outermost Termination, is a transformation tool for proving outermost termination.
-
An analyzer for Java programs.
-
MiniSat is a minimalistic, open-source SAT solver, developed to help researchers and developers alike to get started on SAT. Some key features of MiniSat: * Easy to modify. MiniSat is small and well-documented, and possibly also well-designed, making it an ideal starting point for adapting SAT based techniques to domain specific problems. * Highly efficient. Winning all the industrial categories of the SAT 2005 competition, MiniSat is a good starting point both for future research in SAT, and for applications using SAT. * Designed for integration. MiniSat supports incremental SAT and has mechanisms for adding non-clausal constraints. By virtue of being easy to modify, it is a good choice for integrating as a backend to another tool, such as a model checker or a more generic constraint solver.
* A paper on how to compute localization abstractions using the incremental interface of MiniSat. View this as an example of a non-trivial incremental SAT application. A key feature of the...
-
Non-termination analysis of Logic Programs using Types.
-
SPASS is an automated theorem prover for first-order logic with equality.
News: Friday, May 28: SPASS 3.5/3.7 mac binaries and windows binaries with new GUI available. ... page last modified Friday, 28 May 2010 - 15:19...
-
Jambox is an automated termination prover for string and term rewriting systems.
-
CVC3 is an automatic theorem prover for Satisfiability Modulo Theories (SMT) problems. It can be used to prove the validity (or, dually, the satisfiability) of first-order formulas in a large number of built-in logical theories and their combination.
-
Otter is an automated theorem prover for first-order and equational logic.
-
A termination tool.
-
Waldmeister is a theorem prover for unit equational logic. Its proof procedure is unfailing Knuth-Bendix completion. Waldmeister's main advantage is that efficiency has been reached in terms of time as well as of space. Within that scope, a complete proof object is constructed at run-time.
-
A termination tool for logic programming.
-
Vienna Modular Termination Laboratory (VMTL) is a tool for the (semi-)automatic termination analysis of rewriting systems. Currently, standard as well as context-sensitive and conditional term rewriting systems are supported. VMTL is an implementation of the dependency pair framework, in which termination of rewrite systems is analyzed by so called dependency pair processors. The search for termination proofs in VMTL is guided by a user configurable strategy featuring hierarchical grouping of processors, time-limits on the level of processor groups as well as single processors and parallelization. In addition VMTL provides open interfaces allowing to add new dependency pair processors as well as transformations/preprocessings of rewrite systems in a modular fashion.
-
OSHL-S is an automated theorem prover based on the OSHL algorithm. The current version of OSHL-S includes a few extensions to the original algorithm, such as types, relaxed ordering, caching, etc...
-
REDUCE is an interactive system for general algebraic computations of interest to mathematicians, scientists and engineers.
-
TNT, a transformation for analyzing narrowing termination, is a tool developed by German Vidal and Naoki Nishida to analyze the termination of narrowing.
-
TPA is a tool for proving termination and relative termination of term rewrite systems automatically. It is developed by Adam Koprowski at TU/e within TORPA project. TPA has some novel features compared with other termination provers. It uses the following termination proving techniques: polynomial and matrix interpretations, semantic and predictive labeling (both with booleans and with natural numbers), recursive path ordering (RPO), dependency pair transformation (DP), and dummy elimination.
-
Maude is a high-performance reflective language and system supporting both equational and rewriting logic specification and programming for a wide range of applications. Maude has been influenced in important ways by the OBJ3 language, which can be regarded as an equational logic sublanguage. Besides supporting equational specification and programming, Maude also supports rewriting logic computation.
-
PHP string analyzer is a static program analyzer that approximates the string output of a PHP program with a context-free grammar. The analyzer can be used to check properties of a PHP program. For example, it can be used to validate dynamically generated Web pages by a PHP program.
-
Slothrop is an automated equational theorem prover that performs a variant of Knuth-Bendix completion.
-
By this tool proofs of (relative) termination of string rewriting systems (SRS) can be generated automatically. It was developed by Hans Zantema starting in July 2003. It is based on a combination of polynomial and matrix interpretations, recursive path order, semantic labelling, dependency pairs, transformation order, dummy elimination and RFC-match-bounds. Proofs of non-termination are found by using ancestor graphs. In both the termination competition of 2004 and the termination competition of 2005 this tool performed the best of all tools in the category of string rewriting.
-
The aim of the system daTac is to do automated deduction in first-order logic with equality. Its speciality is to apply deductions modulo some equational properties of operators, such as commutativity or associativity-commutativity (AC). The deduction techniques implemented, based on resolution, paramodulation and term rewriting, have been proved refutationally complete.
-
HOPS is a graphically interactive program development and program transformation system based on term graphs.