@article {193, title = {An extension of lazy abstraction with interpolation for programs with arrays}, journal = {FMSD}, year = {2014}, keywords = {Array programs, Lazy abstraction, Model checking, SMT}, issn = {1572-8102}, doi = {10.1007/s10703-014-0209-9}, author = {Francesco Alberti and Bruttomesso, R. and Ghilardi, S. and Ranise, S. and Natasha Sharygina} } @article {168, title = {Resolution Proof Transformation for Compression and Interpolation}, journal = {CoRR}, volume = {July 2013}, year = {2013}, author = {Rollini, S.F. and Bruttomesso, R. and Natasha Sharygina and Tsitovich, A.} } @conference {150, title = {Lazy Abstraction with Interpolation for Arrays}, booktitle = {18th International Conference on Logic for Programming Artificial Intelligence and Reasoning (LPAR)}, year = {2012}, publisher = {Springer}, organization = {Springer}, address = {M{\'e}rida, Venezuela}, 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 an prove universally quantified properties over arrays in a completely automatic fashion.

}, author = {Francesco Alberti and Bruttomesso, R. and Ghilardi, S. and Ranise, S. and Natasha Sharygina} } @conference {151, title = {SAFARI: SMT-based Abstraction For Arrays with Interpolants}, booktitle = {24th International Conference on Computer Aided Verification (CAV)}, year = {2012}, publisher = {Springer}, organization = {Springer}, address = {Berkeley, California, USA}, abstract = {

We present SAFARI, a model checker designed to prove (possibly universally quantified) safety properties of imperative programs with arrays of unknown length. SAFARI is based on an extension of lazy abstraction capable of handling existentially quantified formul{\ae} for symbolically representing states. A heuristics, called term abstraction, favors the convergence of the tool by {\textquotedblleft}tuning{\textquotedblright} interpolants and guessing additional quantified variables of invariants to prune the search space efficiently.

}, author = {Francesco Alberti and Bruttomesso, R. and Ghilardi, S. and Ranise, S. and Natasha Sharygina} } @conference {144, title = {An Efficient and Flexible Approach to Resolution Proof Reduction}, booktitle = {Haifa Verification Conference (HVC)}, year = {2010}, publisher = {Springer}, organization = {Springer}, address = {Haifa, Israel}, abstract = {

A propositional proof of unsatisfiability is a certificate of the\ unsatisfiability of a Boolean formula. Resolution proofs, as generated by\ modern SAT solvers, find application in many verification techniques\ where the size of the proofs considerably affects efficiency. This paper\ presents a new approach to proof reduction, situated among the purely\ post-processing methods. The main idea is to reduce the proof size by\ eliminating redundancies of occurrences of pivots along the proof paths.\ This is achieved by matching and rewriting local contexts into simpler\ ones. In our approach, rewriting can be easily customized in the way\ local contexts are matched, in the amount of transformations to be performed, or in the different application of the rewriting rules. We provide\ an extensive experimental evaluation of our technique on a set of SMT\ benchmarks, which shows considerable reduction in the proofs size.

}, author = {Rollini, S.F. and Bruttomesso, R. and Natasha Sharygina} } @conference {145, title = {Flexible Interpolation with Local Proof Transformations}, booktitle = {International Conference of Computer Aided Design (ICCAD)}, year = {2010}, publisher = {IEEE Computer Society}, organization = {IEEE Computer Society}, address = {San Jose, USA}, abstract = {

Model checking based on Craig{\textquoteright}s interpolants ultimately relies on efficient engines, such as SMT-solvers, to log proofs of unsatisfiability and to derive the desired interpolant by means of a set of algorithms known in literature. These algorithms, however, are designed for proofs that do not contain mixed predicates. In this paper we present a technique for transforming the propositional proof produced by an SMT-solver in such a way that mixed predicates are eliminated. We show a number of cases in which mixed predicates arise as a consequence of state-of-the-art solving procedures (e.g. lemma on demand, theory combination, etc.). In such cases our technique can be applied to allow the application of known interpolation algorithms. We demonstrate with a set of experiments that our approach is viable.

}, author = {Bruttomesso, R. and Rollini, S.F. and Natasha Sharygina and Tsitovich, A.} } @conference { BPS10, title = {A Flexible Schema for Generating Explanations in Lazy Theory Propagation}, booktitle = {International Conference on Formal Methods and Models for Codesign (MEMOCODE)}, year = {2010}, note = {to appear}, publisher = {IEEE Computer Society}, organization = {IEEE Computer Society}, address = {Grenoble, France}, author = {Bruttomesso, R. and Pek, E. and Natasha Sharygina} } @conference { BPST10, title = {The OpenSMT Solver}, booktitle = {International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS)}, volume = {6015}, year = {2010}, pages = {150-153}, publisher = {Springer}, organization = {Springer}, address = {Paphos, Cyprus}, url = {http://dx.doi.org/10.1007/978-3-642-12002-2_12}, author = {Bruttomesso, R. and Pek, E. and Natasha Sharygina and Tsitovich, A.} } @conference {143, title = {An Extension of the Davis-Putnam Procedure and its Application to Preprocessing in SMT}, booktitle = {7th International Workshop on Satisfiability Modulo Theories (SMT)}, year = {2009}, publisher = {ACM}, organization = {ACM}, address = {Montreal, Canada}, author = {Bruttomesso, R.} } @conference {142, title = {A Scalable Decision Procedure for Fixed-Width Bit-Vectors}, booktitle = {International Conference of Computer Aided Design (ICCAD)}, year = {2009}, publisher = {ACM}, organization = {ACM}, address = {San Jose (CA)}, author = {Bruttomesso, R. and Natasha Sharygina} }