Software Tools

• RDL (Rewrite and Decision Procedures Laboratory). RDL is a fully automatic tool for formula simplification in a quantifier-free first-order theories. RDL is based on the Constraint Contextual Rewriting paradigm and features a tight integration of rewriting and decision procedures. An overview of RDL can be found here.
• TSAT++ is an open platform for satisfiability modulo theories (SMT) based on a tight coupling of satisfiability procedures and a SAT-solver. The current version of TSAT++ supports Separation Logic (also known as Difference Logic). An overview of TSAT++ can be found here.
• The AVISS Tool is a fully automatic security protocol analyser. It is capable to analyse a large portion of the protocols collected in the Clark & Jacob library of security protocols. An overview of the AVISS Tool can be found here. The AVISS Tool is the predecessor of the AVISPA Tool.
• The AVISPA Tool is a fully automatic analyser for large-scale Internet security-sensitive protocols. It comprises 4 back-ends implementing a variety of security protocol verification techniques. An overview of the AVISPA Tool can be found here.
• SATMC (SAT-based Model Checker) is a bounded model checker for security protocols. SATMC reduces the problem of checking whether a protocol is vulnerable to attacks of bounded length to the satisfiability of a propositional formula which is solved by a state-of-the-art SAT solver taken off-the-shelf. SATMC is one of the back-ends of the AVISPA Tool. An overview of SATMC can be found here.
• Eureka is a model checker for sequential software based on the counterexample-guided abstraction refinement (CEGAR) paradigm. Unlike many other software model checkers based on the CEGAR paradigm Eureka analyses arrays precisely. An overview of Eureka can be found here.
• SMT-CBMC is a bounded model checker for sequential software. SMT-CBMC reduces the problem of checking whether an input program has an execution path of bounded length violating an assertion to the satisfiability of a formula with respect to a decidable theory. The resulting formula is fed and solved by a state-of-the-art SMT-solver taken off-the-shelf. An overview of SMT-CBMC can be found here.