@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 {288, title = {Function Summarization Modulo Theories}, booktitle = {22nd International Conference on Logic for Programming Artificial Intelligence and Reasoning, LPAR}, year = {2018}, publisher = {EasyChair Publications}, organization = {EasyChair Publications}, address = {Ethiopia}, keywords = {Author keywords: Software Verification Bounded Model Checking, Craig Interpolation, Function Summaries, Incremental Verification, Satisfiability Modulo Theories, Software Verification}, doi = {10.29007/d3bt}, url = {https://easychair.org/publications/paper/nNLJ}, author = {Sepideh Asadi and Martin Blicha and Grigory Fedyukovich and Antti E. J. Hyv{\"a}rinen and Karine Even-Mendoza and Natasha Sharygina and Hana Chockler} } @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 {269, title = {HiFrog: SMT-based Function Summarization for Software Verification}, booktitle = {23rd International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS)}, year = {2017}, publisher = {Springer}, organization = {Springer}, address = {Uppsala}, abstract = {

Abstract. Function summarization can be used as a means of incremental\ verication based on the structure of the program. HiFrog is\ a fully featured function-summarization-based model checker that uses\ SMT as the modeling and summarization language. The tool supports\ three encoding precisions through SMT: uninterpreted functions, linear\ real arithmetics, and propositional logic. In addition the tool allows optimized\ traversal of reachability properties, counter-example-guided summary\ renement, summary compression, and user-provided summaries.\ We describe the use of the tool through the description of its architecture\ and a rich set of features. The description is complemented by an experimental\ evaluation on the practical impact the dierent SMT precisions\ have on model-checking.

}, url = {https://link.springer.com/chapter/10.1007/978-3-662-54580-5_12 }, author = {Leonardo Alt and Sepideh Asadi and Hana Chockler and Karine Even Mendoza and Grigory Fedyukovich and Antti E. J. Hyv{\"a}rinen and Natasha Sharygina} } @proceedings {238, title = {Theory Refinement for Program Verification}, year = {2017}, publisher = {Springer LNCS series}, address = {Melbourne, Australia}, abstract = {
Recent progress in automated formal verification is to a large degree\ due to the development of constraint languages that are sufficiently light-weight for reasoning but still expressive enough to prove\ properties of programs. Satisfiability modulo theories (SMT) solvers implement efficient\ decision procedures, but offer little direct support for adapting the constraint language to the task at hand. Theory refinement\ is a new approach that modularly adjusts the\ modeling precision based on the properties being verified through the use of\ combination\ of theories. We implement the approach using an augmented version of the theory of\ bit-vectors and uninterpreted functions capable of directly injecting\ non-clausal refinements to the inherent Boolean structure of SMT. In our comparison to a state-of-the-art model checker, our prototype\ implementation is in general competitive, being several orders of magnitudes faster on some instances that are challenging for flattening,\ while computing models that are significantly more succinct.
}, url = {http://verify.inf.usi.ch/hifrog/theoref}, author = {Antti E. J. Hyv{\"a}rinen and Sepideh Asadi and Karine Even Mendoza and Grigory Fedyukovich and Hana Chockler and Natasha Sharygina} }