@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} } @conference {210, title = {On Interpolants and Variable Assignments}, booktitle = {Formal Methods in Computer-Aided Design (FMCAD)}, year = {2014}, address = {Lausanne, Switzerland}, author = {Jancik, P. and KofronĖ‡, J. and Rollini, S.F. and Natasha Sharygina} } @conference {147, title = {Interpolation Properties and SAT-based Model Checking}, booktitle = {11th International Symposium on Automated Technology for Verification and Analysis (ATVA)}, year = {2013}, author = {Gurfinkel, A. and Rollini, S. F. and Natasha Sharygina} } @conference {160, title = {A Parametric Interpolation Framework for First-Order Theories}, booktitle = {12th Mexican International Conference on Artificial Intelligence (MICAI)}, year = {2013}, author = {Kovacs, L. and Rollini, S.F. and Natasha Sharygina} } @conference {180, title = {PeRIPLO: A Framework for Producing Efficient Interpolants for SAT-based Software Verification}, booktitle = {Logic for Programming Artificial Intelligence and Reasoning (LPAR)}, year = {2013}, address = {Stellenbosch, South Africa}, author = {Rollini, S.F. and Leonardo Alt and Grigory Fedyukovich and Antti E. J. Hyv{\"a}rinen and Natasha Sharygina} } @conference {165, title = {PINCETTE - Validating Changes and Upgrades in Networked Software}, booktitle = {17th European Conference on Software Maintenance and Reengineering}, year = {2013}, author = {Chockler, H. and Denaro, G. and Ling, M. and Grigory Fedyukovich and Antti E. J. Hyv{\"a}rinen and Mariani, L. and Muhammad, A. and Oriol, M. and Rajan, A. and Sery, O. and Natasha Sharygina and Tautschnig, M.} } @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 {159, title = {Using Cross-Entropy for Satisfiability}, booktitle = {ACM Symposium on Applied Computing (SAC)}, year = {2013}, author = {Chockler, H. and Ivrii, A. and Matsliah, A. and Rollini, S.F. and Natasha Sharygina} } @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 {146, title = {Leveraging Interpolant Strength in Model Checking}, booktitle = {24th International Conference on Computer Aided Verification (CAV)}, year = {2012}, publisher = {Springer}, organization = {Springer}, address = {Berkeley, California, USA}, abstract = {

Craig interpolation is a well known method of abstraction successfully used in both hardware and software model checking. The logical strength of interpolants can affect the quality of approximations and consequently the performance of the model checkers. Recently, it was observed that for the same resolution proof a complete lattice of interpolants ordered by strength can be derived.
Most state-of-the-art model checking techniques based on interpolation subject the interpolants to constraints that ensure efficient verification as, for example, in transition relation approximation for bounded model checking, counterexample-guided abstraction refinement and function summarization for software update checking. However, in general, these verification-specific constraints are not satisfied by all possible interpolants.
The paper analyzes the restrictions within the lattice of interpolants under which the required constraints are satisfied. This enables investigation of the effect of the strength of interpolants on the particular techniques, while preserving their soundness. As an additional benefit, combination of this result with proof manipulation procedures allows the use of optimized solvers to generate interpolants of different strengths for various model checking techniques.

}, author = {Rollini, S.F. and Sery, O. 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.} }