Software Tools
I have contributed to the design and/or development of the
following 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.