Difference between revisions of "Software"
From vecolib
Sighireanu (Talk | contribs) |
|||
| Line 1: | Line 1: | ||
| + | * [http://www.fit.vutbr.cz/research/groups/verifit/tools/trace_inclusion/ TRACER] 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 | ||
* [http://www.liafa.univ-paris-diderot.fr/spen/ SPEN]: a solver for Separation Logic Entailments | * [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://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 | * [http://frama-c.com/ Frama-C]: a platform dedicated to source-code analysis of C software | ||
Revision as of 18:00, 19 February 2015
- TRACER 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
