@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 {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 {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 {310, title = {A Cooperative Parallelization Approach for Property-Directed k-Induction}, booktitle = {VMCAI 2020 - 21st International Conference on Verification, Model Checking, and Abstract Interpretation}, year = {2020}, address = { New Orleans, USA, 19-25 January 2020}, doi = {10.1007/978-3-030-39322-9_13}, author = {Martin Blicha and Antti E. J. Hyv{\"a}rinen and Matteo Marescotti and Natasha Sharygina} } @mastersthesis {332, title = {Parallelization and modelling techniques for scalable SMT-based verification}, volume = {PhD}, year = {2020}, month = {01.12.2020}, school = {USI Lugano}, abstract = {

Software systems are increasingly involved in our daily life tasks, making their failures potentially damaging both in economic and human terms. As a result, proving the correctness of software is widely thought to be one of the most central challenges for computer science. Model checking is an award-winning (Turing award, 2007) technique for formally and automatically verifying systems, often capable to guarantee the correctness of non-trivial and practical programs. However, model checking is undecidable in the general case. Even when properly restricted to the decidable fragment, the algorithms face strong scalability issues preventing them to converge to the solution. The goal of this thesis is to address such scalability issues in two orthogonal ways. First, the design of parallel solving techniques that exploit the massive amount of computational power offered by distributed computing environments. Second, the design of a modelling technique for effective verification of the new emergent technology of smart contracts running on blockchain systems. The parallel solving research efforts consider both bounded and induction-based unbounded model checking, respectively achieved by instantiating multi-agent solving for the T-DPLL and IC3 algorithms. Multi-agent techniques leverage on the diversification and cooperation among sequential solvers executed in parallel. Diversification is achieved with different parallel search heuristics, and cooperation is performed with the exchange of information both during solving time and via upfront agreements. The effectivenesses of various multi-agent settings are empirically evaluated using the purpose-built multi-agent framework SMTS. Verification approaches for emerging technologies tend to either reuse tools for existing languages that often result in inefficient and even unsound models, or to apply generic techniques which typically require human intervention to succeed. This thesis provides a new direct modelling approach using constrained Horn clauses for the emerging technology of smart contracts. Such approach allows automatic solving exploiting the proposed efforts in improving inductive solvers scalability, and guarantees soundness for the safety proofs. Additionally, the smart-contracts-specific task of measuring the amount of computation needed to execute a transaction, i.e. gas consumption, is considered in this thesis proposing an algorithmic solution. The effectiveness of the modelling technique is empirically evaluated over smart contracts deployed in the Ethereum blockchain using an implementation inside the official compiler for the smart contracts language Solidity that relies on the IC3 algorithm.

}, url = {http://verify.inf.usi.ch/sites/default/files/phd_thesis_matteo_marescotti.pdf}, author = {Matteo Marescotti} } @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 {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 {300, title = {{SMTS:} Distributed, Visualized Constraint Solving}, booktitle = {{LPAR-22.} 22nd International Conference on Logic for Programming, Artificial Intelligence and Reasoning, Awassa, Ethiopia, 16-21 November 2018}, year = {2018}, author = {Matteo Marescotti and Antti E. J. Hyv{\"a}rinen and Natasha Sharygina} } @conference {250, title = {Clause Sharing and Partitioning for Cloud-Based SMT Solving}, booktitle = {ATVA 2016}, year = {2016}, url = {http://verify.inf.usi.ch/sites/default/files/ATVA2016.pdf}, author = {Matteo Marescotti and Antti E. J. Hyv{\"a}rinen and Natasha Sharygina} } @proceedings {246, title = {Combining parallel techniques for Cloud-Based SMT Solving}, year = {2016}, url = {http://verify.inf.usi.ch/sites/default/files/PhD-iFM2016.pdf}, author = {Matteo Marescotti} } @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 {232, title = {Search-Space Partitioning for Parallelizing SMT Solvers}, booktitle = {MEMICS2015}, year = {2015}, url = {http://verify.inf.usi.ch/sites/default/files/memics2015.pdf}, author = {Matteo Marescotti and Antti E. J. Hyv{\"a}rinen and Natasha Sharygina} } @conference {223, title = {Search-Space Partitioning for Parallelizing SMT Solvers}, booktitle = {SAT 2015}, year = {2015}, author = {Antti E. J. Hyv{\"a}rinen and Matteo Marescotti and Natasha Sharygina} } @conference {190, title = {Verification-Aided Regression Testing}, booktitle = {ISSTA}, year = {2014}, month = {06/2014}, abstract = {

In this paper we present Verification-Aided Regression Testing (VART), a novel extension of regression testing that uses model checking to increase the fault revealing capability of existing test suites. The key idea in VART is to extend the use of test case executions from the conventional direct fault discovery to the generation of behavioral properties specific to the upgrade, by (i) automatically producing properties that are proved to hold for the base version of a program, (ii) automatically identifying and checking on the upgraded program only the properties that, according to the developers{\textquoteright} intention, must be preserved by the upgrade, and (iii) reporting the faults and the corresponding counter-examples that are not revealed by the regression tests. Our empirical study on both open source and industrial software systems shows that VART automatically produces properties that increase the effectiveness of testing by automatically detecting faults unnoticed by the existing regression test suites.\ 

}, author = {Pastore, F. and Mariani, L. and Antti E. J. Hyv{\"a}rinen and Grigory Fedyukovich and Natasha Sharygina and Sehestedt, S. and Muhammad, A.} } @conference {165, title = {PINCETTE - Validating Changes and Upgrades in Networked Software}, booktitle = {17th European Conference on Software Maintenance and Reengineering}, year = {2013}, author = {Chockler, H. and Denaro, G. and Ling, M. and Grigory Fedyukovich and Antti E. J. Hyv{\"a}rinen and Mariani, L. and Muhammad, A. and Oriol, M. and Rajan, A. and Sery, O. and Natasha Sharygina and Tautschnig, M.} } @conference {159, title = {Using Cross-Entropy for Satisfiability}, booktitle = {ACM Symposium on Applied Computing (SAC)}, year = {2013}, author = {Chockler, H. and Ivrii, A. and Matsliah, A. and Rollini, S.F. and Natasha Sharygina} }