SMT-AI: an Abstract Interpreter for a Synchronous Extension of SMT-lib
SMT-AI is a tool that over-approximates reachable states of a system described in the SMT-lib format.
It intends to be used as a lemma generator during a k-induction proof.
SMT-AI: an Abstract Interpreter as Oracle for k-induction [DOI] P. Roux, R. Delmas and and P.-L. Garoche Accepted at TAPAS'10, ENTCS Volume 267, Issue 2, October 2010, Pages 55-68
PACSA: Primitive Actor Calculus, a Static Analyzer
The PACSA analyzer takes a term of CAP describing a concurrent system and computes an overapproximation of all reachable states using the abstract interpretation framework of Feret. It relies on several abstract domains to represent properties verified in all states. Some of them are specific to CAP and allow to check the linearity of the term or the absence of orphans.
You can try the current in development prototype in its web interface
Related publications
Abstract Interpretation of Mobile Systems [DOI] J. Feret
JLAP, volume 63(1), special issue on pi-calculus, 2005, Elsevier
Static Analysis of Actors: Type systems vs. Abstract Interpretation [ps.gz] P.-L. Garoche, M. Pantel, and X. Thiroux
Accepted at EAAI'06, no proceedings edited, March 26, 2006 - Vienna, Austria
YASA, yet another simple analyzer
The Yasa prototype was initially written in order to supply a toy analyzer for practical experiments in a master-level course on abstract interpretation.
It takes a C file, builds the control flow graph. Then computes a least fixpoint then a greatest fixpoint of the programs collecting semantics relying on numerical abstract domains. In this version, it only deals with numerical values and doesn't handle function calls and all kind of C constructions (pointers, struct, char values, etc).
It is written in Ocaml and relies on the CIL library to build the control flow graph.
It is released under the GPL.
Eclipse plugin
Thanks to a group of ENSEEIHT students, Yasa is now interfaced with Eclipse. The Eclipse plugin is freely available under a GPL licence. It calls the analyzer and parse the XML result in order to show alarms and abstract elements computed.
A tutorial presents their approach to the Eclipse CDT plugin developement in order to interface a C static analyser.
Zen: an accurate centralizer tool allowing to model check distributed java applications using JavaPathFinder.
Related publications
Accurate Centralization for Applying Model Checking on Networked Applications -- ASE'06 [DOI] C. Artho, and P.-L. Garoche
Miscellaneous
When trying to use the Omega library which is a set of routines for manipulating linear constraints over integer variables, Presburger formulas, and Integer tuple relations and sets, we encounter several compilation problems. Here are some patches:
