Software Tools and Packages
HSMTlib
A Haskell library for easy interaction with multiple SMT solvers. Available through
Hackage.
SPARK parser
A parser library for SPARK code. Available from the
repository.
SPARK-BMC
A bounded model checker for SPARK programs. Available from the
repository.
SPARK-ABS
An experimental predicate abstraction workbench for SPARK code. Available from the
repository.
KATEXP
KAT decision procedures in Python. Available
here.
ARMY
A deductive verification platform for ARM programs using Why3. Available
here
WCET platform
WCET instantiation of a generic static analyzer in Haskell. Available
here.
RGCoq
Mechanization of Rely-Guarantee reasoning in the Coq proof-assistant. Available from this
link.