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.