Author name cluster

Silvio Ranise

Possible papers associated with this exact author name in Arrow. This page groups case-insensitive exact name matches and is not a full identity disambiguation profile.

9 papers

2 author rows

LPAR Conference 2012 Conference Paper

Lazy Abstraction with Interpolants for Arrays

Francesco Alberti
Roberto Bruttomesso
Silvio Ghilardi
Silvio Ranise
Natasha Sharygina

Abstract Lazy abstraction with interpolants has been shown to be a powerful technique for verifying imperative programs. In presence of arrays, however, the method shows an intrinsic limitation, due to the fact that successful invariants usually contain universally quantified variables, which are not present in the program specification. In this work we present an extension of the interpolation-based lazy abstraction in which arrays of unknown length can be handled in a natural manner. In particular, we exploit the Model Checking Modulo Theories framework, to derive a backward reachability version of lazy abstraction that embeds array reasoning. The approach is generic, in that it is valid for both parameterized systems and imperative programs. We show by means of experiments that our approach can synthesize and prove universally quantified properties over arrays in a completely automatic fashion.

Details

I&C Journal 2011 Journal Article

Automatic decidability and combinability

Christopher Lynch
Silvio Ranise
Christophe Ringeissen
Duc-Khanh Tran

Verification problems can often be encoded as first-order validity or satisfiability problems. The availability of efficient automated theorem provers is a crucial pre-requisite for automating various verification tasks as well as their cooperation with specialized decision procedures for selected theories, such as Presburger Arithmetic. In this paper, we investigate how automated provers based on a form of equational reasoning, called paramodulation, can be used in verification tools. More precisely, given a theory T axiomatizing some data structure, we devise a procedure to answer the following questions. Is the satisfiability problem of T decidable by paramodulation? Can a procedure based on paramodulation for T be efficiently combined with other specialized procedures by using the Nelson–Oppen schema? Finally, if paramodulation decides the satisfiability problem of two theories, does it decide satisfiability in their union? The procedure capable of answering all questions above is based on Schematic Saturation; an inference system capable of over-approximating the inferences of paramodulation when solving satisfiability problems in a given theory T. Clause schemas derived by Schematic Saturation describe all clauses derived by paramodulation so that the answers to the questions above are obtained by checking that only finitely many different clause schemas are derived or that certain clause schemas are not derived.

Details DOI

LPAR Conference 2006 Conference Paper

Automatic Combinability of Rewriting-Based Satisfiability Procedures

Hélène Kirchner
Silvio Ranise
Christophe Ringeissen
Duc-Khanh Tran

Abstract We address the problems of combining satisfiability procedures and consider two combination scenarios: (i) the combination within the class of rewriting-based satisfiability procedures and (ii) the Nelson-Oppen combination of rewriting-based satisfiability procedures and arbitrary satisfiability procedures. In each scenario, we use meta-saturation, which schematizes saturation of the set containing the axioms of a given theory and an arbitrary set of ground literals, to syntactically decide sufficient conditions for the combinability of rewriting-based satisfiability procedures. For (i), we give a sufficient condition for the modular termination of meta-saturation. When meta-saturation for the union of theories halts, it yields a rewriting-based satisfiability procedure for the union. For (ii), we use meta-saturation to prove the stable infiniteness of the component theories and deduction completeness of their rewriting-based satisfiability procedures. These properties are important to establish the correctness of the Nelson-Oppen combination method and to obtain an efficient implementation.

Details

JELIA Conference 2006 Conference Paper

Deciding Extensions of the Theory of Arrays by Integrating Decision Procedures and Instantiation Strategies

Silvio Ghilardi
Enrica Nicolini
Silvio Ranise
Daniele Zucchelli

Abstract The theory of arrays, introduced by McCarthy in his seminal paper “Toward a mathematical science of computation”, is central to Computer Science. Unfortunately, the theory alone is not sufficient for many important verification applications such as program analysis. Motivated by this observation, we study extensions of the theory of arrays whose satisfiability problem (i. e. checking the satisfiability of conjunctions of ground literals) is decidable. In particular, we consider extensions where the indexes of arrays has the algebraic structure of Presburger Arithmetic and the theory of arrays is augmented with axioms characterizing additional symbols such as dimension, sortedness, or the domain of definition of arrays. We provide methods for integrating available decision procedures for the theory of arrays and Presburger Arithmetic with automatic instantiation strategies which allow us to reduce the satisfiability problem for the extension of the theory of arrays to that of the theories decided by the available procedures. Our approach aims to reuse as much as possible existing techniques so to ease the implementation of the proposed methods. To this end, we show how to use both model-theoretic and rewriting-based theorem proving (i. e. , superposition) techniques to implement the instantiation strategies of the various extensions.

