@article {379, title = {SMT-based verification of program changes through summary repair}, journal = {Formal Methods in System Design}, year = {2023}, month = {05/2023}, abstract = {This article provides an innovative approach for verification by model checking of programs that undergo continuous changes. To tackle the problem of repeating the entire model checking for each new version of the program, our approach verifies programs incrementally. It reuses computational history of the previous program version, namely function summaries. In particular, the summaries are over-approximations of the bounded program behaviors. Whenever reusing of summaries is not possible straight away, our algorithm repairs the summaries to maximize the chance of reusability of them for subsequent runs. We base our approach on satisfiability modulo theories (SMT) to take full advantage of lightweight modeling approach and at the same time the ability to provide concise function summarization. Our approach leverages pre-computed function summaries in SMT to localize the checks of changed functions. Furthermore, to exploit the trade-off between precision and performance, our approach relies on the use of an SMT solver, not only for underlying reasoning, but also for program modeling and the adjustment of its precision. On the benchmark suite of primarily Linux device drivers versions, we demonstrate that our algorithm achieves an order of magnitude speedup compared to prior approaches.}, doi = {https://doi.org/10.1007/s10703-023-00423-0}, url = {https://link.springer.com/epdf/10.1007/s10703-023-00423-0?sharing_token=irB5EyKrDQwFBGsATR5X_Pe4RwlQNchNByi7wbcMAY69DCBPoCd5OukXnJUT4hJ-i8lTSfPkBgFCDWhP5zZ6F07I66RayboKJEpVSax8y-1gkPqsTej9UbMHSNiNQ_jERujVnNQQ7kvxuZcpsB3rGMYcHJEINXClhcP3Ttz85V4=}, author = {Sepideh Asadi and Martin Blicha and Antti E. J. Hyv{\"a}rinen and Grigory Fedyukovich and Natasha Sharygina} } @conference {369, title = {SolCMC: Solidity Compiler{\textquoteright}s Model Checker}, booktitle = {CAV}, year = {2022}, address = { Haifa, Isreal}, abstract = {

Formally verifying smart contracts is important due to their immutable nature, usual open source licenses, and high financial incentives for exploits. Since 2019 the Ethereum Foundation{\textquoteright}s Solidity compiler ships with a model checker. The checker, called SolCMC, has two different reasoning engines and tracks closely the development of the Solidity language. We describe SolCMC{\textquoteright}s architecture and use from the perspective of developers of both smart contracts and tools for software verification, and show how to analyze nontrivial properties of real life contracts in a fully automated manner.

}, keywords = {SolCMC}, author = {Leonardo Alt and Martin Blicha and Antti E. J. Hyv{\"a}rinen and Natasha Sharygina} } @article {373, title = {A Solicitous Approach to Smart Contract Verification}, journal = {ACM Transactions on Privacy and Security}, year = {2022}, type = {Full-Length Research Paper}, url = {https://dl.acm.org/doi/10.1145/3564699}, author = {Rodrigo Otoni and Matteo Marescotti and Leonardo Alt and Patrick Eugster and Antti E. J. Hyv{\"a}rinen and Natasha Sharygina} } @conference {319, title = {Accurate Smart Contract Verification through Direct Modelling}, booktitle = {ISoLA 2020 - 9th International Symposium On Leveraging Applications of Formal Methods, Verification and Validation}, year = {2020}, publisher = {Springer International Publishing}, organization = {Springer International Publishing}, isbn = {978-3-030-61467-6}, doi = {doi.org/10.1007/978-3-030-61467-6_12}, url = {https://link.springer.com/chapter/10.1007\%2F978-3-030-61467-6_12}, author = {Matteo Marescotti and Rodrigo Otoni and Leonardo Alt and Patrick Eugster and Antti E. J. Hyv{\"a}rinen and Natasha Sharygina} } @conference {326, title = {Farkas-Based Tree Interpolation}, booktitle = {SAS 2020 - 27th Static Analysis Symposium}, year = {2020}, publisher = {Springer}, organization = {Springer}, address = {Online Conference}, url = {https://link.springer.com/chapter/10.1007\%2F978-3-030-65474-0_16}, author = {Sepideh Asadi and Martin Blicha and Antti Hyv{\"a}rinen and Grigory Fedyukovich and Natasha Sharygina} } @conference {322, title = {Incremental Verification by SMT-based Summary Repair}, booktitle = {20th conference on FORMAL METHODS in COMPUTER-AIDED DESIGN {\textendash} FMCAD 2020}, year = {2020}, publisher = {IEEE digital library, TU Wien Academic Press}, organization = {IEEE digital library, TU Wien Academic Press}, isbn = {978-3-85448-042-6}, url = {http://verify.inf.usi.ch/sites/default/files/upprover-fmcad20.pdf}, author = {Sepideh Asadi and Martin Blicha and Antti E. J. Hyv{\"a}rinen and Grigory Fedyukovich and Natasha Sharygina} } @article {351, title = {Exploiting partial variable assignment in interpolation-based model checking.}, journal = {Formal Methods in System Design}, year = {2019}, abstract = {

Craig interpolation has been successfully employed in symbolic program verification as a means of abstraction for sets of program states. In this article, we present the partial variable assignment interpolation system, an extension of the labeled interpolation system, enriched by partial variable assignments. It allows for both generation of smaller interpolants as well as for their faster computation. We present proofs of important properties of the interpolation system as well as a set of experiments proving its usefulness.

}, url = {https://link.springer.com/article/10.1007\%2Fs10703-019-00342-z}, author = {Pavel Jan{\v c}{\'\i}k and Jan Kofron and Leonardo Alt and Grigory Fedyukovich and Antti E. J. Hyv{\"a}rinen and Natasha Sharygina} } @conference {293, title = {Computing Exact Worst-Case Gas Consumption for Smart Contracts}, booktitle = {International Symposium on Leveraging Applications of Formal Methods ISoLA 2018: Leveraging Applications of Formal Methods, Verification and Validation. Industrial Practice }, year = {2018}, publisher = {Springer}, organization = {Springer}, address = {Cyprus}, abstract = {

The Ethereum platform is a public, distributed, blockchain-based database that is maintained by independent parties. A user interacts with Ethereum by writing programs and having miners execute them for a fee charged on-the-fly based on the complexity of the execution. The exact fee, measured in gas consumption, in general depends on the unknown Ethereum state, and predicting even its worst case is in principle undecidable. Uncertainty in gas consumption may result in inefficiency, loss of money, and, in extreme cases, in funds being locked for an indeterminate duration. This feasibility study presents two methods for determining the exact worst-case gas consumption of a bounded Ethereum execution using methods influenced by symbolic model checking. We give several concrete cases where gas consumption estimation is needed, and provide two approaches for determining gas consumption, one based on symbolically enumerating execution paths, and the other based on computing paths modularly based on the program structure.

}, doi = {doi.org/10.1007/978-3-030-03427-6_33}, url = {https://link.springer.com/chapter/10.1007\%2F978-3-030-03427-6_33}, author = {Matteo Marescotti and Martin Blicha and Antti E. J. Hyv{\"a}rinen and Sepideh Asadi 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 {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 {277, title = {Duality-Based Interpolation for Quantifier-Free Equalities and Uninterpreted Functions}, booktitle = {17th Conference on Formal Methods in Computer-Aided Design (FMCAD 2017) }, year = {2017}, publisher = {IEEE XPlore and ACM Digital Libraries}, organization = {IEEE XPlore and ACM Digital Libraries}, address = {TU Wien, Vienna, Austria,}, url = {http://www.cs.utexas.edu/users/hunt/FMCAD/FMCAD17/fmcad17_proceedings.pdf}, author = {Leonardo Alt and Antti Hyv{\"a}rinen and Sepideh Asadi 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} } @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} } @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} } @conference {248, title = {Flexible Interpolation for Efficient Model Checking}, booktitle = {MEMICS 2016}, year = {2016}, url = {http://verify.inf.usi.ch/sites/default/files/MEMICS2016.pdf}, author = {Antti E. J. Hyv{\"a}rinen and Leonardo Alt and Natasha Sharygina} } @conference {335, title = {OpenSMT2: An SMT Solver for Multi-Core and Cloud Computing}, year = {2016}, author = {Antti E. J. Hyv{\"a}rinen and Matteo Marescotti and Leonardo Alt and Natasha Sharygina} } @conference {234, title = {PVAIR: Partial Variable Assignment InterpolatoR}, booktitle = {FASE2016}, year = {2016}, url = {http://verify.inf.usi.ch/sites/default/files/main-2.pdf}, author = {Pavel Jan{\v c}{\'\i}k and Leonardo Alt and Grigory Fedyukovich and Antti E. J. Hyv{\"a}rinen and Jan Kofron and Natasha Sharygina} } @article {216, title = {Decision Procedures for Flat Array Properties}, journal = {J. Autom. Reasoning}, volume = {54}, year = {2015}, month = {04/2015}, pages = {352}, chapter = {327}, author = {Francesco Alberti and Ghilardi, S. and Natasha Sharygina} } @conference {221, title = {A new Acceleration-based Combination Framework for Array Properties}, booktitle = {FROCOS 2015}, year = {2015}, author = {Francesco Alberti and Silvio Ghilardi and Natasha Sharygina} } @conference {222, title = {A Proof-Sensitive Approach for Small Propositional Interpolants}, booktitle = {VSTTE 2015}, year = {2015}, url = {http://verify.inf.usi.ch/sites/default/files/main_0.pdf}, author = {Leonardo Alt and Grigory Fedyukovich and Antti E. J. Hyv{\"a}rinen and Natasha Sharygina} } @mastersthesis {219, title = {An SMT-based verification framework for software systems handling arrays}, volume = {PhD}, year = {2015}, month = {02/2015}, pages = {188}, school = {Universit{\`a} della Svizzera Italiana}, type = {Doctoral Dissertation}, address = {Lugano}, url = {http://www.falberti.it/thesis/phd.pdf}, author = {Francesco Alberti} } @conference {185, title = {Decision Procedures for Flat Array Properties}, booktitle = {TACAS}, year = {2014}, publisher = {Springer}, organization = {Springer}, address = {Grenoble, France}, abstract = {
We present new decidability results for quantified fragments\ of theories of arrays. Our decision procedures are fully declarative, parametric in the theories of indexes and elements and orthogonal with respect to known results. We also discuss applications to the analysis of\ programs handling arrays.
}, author = {Francesco Alberti and Ghilardi, S. and Natasha Sharygina} } @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 {194, title = {VERIGE: Verification with Invariant Generation Engine}, booktitle = {SPIN}, year = {2014}, publisher = {ACM}, organization = {ACM}, author = {Latorre, N. and Francesco Alberti and Natasha Sharygina} } @article {173, title = {Abstraction and Acceleration in SMT-based Model-Checking for Array Programs}, journal = {CoRR}, volume = {April 2013}, year = {2013}, author = {Francesco Alberti and Ghilardi, S. and Natasha Sharygina} } @conference {167, title = {Definability of Accelerated Relations in a Theory of Arrays and Its Applications}, booktitle = {Frontiers of Combining Systems}, year = {2013}, author = {Francesco Alberti and Ghilardi, S. 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 {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} }