You are here
- Phone: 0461314192
- FBK Povo
Silvio Ranise received his Ms. Eng. in 1997 at the University of Genova (Italy) and his PhD in Computer Engineering from the University of Genova (Italy) and the University H. Poincare ́ (Nancy, France) in 2002 in the context of a joint PhD program between Italy and France. He works at FBK in the S&T Research Unit as Senior Researcher since April 2010. His previous appointments are: assistant professor at the U. H. Poincare ́ in 2001-2002, INRIA researcher at the LORIA computer science laboratory of Nancy in 2002-2008, research associate at the University of Verona (in the context of the EU Project AVANTSSAR) in 2008-2010, visiting professor at the Department of Computer Science of the University of Milano. His research focuses on formal methods for the automatic analysis of security-sensitive applications and he has published more than 65 papers in international conferences and journals on automated analysis of security policies, infinite state model checking, and Satisfiability Modulo Theories (SMT) solving. He has been initiator and co-ordinator of the SMT-Lib initiative, and started the SMT workshop series on SMT techniques. He has also given tutorials on SMT and infinite state model checking techniques at international conferences. In 2010, he received the HVC award for his “pivotal and continuous role in building and promoting the SMT community.”
M. Bozzano; R. Bruttomesso; A. Cimatti; T. Antero Junttila; S. Ranise; Rossum Peter van; R. Sebastiani,Efficient Theory Combination via Boolean Search,Many approaches to the decision of quantifier free formulae with respect to a background theory T - also known as Satisfiability Modulo Theory, or SMT(T) - rely on the integration between an enumerator of truth assignments and a decision procedure for conjunction of literals in T. When the background theory is the combination T1 U T2 of two simpler theories, the approach is typically instantiated by means of a combination schema (e.g. Nelson-Oppen, Shostak).
In this paper we propose a new approach to SMT(T1 U T2), where the enumerator of truth assignments is integrated with two decision procedures for T1 and for T2, which act independently from each other. The key idea is to search for a truth assignment not only to the atoms occurring in the purified formula, but also to all the equalities between interface variables.
This approach is simple and expressive: for instance, no modification is required to handle non-convex theories (as opposed to traditional Nelson-Oppen combinations which require a mechanism for splitting). Furthermore, it can be made practical by leveraging on state-of-the-art boolean and SMT search techniques, and on theory layering (i.e. cheaper reasoning first, and more often).
We provide thorough experimental evidence to support our claims: we instantiate the framework with two decision procedures for the combinations of Equality and Uninterpreted Functions (EUF) and Linear Arithmetic (LA), both for (the convex case of) reals and for (the non-convex case of) integers; we analyze the impact of the different optimizations on a variety of test cases; and we compare the approach with competitor tools, obtaining speed-ups up to two orders of magnitude,2005
M. Bozzano; R. Brutomesso; A. Cimatti; T. A. Junttila; S. Ranise; Rossen Peter van; R. Sebastiani,Efficient Satisfiability Modulo Theories via Delayed Theory Combination,The problem of deciding the satisfiability of a quantifier-free formula with respect to a background theory, also known as Satisfiability Modulo Theories (smt), is gaining increasing relevance in verification: representation capabilities beyond propositional logic allow for a natural modeling of real-world problems (e.g., pipeline and RTL circuits verification, proof obligations in software systems).
In this paper, we focus on the case where the background theory is the combination T1 U T2 of two simpler theories. Many smt procedures combine a boolean model enumeration with a decision procedure for T1 U T2, where conjunctions of literals can be decided by an integration schema such as Nelson-Oppen, via a structured exchange of interface formulae (e.g., equalities in the case of convex theories, disjunctions of equalities otherwise).
We propose a new approach for SMT(T1 U T2), called Delayed Theory Combination, which does not require a decision procedure for T1 U T2, but only individual decision procedures for T1 and T2, which are directly integrated to the boolean model enumerator.
This approach is much simpler and natural, allows each of the solvers to be implemented and optimized without taking into account the others, and it nicely encompasses the case of non-convex theories.
We show the effectiveness of the approach by a thorough experimental comparison,2005
J. F.. Couchot; A. Giorgetti; D. Deharbe; S. Ranise,Scalable Automated Proving and Debugging of Set-Based Specfications,in «JOURNAL OF THE BRAZILIAN COMPUTER SOCIETY»,vol. 2,n. 9,2004
S. Ranise; C. Ringeissen; D. K. Tran,Nelson-Oppen, Shostak and the Extended Canonizer: A Family Picture with a Newborn,2004, (Theoretical Aspects of Computing - ICTAC 2004 First International Colloquium,Guiyang, China,09/20/2004 a 09/24/2004)
D. Déharbe; A. Imine; S. Ranise,Abstraction-Driven Verification of Array Programs,2004, (Artificial Intelligence and Symbolic Computation 7th International Conference, AISC 2004,Linz, Austria,09/22/2004 a 09/24/2004)
Armando A.; Bonacina M.P.; Sehgal A. K.; Ranise S.; Rusinowitch M.,High Performance Deduction for verification: a case study in the theory of arrays,Proceedings of the 2nd Verification Workshop (VERIFY02),2002, pp. 103-112, (2nd Verification Workshop (VERIFY02),Copenhagen, Denmark,25-26/07/2002)
ARMANDO A.; COGLIO A.; GIUNCHIGLIA F.; RANISE S.,The Control Component of Open Mechanized Reasoning Systems: Annotation and Tactics,in «JOURNAL OF SYMBOLIC COMPUTATION»,vol. 32,2001, pp. 305 -332
ARMANDO A.; RANISE S.,A Practical Extension Mechanism for Decision Procedures:
the Case Study of Universal Presburger Arithmetic,in «JOURNAL OF UNIVERSAL COMPUTER SCIENCE»,vol. 7 (issue 2),2001, pp. 124 -140
Armando A.; Kohlhase M.; Ranise S.,Coommunication Protocols for Mathematical Services based on KQML and OMRS,Symbolic Computation and Automated Reasoning : The Calculemus-2000 Symposium,NATICK, MA,AK Peters, Ltd.,2001, pp. 33 -48
Armando A.; Peccia F.; Ranise S.,The Phase Transition of the Linear Inequalities Problem,Principles and Practice of Constraint Programming - CP 2001,vol.2239,2001, pp. 422-432, (7th International Conference, CP 2001,Paphos, Cyprus,26 nov/1 Dec 2001)