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