Uncategorized

OpenSMT

Roberto — Tue, 16 Sep 2008 16:02:46 +0200

As a part of research on decision procedures, our Lab develops a tool, OpenSMT, that is used as a framework to perform all our experiments.

OpenSMT is a compact and open-source SMT-solver written in C++, with the main goal of making SMT-Solvers easy to understand and use as a computational engine of formal verification. OpenSMT is built on top of MiniSAT (http://minisat.se).

Loopfrog

mcWebAdmin — Mon, 03 Dec 2007 17:44:03 +0100

As a part of the "Detection of Security Flaws and Vulnerabilities by Guided Model Checking" project we implemented the tool called Loopfrog - an Abstract Interpretation based static analyzer for C programs.

eVolCheck

mcWebAdmin — Tue, 05 Jun 2012 22:00:22 +0200

eVolCheck is a bounded upgrade checker of C, built on the top of FunFrog. It uses interpolation-based function summaries, extracted from original version of a program, for incremental verification of an upgraded version of the program.

In each incremental check, eVolCheck first identifies the modified function on the syntactical level and then attempts to show that the old function summaries are still valid over-approximations of the behaviour of the modified functions. These are local and thus cheap checks.

SAFARI

Francesco — Wed, 18 Jan 2012 14:47:55 +0100

SAFARI - SMT-based Abstraction For Arrays with Interpolants - is a model checker designed to prove safety (possibly universally quantified) properties of imperative programs with arrays. SAFARI is based on an extension of the Lazy Abstraction paradigm capable of handling existentially quantified formulae by using a combination of quantifier-free interpolation algorithms for the indexes and elements in the arrays during refinement.

FunFrog

Ondrej — Tue, 16 Aug 2011 15:08:43 +0200

FunFrog is a bounded model checker of C using interpolation-based function summaries. FunFrog uses Craig interpolation to extract function summaries and reuses them in subsequent verification runs as a means of over-approximation of the precise functions' behavior.

To deal with spurious errors, which are possible due to the over-approximation, FunFrog employs a counter-example guided refinement strategy to identify too coarse summaries responsible for the error trace and replaces those with precise behavior representation in the next iteration.

Synergy

mcWebAdmin — Sat, 25 Oct 2008 22:38:13 +0200

The techniques developed for "The Synergy of Precise and Fast Abstractions for Program Veriﬁcation" project are implemented on top of SATABS model-checker for ANSI-C programs. The tool allows to compare effectiveness of abstraction techniques in CEGAR-based verification. Details of the techniques can be found in [1].

Tool binary (1,6MB) compiled for Linux/i386.

References

The Synergy of Precise and Fast Abstractions for Program Veriﬁcation, Sharygina, N.; Tonetta, S.; Tsitovich, A. , 24th Annual ACM Symposium on Applied Computing (SAC), Honolulu, USA, p.566-573, ACM (2009)

Boppo

Aliaksei — Wed, 13 Feb 2008 12:23:03 +0100

Boppo is a model checker for Boolean programs. Features:

Partial Order Reduction
Fixpoint detection using QBF
Support for the constrain construct

It is a joint product of Byron Cook, Daniel Kroening, and Natasha Sharygina.
Download Boppo

SATABS

Aliaksei — Wed, 13 Feb 2008 11:47:35 +0100

SATABS is a verification tool for ANSI-C and C++ programs. It allows verifying array bounds (buffer overflows), pointer safety, exceptions and user-specified assertions. Furthermore, it can check ANSI-C and C++ for consistency with other languages, such as Verilog. SATABS computes an abstraction of the program in order to handle large amounts of code. SATABS home page