Difference between revisions of "Software"
From vecolib
| (One intermediate revision by the same user not shown) | |||
| Line 1: | Line 1: | ||
| − | * [ https://github.com/timothy-king/CVC4SepLogic CVC4SepLog] SMT solver for quantifier-free ground Separation Logic over unrestricted data theories | + | * [https://github.com/cathiec/AltImpact AltImpact] tool for checking emptiness of Alternating Data Automata |
| + | * [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/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.fit.vutbr.cz/research/groups/verifit/tools/slide/ SLIDE]: a solver for Separation Logic with Inductive Definitions | ||
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
