You are here
Silvio Ranise
 Email:
 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 20012002, INRIA researcher at the LORIA computer science laboratory of Nancy in 20022008, research associate at the University of Verona (in the context of the EU Project AVANTSSAR) in 20082010, visiting professor at the Department of Computer Science of the University of Milano. His research focuses on formal methods for the automatic analysis of securitysensitive 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 coordinator of the SMTLib 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.”

H. Kirchner; S. Ranise; C. Ringeissen; D. K. Tran,Automatic Combinability of RewritingBased Satisfiability Procedures,2006, (Logic for Programming, Artificial Intelligence, and Reasoning 13th International Conference, LPAR 2006,Phnom Penh, Cambodia,11/13/2006 a 11/17/2006)

S. Ranise; C. G. Zarba,A Theory of SinglyLinked Lists and its Extensible Decision Procedure,2006, (Fourth IEEE International Conference on Software Engineering and Formal Methods (SEFM 2006),Pune, India,09/11/2006 a 09/15/2006)

Armando A.; Compagna L.; Ranise S.,Rewrite and Decision Procedure Laboratory: Combining Rewriting, Satisfiability Checking, and Lemma Speculation,Mechanizing Mathematical Reasoning, Essays in Honor of Jörg H. Siekmann on the Occasion of his 60th Birthday,Berlin,SpringerVerlag,2005, pp. 30 45

A. Armando; L. Compagna; S. Ranise,Rewriting and Decision Procedure Laboratory: Combining Rewriting, Satisfiability Checking, and Lemma Speculation,Mechanizing Mathematical Reasoning: Essays in Honor of Jörg H. Siekmann on the Occasion of His 60th Birthday,Berlin Heidelberg,Springer,2005, pp. 30 45

Armando A.; Bonacina M. P.; Ranise S.; Schulz S.,On a rewriting approach to satisfiability procedures: extension, combination of theories and an experimental appraisal,in «LECTURE NOTES IN COMPUTER SCIENCE»vol.3717,2005, pp. 6580, (Frontiers of Combining Systems, 5th International Workshop, FroCoS 2005,Vienna, Austria,1921/09/2005)

H. Kirchner; S. Ranise; C. Ringeissen and D. K. Tran,On SuperpositionBased Satisfiability Procedures and Their Combination,2005, (Theoretical Aspects of Computing – ICTAC 2005,Hanoi, Vietnam,10/17/2005 a 10/21/2005)

S. Ranise; C. Ringeissen; C. G. Zarba,Combining Data Structures with Nonstably Infinite Theories Using ManySorted Logic,2005, (Frontiers of Combining Systems,Vienna, Austria,09/19/2005 a 09/21/2005)

P. Fontaine; S. Ranise; C. G. Zarba,Combining Lists with Nonstably Infinite Theories,2005, (Logic for Programming, Artificial Intelligence, and Reasoning 11th International Conference, LPAR 2004,Montevideo, Uruguay,03/14/2005 a 03/18/2005)

Marco Bozzano; Roberto Bruttomesso; Alessandro Cimatti; Tommi Junttila; Silvio Ranise; Peter van Rossum; Roberto Sebastiani,Efficient Satisfiability Modulo Theories via Delayed Theory Combination,Proceeding of 17th Int. Conference on Computer Aided Verification,Springer,vol.3576,2005, pp. 335349, (CAV,University of Edinburgh, Scotland, UK,610/07/2005)

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. NelsonOppen, 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 nonconvex theories (as opposed to traditional NelsonOppen combinations which require a mechanism for splitting). Furthermore, it can be made practical by leveraging on stateoftheart 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 nonconvex 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 speedups up to two orders of magnitude,2005