Difference between revisions of "Software"

From vecolib
Jump to: navigation, search
(Created page with "* [http://www.fit.vutbr.cz/research/groups/verifit/tools/slide/ SLIDE]: solver for Separation Logic with Inductive Definitions * [http://www.liafa.univ-paris-diderot.fr/spen/...")
 
 
(7 intermediate revisions by 2 users not shown)
Line 1: Line 1:
* [http://www.fit.vutbr.cz/research/groups/verifit/tools/slide/ SLIDE]: solver for Separation Logic with Inductive Definitions
+
* [https://github.com/cathiec/AltImpact AltImpact] tool for checking emptiness of Alternating Data Automata
* [http://www.liafa.univ-paris-diderot.fr/spen/ SPEN]: solver for Separation Logic Entailments
+
* [https://github.com/cristina-serban/inductor Inductor] cyclic prover for systems of inductive definitions
 +
* [https://github.com/timothy-king/CVC4SepLogic CVC4SepLog] SMT solver for quantifier-free ground Separation Logic over unrestricted data theories
 +
* [http://www.fit.vutbr.cz/research/groups/verifit/tools/includer/ all_included] a tool for checking trace inclusion between infinite state systems
 +
* [http://www.fit.vutbr.cz/research/groups/verifit/tools/slide/ SLIDE]: a solver for Separation Logic with Inductive Definitions
 +
* [http://www.liafa.univ-paris-diderot.fr/spen/ SPEN]: a solver for Separation Logic Entailments
 +
* [http://www.liafa.univ-paris-diderot.fr/celia/ CELIA]: a tool-set for static analysis and verification of programs with dynamic memory
 +
* [http://frama-c.com/ Frama-C]: a platform dedicated to source-code analysis of C software

Latest revision as of 12:22, 6 September 2017

  • AltImpact tool for checking emptiness of Alternating Data Automata
  • Inductor cyclic prover for systems of inductive definitions
  • CVC4SepLog SMT solver for quantifier-free ground Separation Logic over unrestricted data theories
  • all_included a tool for checking trace inclusion between infinite state systems
  • SLIDE: a solver for Separation Logic with Inductive Definitions
  • SPEN: a solver for Separation Logic Entailments
  • CELIA: a tool-set for static analysis and verification of programs with dynamic memory
  • Frama-C: a platform dedicated to source-code analysis of C software