@conference {358, title = {Lookahead in Partitioning SMT}, booktitle = {Formal Methods in Computer-Aided Design - FMCAD 2021}, year = {2021}, publisher = {IEEE digital library}, organization = {IEEE digital library}, address = {Online Conference}, abstract = {

Lookahead in propositional satisfiability has proven efficient as a heuristic in pre- and in-processing, for partitioning instances for parallel solving, and as the main driver of a standalone solver. While applying similar techniques in satisfiability modulo theories is potentially equally useful, adapting lookahead to learning theory clauses and to estimating search space sizes in the presence of first-order structures is not straightforward. This paper addresses both of these observations. We give a hybrid algorithm that integrates lookahead into the state-based representation of an SMT solver and show that in the vast majority of cases it is possible to compute full lookahead up to depth four on inexpensive theories. We also show the role of first-order structures in SMT search space: while in most of our benchmarks the partitions are easier to solve than the original instance, we identify cases where lookahead results in sequences of increasingly difficult instances for a computationally expensive theory.

}, author = {Antti E. J. Hyv{\"a}rinen and Matteo Marescotti and Natasha Sharygina} } @conference {353, title = {Lattice-based SMT for program verification}, booktitle = {International Conference on Formal Methods and Models for System Design, (MEMOCODE)}, year = {2019}, publisher = {ACM-IEEE}, organization = {ACM-IEEE}, abstract = {

We present a lattice-based satisfiability modulo theory for verification of programs with library functions, for which the mathematical libraries supporting these functions contain a high number of equations and inequalities. Common strategies for dealing with library functions include treating them as uninterpreted functions or using the theories under which the functions are fully defined. The full definition could in most cases lead to instances that are too large to solve efficiently. Our lightweight theory uses lattices for efficient representation of library functions by a subset of guarded literals. These lattices are constructed from equations and inequalities of properties of the library functions. These subsets are found during the lattice traversal. We generalise the method to a number of lattices for functions whose values depend on each other in the program, and we describe a simultaneous traversal algorithm of several lattices, so that a combination of guarded literals from all lattices does not lead to contradictory values of their variables. We evaluate our approach on benchmarks taken from the robotics community, and our experimental results demonstrate that we are able to solve a number of instances that were previously unsolvable by existing SMT solvers.

}, url = {https://dl.acm.org/doi/10.1145/3359986.3361214}, author = {Karine Even Mendoza and Antti E. J. Hyv{\"a}rinen and Hana Chockler and Natasha Sharygina} } @conference {287, title = {Lattice-Based Refinement in Bounded Model Checking}, booktitle = {VSTTE}, year = {2018}, month = {07/2018}, author = {Karine Even-Mendoza and Sepideh Asadi and Antti Hyv{\"a}rinen and Hana Chockler and Natasha Sharygina} } @conference {290, title = {Lookahead-Based SMT Solving}, booktitle = {LPAR-22}, year = {2018}, month = {November 2018}, publisher = {EasyChair}, organization = {EasyChair}, address = {Awassa, Ethiopia}, url = {http://www.inf.usi.ch/postdoc/hyvarinen/publications/HyvarinenMSCS_LPAR2018.pdf}, author = {Antti E. J. Hyv{\"a}rinen and Matteo Marescotti and Parvin Sadigova and Hana Chockler and Natasha Sharygina} } @conference {279, title = {LRA Interpolants from No Man{\textquoteright}s Land}, booktitle = {Haifa Verification Conference (HVC)}, year = {2017}, publisher = {Springer{\textquoteright}s Lecture Notes in Computer Science series (LNCS)}, organization = {Springer{\textquoteright}s Lecture Notes in Computer Science series (LNCS)}, author = {Leonardo Alt and Antti E. J. Hyv{\"a}rinen and Natasha Sharygina} } @article {164, title = {Loop summarization using state and transition invariants}, journal = {Formal Methods in System Design}, volume = {42}, year = {2013}, issn = {0925-9856}, author = {Kroening, D. and Natasha Sharygina and Tonetta, S. and Tsitovich, A. and Wintersteiger, C.M.} } @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 { twks11, title = {Loop Summarization and Termination Analysis}, booktitle = {International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS)}, volume = {6605}, year = {2011}, pages = {81-95}, publisher = {Springer}, organization = {Springer}, address = {Saarbr{\"u} Germany}, url = {http://dx.doi.org/10.1007/978-3-642-19835-9_9}, author = {Aliaksei Tsitovich and Natasha Sharygina and Christoph M. Wintersteiger and Kroening, Daniel} } @conference {153, title = {Loopfrog: A Static Analyzer for ANSI-C Programs}, booktitle = {The 24th IEEE/ACM International Conference on Automated Software Engineering}, year = {2009}, publisher = {IEEE Computer Society}, organization = {IEEE Computer Society}, address = {Auckland, New Zealand}, abstract = {

Practical software verification is dominated by two major classes of techniques. The first is model checking, which provides total precision, but suffers from the state space explosion problem. The second is abstract interpretation, which is usually much less demanding, but often returns a high number of false positives.

We present Loopfrog, a static analyzer that combines the best of both worlds: the precision of model checking and the performance of abstract interpretation. In contrast to traditional static analyzers, it also provides "leaping" counterexamples to aid in the diagnosis of errors.

}, author = {Kroening, D. and Natasha Sharygina and Tonetta, S. and Tsitovich, A. and Wintersteiger, C.M.} } @conference {152, title = {Loop Summarization using Abstract Transformers}, booktitle = {6th International Symposium on Automated Technology for Verification and Analysis (ATVA)}, year = {2008}, publisher = {Springer, Volume 5311}, organization = {Springer, Volume 5311}, address = {Seoul, South Korea}, abstract = {

Existing program analysis tools that implement abstraction rely on saturating procedures to compute over-approximations of fixpoints. As an alternative, we propose a new algorithm to compute an over-approximation of the set of reachable states of a program by replacing loops in the control flow graph by their abstract transformer. Our technique is able to generate diagnostic information in case of property violations, which we call leaping counterexamples. We have implemented this technique and report experimental results on a set of large ANSI-C programs using abstract domains that focus on properties related to string-buffers.

}, author = {Kroening, D. and Natasha Sharygina and Tonetta, S. and Tsitovich, A. and Wintersteiger, C.M.} }