Tools on Rewriting
-
μ-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.
relations which can be associated to them: ... * operational termination of conditional rewriting. ... remarkable that in the last termination competition (2021), MU-TERM ... Union Europea [2011-W...
-
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.
ACL2 Version 8.3 ... paper note icon Differences from Version 8.2 tiny warning icon filing ... April 14, 2020 ... * ACL2+Books Manual (Version 8.3) ... * ACL2 User's Manual (Version 8.3)...
-
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.
the whole system. ACP is participating Confluence Competition (CoCo). ... Support of certificates generation For few criteria, ACP can generate certificates in CPF format, w...
-
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.
-
CARPA (Counter examples in Abstract Rewriting Produced Automatically) is a tool that automatically generates examples of finite abstract rewrite systems satisfying a given list of properties.
* The paper Automatically finding particular term rewriting systems presenting the tool Carpa+ and the underlying theory. ... Last change: July 12, 2018...
-
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, 2011, 2012, and 2013 in the international termination competition....
-
CeTA is a tool that certifies termination analysis (in terms of a termination proof) provided by a termination tool.
The current version is 3.0.1. To access previous versions of CeTA and see the differences please visit this site....
-
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).
-
CITP is a tool for proving inductive properties of software systems specified with constructor- based logics. CITP is equipped with a default proof strategy for the automated verification of Observational Transitional Systems (OTS), but the area of applications is not restricted to OTS. The proof strategy can be customised by the user, or the basic tactics can be applied step-by-step. The Kernel of CITP is implemented in Core Maude. The interface of CITP is implemented in Full Maude.
-
A Coq library on rewriting and termination with tactics for automatically checking the conditions of termination theorems.
CoLoR: a Coq Library on Rewriting and termination __________________________________________________________________ ... CoLoR is a library of formal mathematical definitions and proofs of theor...
-
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.
* Coq 8.4pl5 is out 10-25-14...
-
The CRSX project aims at implementing a generic higher-order rewrite engine based on the Combinatory Reduction Systems (CRS) formalism.
CRSX--Combinatory Reduction Systems with Extensions. ... CRSX implements higher-order rewriting based on Combinatory Reduction Systems (CRS) with some extensions. ... Copyright (c) 2006, 2013 IBM Co...
-
CSI is an automatic confluence prover for first-order rewrite systems. It is based on the Tyrolean Termination Tool 2 (TTT2).
* July 2021: Version 1.2.5 released. (CoCo 2021 version; adds outside-closure criterion) ... You can also download the source. The current version is 1.2.5. To...
-
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.
-
CVC4 is a tool for determining the satisfiability of a first order formula modulo a first order theory (or a combination of such theories). It is the fourth in the Cooperating Validity Checker family of tools (CVC, CVC Lite, CVC3) but does not directly incorporate code from any previous version. CVC4 is intended to be an open and extensible SMT engine. It can be used as a stand-alone tool or as a library. It has been designed to increase the performance and reduce the memory overhead of its predecessors. CVC4 is still a research prototype and is not yet ready for public release. Users looking for an industrial-strength SMT solver are encouraged to use CVC3 instead (for now).
* Google...
-
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.
-
Frama-C is a tool consisting of several static analysis techniques for the programming language C.
15 July 2020 Frama-Clang 0.0.9 is out. Download it here ....
-
GHC is a state-of-the-art, open source, compiler and interactive environment for the functional language Haskell. Highlights: * GHC supports the entire Haskell 2010 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. * GHC works on several platforms including Windows, Mac, Linux, most varieties of Unix, and several different processor architectures. There are detailed instructions for porting GHC to a new platform. * GHC has extensive optimisation capabilities, including inter-module optimisation. * GHC compiles Haskell code either directly to native code or using LLVM as a back-end. GHC can also generate C code as an intermediate target for porting to new platforms. The interactive environment compiles Haskell to bytecode, and supports execution of mixed bytecode/compiled programs. * Profiling is supported, both by time/allocation and various kinds of heap profiling. * GHC comes with several libraries, and thousands more are available on Hackage.
11 July 2014 GHC 7.8.3 Released! [download]...
-
A SAT solver that predicts learnt-clause usefulness.
News: glucose 2.1 won the SAT Challenge 2012, Application Benchmarks. ... glucose v2.1 code released Jul, 2012 ... glucose v2.1 won the "best single engine solver in the application track&quo...
-
A termination tool for C programs.
-
mascott is a fully automatic AC-completion tool.
-
A termination tool.
-
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.
* Maxcomp v1.1 (March 9, 2015; support for ocamlyices 0.7.1) ... * Maxcomp v1.0...
-
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.
The most recent version of OCaml is 4.07.0. It was released on 2018-07-10. ... Some of the highlights in release 4.07 are: * The way the standard library modules are organized internally has ...
-
A SAT solver.
-
A SAT solver.
team contact software publications teaching jobs ... GI-Dissertation Award 2020 ... FMCAD'20 Student Forum Best Student Contribution ... SAT'20 Best Presentation Award ... GCAI'19 Post and I...
-
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....
-
REDUCE is an interactive system for general algebraic computations of interest to mathematicians, scientists and engineers.
Page last modified on Tuesday 2nd January 2024. ... C. Hearn and the REDUCE developers 2009-2024. All Rights Reserved. ... Microsoft Internet Explorer does not display this web site correctly; pleas...
-
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.
TcT version 3.3 released 2019/05/10 __________________________________________________________________ ... Compatibility release for recent ghc version (ghc-8.6.5)....
-
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.
The current version is Yices 2.6.1. It was released on 2018-10-26....