Details

I&C Journal 2006 Journal Article

Efficient theory combination via boolean search

Marco Bozzano
Roberto Bruttomesso
Alessandro Cimatti
Tommi Junttila
Silvio Ranise
Peter van Rossum
Roberto Sebastiani

Many approaches to deciding the satisfiability 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 T is the combination T 1 ∪ T 2 of two simpler theories, the approach is typically instantiated by means of a theory combination schema (e. g. Nelson–Oppen, Shostak). In this paper we propose a new approach to SMT ( T 1 ∪ T 2 ), where the enumerator of truth assignments is integrated with two decision procedures, one for T 1 and one for T 2, acting independently from each other. The key idea is to search for a truth assignment not only to the atoms occurring in the formula, but also to all the equalities between variables which are shared between the theories. 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 state-of-the-art competitor tools, showing that our implemented tool compares positively with them, sometimes with dramatic gains in performance.

Details DOI

IS Journal 2006 Journal Article

Intelligent Systems and Formal Methods in Software Engineering

Bernhard Beckert
Tony Hoare
Reiner Hahnle
Douglas Smith
Cordell Green
Silvio Ranise
Cesare Tinelli
Thomas Ball

Over the last few years, technologies for the formal description, construction, analysis, and validation of software - based mostly on logics and formal reasoning - have matured. We can expect them to complement and partly replace traditional software engineering methods in the future. Formal methods in software engineering are an increasingly important application area for intelligent systems. The field has outgrown the area of academic case studies, and industry is showing serious interest. We convincingly argue that we've reached the point where we can solve the problem of how to formally verify industrial-scale software. We propose program verification as a computer science Grand Challenge. Deductive software verification is a core technology of formal methods. We describe recent dramatic changes in the way it's perceived and used. Another important base technique of formal methods, besides software verification, is synthesizing software that's correct by construction because it's formally derived from its specification. We discuss recent developments and trends in this area. Surprisingly efficient decision procedures for the satisfiability modulo theories problem have recently emerged. We explain these techniques and why they're important for all formal-methods tools. We look at formal methods from an industry perspective. We explain the success of Microsoft Research's SLAM project, which has developed a verification tool for device drivers

Details DOI

LPAR Conference 2004 Conference Paper

Combining Lists with Non-stably Infinite Theories

Pascal Fontaine
Silvio Ranise
Calogero G. Zarba

Abstract In program verification one has often to reason about lists over elements of a given nature. Thus, it becomes important to be able to combine the theory of lists with a generic theory T modeling the elements. This combination can be achieved using the Nelson-Oppen method only ifT is stably infinite. The goal of this paper is to relax the stable-infiniteness requirement. More specifically, we provide a new method that is able to combine the theory of lists with any theory T of the elements, regardless of whether T is stably infinite or not. The crux of our combination method is to guess an arrangement over a set of variables that is larger than the one considered by Nelson and Oppen. Furthermore, our results entail that it is also possible to combine T with the more general theory of lists with a length function.

Details

I&C Journal 2003 Journal Article

A rewriting approach to satisfiability procedures

Alessandro Armando
Silvio Ranise
Michaël Rusinowitch

We show how a well-known superposition-based inference system for first-order equational logic can be used almost directly for deciding satisfiability in various theories including lists, encryption, extensional arrays, extensional finite sets, and combinations of them. We also give a superposition-based decision procedure for homomorphism.

Details DOI

CSL Conference 2001 Conference Paper

Uniform Derivation of Decision Procedures by Superposition

Alessandro Armando
Silvio Ranise
Michaël Rusinowitch

Abstract We show how a well-known superposition-based inference system for first-order equational logic can be used almost directly as a decision procedure for various theories including lists, arrays, extensional arrays and combinations of them. We also give a superposition-based decision procedure for homomorphism.

Details