@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 {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} } @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} } @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} }