EUREKA is the name of a project at the artificial intelligence laboratory, a research lab within the university of genova, in collaboration with the section of computer science, physical sciences department, university of napoli "federico II".

EUREKA was also part of an italian research project (partially funded by the italian ministry of university) called synthesis of deduction-based decision procedures with applications to the automatic formal analysis of software (PRIN no. 2003-097383).

currently the EUREKA project consists of two branches: one deals with symbolic model checking in the framework of abstraction and refinement, while the other deals with bounded model checking. both the branches investigate the use of decision procedures (and their combination) in model checking of sequential software, particularly of C programs.

people currently involved in this project are:

• alessandro armando, associate professor, university of genova.
• massimo benerecetti, associate professor, university of napoli.
• jacopo mantovani, phd student, university of genova.
• dario carotenuto, phd student, university of napoli.
• pasquale spica, phd student, university of napoli.
• lorenzo platania, phd student, university of genova.
• Dario Della Monica, msc student, university of napoli.
• Fulvio Polito, msc student, university of napoli.

smt-cbmc stands for satisfiability modulo theories in C bounded model checking. intuitively, given a C program and some properties P, smt-cbmc builds a quantifier free formula (instead of a boolean propositional formula) such that every model (if any) represents a trace that leads to a violation of P. the formula is solved using smt solvers instead of sat solvers

please click here if you want to know more.

aim of this branch of the project is to develop an effective model checker for sequential C programs, following the counterexample guided abstraction refinement schema. Particularly, instead of abstracting to boolean programs we abstract to linear programs. linear programs differ from boolean programs in that program variables range over a numeric domain (e.g. the integers); moreover, all conditions and assignments to variables involve linear expressions.

please click here if you want to know more.

August, 2007
A. Armando, M. Benerecetti, D. Carotenuto, J. Mantovani, P. Spica
The Eureka Tool for Software Model Checking,
In the proceedings of the 22nd IEEE/ACM ASE Conference, Atlanta, Georgia, USA.
[pdf]

December, 2006
A. Armando, M. Benerecetti, J. Mantovani,
Abstraction Refinement of Linear Programs with Arrays,
In the proceedings of the 13th TACAS Conference, Braga, Portugal.
LNCS 4424, Springer Verlag.
[pdf]

January, 2006
A. Armando, J. Mantovani, L. Platania
Bounded Model Checking of Software using SMT Solvers instead of SAT Solvers.
In the proceedings of the 13th SPIN workshop, Vienna (A).
LNCS 3925, Springer Verlag.
[pdf][ps][DBLP bibtex]

June, 2005
A. Armando, M. Benerecetti, J. Mantovani,
Model Checking Linear Programs with Arrays.
In the proceedings of SoftMC 2005 International Workshop on Software Model Checking, Edinburgh (UK)
ENTCS Volume 144, Issue 3
[pdf][DBLP bibtex]

November, 2004
A. Armando, C. Castellini, J. Mantovani,
Software Model Checking using Linear Constraints.
ICFEM 2004, International Conference on Formal Engineering Methods, Seattle (USA)
LNCS Volume 3308, Springer Verlag.
[pdf][ps] [DBLP bibtex]

December, 2005
A. Armando, J. Mantovani, L. Platania
Bounded Model Checking of Software using SMT Solvers instead of SAT Solvers.
Technical Report, DIST, University of Genova.
(A revised version of this technical report is to appear also in the proceedings of the 13th SPIN workshop.)
[pdf][ps]

April, 2005
A. Armando, M. Benerecetti, J. Mantovani,
Abstracting Linear Programs with Arrays into Linear Programs.
Technical Report, DIST, University of Genova.
[pdf][ps]

May, 2004
A. Armando, C. Castellini, J. Mantovani,
Introducing Full Linear Arithmetic to Symbolic Software Model Checking.
Technical Report, DIST, University of Genova.
The long version of the above paper.
[pdf][ps]

28/03/2007
Abstraction Refinement of Linear Programs with Arrays.
Given by Jacopo Mantovani at TACAS 07, the 13th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, Braga, Portugal. A.
[pdf]

31/03/2006
Bounded Model Checking of Software using SMT solvers instead of SAT solvers.
Given by Lorenzo Platania at SPIN 06, the 13th International Workshop on Model Checking of Software, Vienna, A.
[pdf]

09/11/2005
Software Model Checking at AI-Lab.
Given by Jacopo Mantovani at the SAP Reseach Labs, Sophia Antipolis, France.
[pdf]

12/09/2005
Bounded Model Checking of C Programs using a SMT solver instead of a SAT solver.
Given by Alessandro Armando at the informal forum on decision procedures held in Cambridge, UK.
[pdf]

11/07/2005
Model Checking Linear Programs with Arrays.
Given by Jacopo Mantovani at SoftMC 2005, International Workshop on Software Model Checking, Edinburgh, Scotland, UK.
[pdf]

19/05/2005
Model Checking Imperative Programs.
Invited Talk given by Jacopo Mantovani at the Computer Science Department (DSI) of the University of Milano.
[pdf]

11/11/2004
Software Model Checking using Linear Constraints.
Given by Jacopo Mantovani at ICFEM 2004, the sixth International Conference on Formal Engineering Methods, Seattle, USA.
[pdf]

18/06/2004
Linear Constraints in Symbolic Software Model Checking.
Given by Jacopo Mantovani at CoVer3, the third CoVer Project Workshop, joint with CILC 2004.
[pdf]