# Différences

Cette page vous donne les différences entre la révision choisie et la version actuelle de la page.

smtsolvers [Le 17/03/2019 à 23:26] jaxom depl astuces |
— (Version actuelle) | ||
---|---|---|---|

Ligne 1: | Ligne 1: | ||

- | ===== SMT Solvers ===== | ||

- | \\ | ||

- | ==== haRVey ==== | ||

- | \\ | ||

- | haRVey is a SMT (Satisfiability Modulo Theories) prover. There are presently two branches of haRVey: haRVey-SAT and haRVey-FOL.\\ | ||

- | |||

- | * haRVey-FOL integrates a First-Order Logic theorem prover (hence its name), i.e. the E-prover. It uses the superposition calculus as implemented by the E-prover, to determine the satisfiability of Boolean combinations of atoms with functions interpreted in a first-order theory with equality.\\ | ||

- | |||

- | * haRVey-SAT is based on congruence closure, the Nelson-Oppen framework, and rudimentary instantiation techniques to decide the satisfiability of a set of atoms written with uninterpreted symbols, linear arithmetics, some lambda-expressions, and some quantifiers. The Boolean engine is a SAT solver (zChaff or %%MiniSAT%%), hence its name.\\ | ||

- | |||

- | * License:\\ | ||

- | * haRVey-FOL: GNU LGPL 2.1\\ | ||

- | * haRVey-FOL relies on E-prover (http://eprover.org/): GNU GPL\\ | ||

- | * haRVey-SAT: BSD like\\ | ||

- | * haRVey-SAT relies on %%MiniSat%%(http://minisat.se/): BSD like\\ | ||

- | * Web site: http://harvey.loria.fr/haRVey.php\\ | ||

- | |||

- | |||

- | \\ | ||

- | ==== CVC3 ==== | ||

- | \\ | ||

- | 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.\\ | ||

- | |||

- | CVC3 is the last offspring of a series of popular SMT provers, which originated at Stanford University with the SVC system. In particular, it builds on the code base of CVC Lite, its most recent predecessor. Its high level design follows that of the Sammy prover.\\ | ||

- | |||

- | CVC3 works with a version of first-order logic with polymorphic types and has a wide variety of features including:\\ | ||

- | |||

- | * several built-in base theories: rational and integer linear arithmetic, arrays, tuples, records, inductive data types, bit vectors, and equality over uninterpreted function symbols;\\ | ||

- | * support for quantifiers;\\ | ||

- | * an interactive text-based interface;\\ | ||

- | * a rich C and C++ API for embedding in other systems;\\ | ||

- | * proof and model generation abilities;\\ | ||

- | * predicate subtyping;\\ | ||

- | * essentially no limit on its use for research or commercial purposes (see license).\\ | ||

- | |||

- | \\ | ||

- | * License: BSD like\\ | ||

- | * Web site: http://www.cs.nyu.edu/acsys/cvc3/\\ | ||

- | |||

- | ==== CVC4 ==== | ||

- | |||

- | CVC4 is an efficient open-source 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 the fourth in the Cooperating Validity Checker family of tools (CVC, CVC Lite, CVC3) but does not directly incorporate code from any previous version. A joint project of NYU and U Iowa, CVC4 aims to support the features of CVC3 and SMT-LIBv2 while optimizing the design of the core system architecture and decision procedures to take advantage of recent engineering and algorithmic advances. | ||

- | |||

- | CVC4 is intended to be an open and extensible SMT engine, and it can be used as a stand-alone tool or as a library, with essentially no limit on its use for research or commercial purposes (see license). Contributors to CVC4 are required to sign a Contributor License Agreement (CLA), which can be found here. | ||

- | |||

- | CVC4 works with a version of first-order logic with polymorphic types and has a wide variety of features including: | ||

- | |||

- | * several built-in base theories: rational and integer linear arithmetic, arrays, tuples, records, inductive data types, bit-vectors, strings, and equality over uninterpreted function symbols; | ||

- | * support for quantifiers; | ||

- | * an interactive text-based interface; | ||

- | * a rich C++ API for embedding in other systems; | ||

- | * model generation abilities. | ||

- | |||

- | * License: BSD like | ||

- | * Web site: http://cvc4.cs.stanford.edu/web/ | ||

- | |||

- | |||

- | ==== SAL ==== | ||

- | \\ | ||

- | The heart of SAL is a language, developed in collaboration with Stanford and Berkeley, for specifying concurrent systems in a compositional way. It is supported by a tool suite that includes state of the art symbolic (BDD-based) and bounded (SAT-based) model checkers, an experimental "Witness" model checker, and a unique "infinite" bounded model checker based on SMT solving. Auxiliary tools include a simulator, deadlock checker and an automated test generator.\\ | ||

- | |||

- | * License: GNU GPL\\ | ||

- | * Web site: http://sal.csl.sri.com/\\ | ||

- | |||

- | \\ | ||

- | ==== Alt Ergo ==== | ||

- | \\ | ||

- | Alt-Ergo is an automatic theorem prover dedicated to program verification. Alt-Ergo is based on CC(X) a congruence closure algorithm parameterized by an equational theory X. Currently, CC(X) can be instantiated by the empty equational theory and by the linear arithmetics. Alt-Ergo contains also a home made SAT-solver and an instantiation mechanism.\\ | ||

- | |||

- | * License: GNU GPL\\ | ||

- | * Web site: http://alt-ergo.lri.fr/\\ | ||

- | |||

- | ==== Gappa ==== | ||

- | \\ | ||

- | Gappa (//Génération Automatique de Preuves de Propriétés Arithmétiques//) is a tool intended to help verifying and formally proving properties on numerical programs dealing with floating-point or fixed-point arithmetic. It has been used to write robust floating-point filters for CGAL and it is used to certify elementary functions in CRlibm. While Gappa is intended to be used directly, it can also act as a backend prover for the Why software verification plateform or as an automatic tactic for the Coq proof assistant.\\ | ||

- | |||

- | * License: GNU LGPL and CeCILL | ||

- | * Web site: http://gappa.gforge.inria.fr/ | ||

- | |||

- | |||

- | ==== STP ==== | ||

- | |||

- | STP is a constraint solver (also referred to as a decision procedure or automated prover) aimed at solving constraints generated by program analysis tools, theorem provers, automated bug finders, intelligent fuzzers and model checkers. STP has been used in many research projects at Stanford, Berkeley, MIT, CMU and other universities. It is also being used at many companies such as NVIDIA, some startup companies, and by certain government agencies. | ||

- | |||

- | The input to STP are formulas over the theory of bit-vectors and arrays (This theory captures most expressions from languages like C/C++/Java and Verilog), and the output of STP is a single bit of information that indicates whether the formula is satisfiable or not. If the input is satisfiable, then it also generates a variable assignment to satisfy the input formula. | ||

- | |||

- | * License: BSD like | ||

- | * Web site: http://people.csail.mit.edu/vganesh/STP_files/stp.html | ||

- | |||

- | ==== Z3 ==== | ||

- | |||

- | Z3 is a theorem prover from Microsoft Research. | ||

- | |||

- | * License: BSD like | ||

- | * Web site: https://github.com/Z3Prover/z3 | ||

- | |||