AVIACC

Analysis and Verification of Critical Concurrent Programs

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.

r5 - 20 May 2015 - 09:17:14 - JorgeSousaPinto
This site is powered by the TWiki collaboration platform Copyright by the contributing authors. Ideas, requests, problems? Send feedback.
Syndicate this site RSSATOM