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