Piergiorgio Bertoli
(researcher, ITC-IRST),
Marco Bozzano
(researcher, ITC-IRST),
Alessandro Cimatti
(researcher, ITC-IRST),
Roberto Sebastiani
(assistant professor, University of Trento, collaborator of ITC-IRST).
IRST participates in tasks: 1.2, 2.3, 3.2 and 3.4. IRST is a leader
of tasks 1.2 and 3.4.
The definition of decision procedures for expressive logical theories,
in particular those handling formulas combining boolean propositions
and constraints over real variables, is a very important and
challenging problem. Its importance lies in the fact that problems
arising from different real-world domains, ranging from formal
verification of infinite state systems to planning with resources, can
be easily encoded as decision problems for such theories. The challenge
is to define automatic decision procedures, that are able to deal with
a wide class of problems, but are also able to recognize easy problems
and to deal with them efficiently.
In particular, our ultimate goal goes in direction of the development
of verification tools (model checkers) for complex real-world systems
and protocols, in particular of timed systems. This requires procedures
able to handle both the (rather heavy) boolean reasoning component and
the mathematical solving component which are intrinsic in this kind of
problems.
As our contribution to Task 1.2, we present the foundations and the
basic algorithms for a new class of procedures for solving boolean
combinations of boolean and mathematical propositions, which combine
boolean and mathematical solvers, and we highlight the main
requirements that boolean and mathematical solvers must fulfil in order
to achieve the maximum benefits from their integration.
For details see [1,2,4,
10].
As our contribution to Task 2.3, we present MathSAT. MathSAT is a
decision procedures for combinations of boolean and linear mathematical
propositions, based on two main ingredients. The first is a SAT
procedure, for dealing efficiently with the propositional component of
the problem. The second is a tight integration, within the DPLL
architecture, of a set of mathematical deciders for theories of
increasing expressive power. The existence of such procedure opens the
ability to solve problems arising from real-world domains such as
verification of timed and hybrid systems and planning with resources.
For details see [2].
As our contribution to Task 3.2 we propose a new, symbolic verification
technique that extends the Bounded Model Checking (BMC) approach for
the verification of timed and hybrid systems. The approach is based on
the
following ingredients. First, a BMC problem for timed systems is
reduced to the satisfiability of a math-formula, i.e., a boolean
combination of propositional variables and linear mathematical
relations over real variables (used to represent clocks and continuous
dynamics). Then, an
appropriate solver, a customized version of MathSAT (see above), is
used to check the satisfiability of the math-formula.
The proposed approach allows for handling expressive properties in a
fully-symbolic way. A preliminary experimental evaluation confirms the
potential of the approach.
For details see [3,
9].
Finally, as our contribution to Task 3.4, we show how existing systems
are captured by our framework described in task 1.2.
For details see [1].
Gilles Audemard (University of Provence, France). Young
visiting researcher at IRST (Trento) from 1/11/01 to 31/8/02.
Gilles' work focused on the analysis, design and implementation of efficient algorithms that combine algebraic decision procedures (mathematical solving & computing services) and logical reasoning capabilities (proving services), with the main goal of automatically verifying timed systems. In particular, he took part to the requirement analysis, design and implementation of MathSAT [2], a system combining the (high-performances) boolean reasoning capabilities of the SAT procedure SIM with the mathematical solving capability of a home-made decision procedure for linear arithmetic formulas over the reals. He has taken in charge the development of the resulting system.
He contributed to the development of the general framework (logical foundations and basic algorithms) for combining boolean decision procedures and mathematical solvers, and to the definition of the main requirements that boolean and mathematical solvers must fulfill in order to achieve the maximum benefits from their integration [1]. To this extent, his contribution focused mainly on the requirements for boolean decision procedures.
He also contributed to the development of the encoder able to convert a Bounded Model Checking problem for timed systems into the satisfiability of math-formulas[3].
Gilles already had a good background in pure SAT. He has undergone an intensive training in formal methods, model checking, techniques for integrating SAT with domain-specific procedures and techniques for mathematical solving.
He presented a part of his work during the CALCULEMUS Network Task Forces Meeting (Genova, 14-15 February 2002).
Artur Kornilowicz (University of Bialystok, Poland). Young
visiting researcher at IRST (Trento) from 16/7/01 to 30/6/02.
Artur's work focused on the design and implementation of efficient algorithms that automatically establish the satisfiability of a specific class of mathematical formulae, which can be used to model timed systems. The algorithms are designed in order to closely integrate as a Math-Solver module of MathSAT [2]. He has taken in charge the development of the Math-Solver module.Daniel Sheridan (School of Informatics, University of Edumburgh). Young visiting researcher at IRST (Trento) from 13/2/03 to 6/4/03.
He also contributed to the development of the general framework for combining boolean decision procedures and mathematical solvers, and to the definition of the main requirements that boolean and mathematical solvers must fulfill in order to achieve the maximum benefits from their integration [1]. To this extent, his contribution focused mainly on the requirements for mathematical solvers.
He contributed to the conception of the logical encoding for converting a Bounded Model Checking problem for timed systems into the satisfiability of math-formulas[3].
Artur already had a good background in logic and in logical formalization of problems. He has undergone an intensive training in SAT, formal methods, model checking, techniques for integrating SAT with domain-specific procedures, and algorithms for mathematical solving.
He presented a part of his work during the CALCULEMUS Network Task Forces Meeting (Genova, 14-15 February 2002).
Stephan worked on four main topics during his CALCULEMUS stay: Communication protocols for reasoning systems, improvements for first-order deduction systems, automated domain exploration, and decision procedures for fragments of first order logic. Most of his work at ICT/irst was on the last topic. He developed and implemented a robust and efficient congruence closure algorithm that forms the equational solver of the latest version of MathSat. The system makes MathSat into an efficient decision procedure for the logic of equality with uninterpreted function symbols (EUF) and plays an important role in reasoning about other theories. In fall 2003, Stephan attended the Fourth International Workshop on the Implementation of Logics (as an invited speaker) and LPAR-2004. In summer 2004, he presented a number of results obtained during his CALCULEMUS work at IJCAR-2004 and the IJCAR-Workshop on Empirically Successful First-Order Reasoning. He published the papers [11,12,13,14].Tommi Junttila (Helsinki University of Technology, Finland). Young visiting researcher at IRST (Trento) from 15/1/04 to 31/8/04.
Tommi's work focused on the analysis, design and implementation of efficient algorithms that combine algebraic decision procedures (mathematical solving) and logical reasoning capabilities (proving services). In particular, he took part to the requirement analysis, design and implementation of the new version of MathSAT [2], a system combining the (high-performance) boolean reasoning capabilities with the mathematical solving capability. His main contributions were the designing and implementing the top-level solver module and the preprocessor for non-clausal formulae in the new version of the MathSAT solver. The top-level solver extends the Minisat Boolean satisfiability checker developed at Chalmers University by interfacing it with the data structures representing non-Boolean formulae and with theory specific solvers such as one for the theory of equality with uninterpreted functions and one for linear and non-linear arithmetics. The preprocessor for non-clausal formulae enables one to use more natural and compact form for describing problems. The formulae are then translated to the special conjunctive normal form accepted by the top-level solver by a series of satisfiability preserving steps. In addition, he has contributed to the bounded model checker module of the NuSMV symbolic model checker. He has improved the Boolean circuit package in NuSMV so that it now produces more compact representations of problems. Furthermore, he has designed and implemented a module for incremental satisfiability checking in NuSMV. Based on this module, he has implemented the temporal induction algorithms described by Een and Sorensen in [6] and integrated incremental SAT solving also to bounded model checking of linear time temporal properties. During his stay in Trento he has participated in two conferences, the International Conference on Application of Concurrency to System Design (ACSD 2004) in Hamilton, Canada, June 2004 and 25th International Conference on Application and Theory of Petri Nets (ATPN 2004) in Bologna, Italy, June 2004. In these conferences, he presented new results concerning the symmetry reduction method for explicit state space anylysis obtained prior to the visit at IRST. The presented papers are [7][8] The conference trips were funded by IRST through the CALCULEMUS project.Peter van Rossum (The Netherlands). Young visiting researcher at IRST (Trento) from 15/1/04 to 31/8/04.
The focus of his work has been towards the constant improvement of the model checker NuSMV. Initially this involved working on increasing the functionality provided by the program, by means of allowing input files to be automatically run through external preprocessors. He also made the modifications necessary to integrate the improved RBC encodings which Tommi Junttila had provided. He has been involved in the revision of the user-manual and tutorial to reflect the changes made to NuSMV. The other main area of his work has been to investigate the boolean encoding methods used by NuSMV, with the aim of improving the solution times for SAT-based bounded model checking. Primarily, it has focused on reducing the size of the formula which is passed to the external SAT solver. He has also been involved in the testing and benchmarking of the new incremental algorithms which have been added to the latest version of NuSMV.