Lazy Abstraction with Interpolants for Arrays

traction with Interpolants for Arrays Francesco Alberti1 , Roberto Bruttomesso2 , Silvio Ghilardi2 , Silvio Ranise3 , Natasha Sharygina1 1 Universit`a della Svizzera Italiana, Lugano, Switzerland 2 Universit`a degli Studi di Milano, Milan, Italy 3 FBK-Irst, Trento, Italy 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 nt 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 imperativ...

• Type: Journal
• Year: 2012
• Where: LPAR
• Authors: Francesco Alberti, Roberto Bruttomesso, Silvio Ghilardi, Silvio Ranise, Natasha Sharygina
• Keywords: Automated Reasoning, Della Svizzera Italiana, Irst Trento, LPAR 2012, Lugano Switzerland