Software

• 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