# Formal Verification via Boolean and Theory Reasoning (SMT)

State-of-the-art techniques used in Formal Verification ultimately rely on the expression of properties (of the system to verify) in terms of languages that can be easily understood and processed by automatic tools.

One of the most used languages nowadays is Boolean logic at the propositional level; its associated decision problem, SAT, has been extensively studied in the latest decade. The reason for the success of SAT is twofold: (i) the simplicity and flexibility of propositional logic and (ii) the availability of extremely efficient and robust tools for deciding SAT (SAT-Solvers).

Satisfiability Modulo Theories (SMT for short) is a novel paradigm that supports the encoding of formal properties at a higher level of expressiveness than Booleans. Beside propositional logic, the language (that comes with different flavors) allows for the expression of other useful theories, such as linear arithmetic, arrays and bit-vectors. The language of SMT can be therefore used to replace simple Boolean logic or to express properties that cannot be encoded into SAT.

As for SAT, the need for automatic tools in formal verification led to the development of SMT-Solvers. SMT-Solvers are based on the same engine of SAT-Solvers, and they integrate theory reasoning and Boolean reasoning in an elegant and effective framework.

The first goal of the project consists in the development of new efficient decision procedures for SMT, and in the application of SMT instead of SAT in the domain of Formal Verification.

From the point of view of Formal Verification, the problem of determining if a system respects a certain property can be effectively translated into verifying the satisfiability of a logic formula encoding both the system and the property.

In case the formula under examination does not admit a model, SMT-Solvers can be easily instructed to produce a certificate in the form of a propositional resolution proof of unsatisfiability, by keeping track of the steps performed while looking for such a model.

A remarkable application of resolution proofs within the field of Model Checking is related to the generation of mathematical objects called interpolants. We can think of a system as an encoding into the logic of a graph characterized by a set of initial states, a set of failure states (where the property of interest is violated) and a transition relation, which describes the connections among states. Interpolation can be then used as an alternative to the expensive exact computation, step by step, of the sets of states which are reachable from the initial ones.

State-of-the-art procedures for interpolation in SMT generate interpolants basing on the structure of resolution proofs of unsatisfiability. An important aspect of the project is the investigation of transformation techniques for resolution proofs, aimed at reducing the size and modifying the topology, in order to obtain interpolants of better quality in several theories of interest.

Our current results include papers [1][2][3][4], and the OpenSMT tool, the SMT-solving framework we use for both research and experimentation.

### Publications:

1. Incremental Verification by SMT-based Summary Repair Sepideh Asadi, Martin Blicha, Antti E. J. Hyvärinen, Grigory Fedyukovich, Natasha Sharygina, FMCAD 2020: 77-82
2. Farkas-Based Tree Interpolation Sepideh Asadi, Martin Blicha, Antti E. J. Hyvärinen, Grigory Fedyukovich, Natasha Sharygina, SAS 2020: 357-379
3. A Cooperative Parallelization Approach for Property-Directed k-Induction Martin Blicha, Antti E. J. Hyvärinen, Matteo Marescotti, Natasha Sharygina, VMCAI 2020: 270-292
4. Decomposing Farkas Interpolants Martin Blicha, Antti E. J. Hyvärinen, Jan Kofron, Natasha Sharygina, TACAS (1) 2019: 3-20
5. Lookahead-Based SMT Solving Antti E. J. Hyvärinen, Matteo Marescotti, Parvin Sadigova, Hana Chockler, Natasha Sharygina, LPAR 2018: 418-434
6. SMTS: Distributed, Visualized Constraint Solving Matteo Marescotti, Antti E. J. Hyvärinen, Natasha Sharygina, LPAR 2018: 534-542
7. Duality-based interpolation for quantifier-free equalities and uninterpreted functions Leonardo Alt, Antti Eero Johannes Hyvärinen, Sepideh Asadi, Natasha Sharygina, FMCAD 2017: 39-46
8. LRA Interpolants from No Man's LandLeonardo Alt, Antti E. J. Hyvärinen, Natasha Sharygina, Haifa Verification Conference 2017: 195-210
9. Theory Refinement for Program Verification Antti E. J. Hyvärinen, Sepideh Asadi, Karine Even-Mendoza, Grigory Fedyukovich, Hana Chockler, Natasha Sharygina, SAT 2017: 347-363
10. HiFrog: SMT-based Function Summarization for Software Verification Leonardo Alt, Sepideh Asadi, Hana Chockler, Karine Even-Mendoza, Grigory Fedyukovich, Antti E. J. Hyvärinen, Natasha Sharygina, TACAS (2) 2017: 207-213
11. Clause Sharing and Partitioning for Cloud-Based SMT Solving Matteo Marescotti, Antti E. J. Hyvärinen, Natasha Sharygina, ATVA 2016: 428-443
12. PVAIR: Partial Variable Assignment InterpolatoR Pavel Jancík, Leonardo Alt, Grigory Fedyukovich, Antti E. J. Hyvärinen, Jan Kofron, Natasha Sharygina, FASE 2016: 419-434
13. OpenSMT2: An SMT Solver for Multi-core and Cloud Computing Antti E. J. Hyvärinen, Matteo Marescotti, Leonardo Alt, Natasha Sharygina, SAT 2016: 547-553
14. Symbolic Detection of Assertion Dependencies for Bounded Model Checking Grigory Fedyukovich, Andrea Callia D'Iddio, Antti E. J. Hyvärinen, Natasha Sharygina, FASE 2015: 186-201
15. Flexible Interpolation for Efficient Model Checking Antti E. J. Hyvärinen, Leonardo Alt, Natasha Sharygina, MEMICS 2015: 11-22
16. Search-Space Partitioning for Parallelizing SMT Solvers Antti E. J. Hyvärinen, Matteo Marescotti, Natasha Sharygina, SAT 2015: 369-386
17. A Proof-Sensitive Approach for Small Propositional Interpolants Leonardo Alt, Grigory Fedyukovich, Antti E. J. Hyvärinen, Natasha Sharygina, VSTTE 2015: 1-18
18. Optimizing Function Summaries Through Interpolation. Validation of Evolving Software 2015 Simone Fulvio Rollini, Leonardo Alt, Grigory Fedyukovich, Antti Eero Johannes Hyvärinen, Natasha Sharygina, Validation of Evolving Software 2015: 73-82
19. PeRIPLO: A Framework for Producing Effective Interpolants in SAT-Based Software Verification Simone Fulvio Rollini, Leonardo Alt, Grigory Fedyukovich, Antti Eero Johannes Hyvärinen, Natasha Sharygina, LPAR 2013: 683-693
20. A Scalable Decision Procedure for Fixed-Width Bit-Vectors Bruttomesso, R.; Sharygina, N. , International Conference of Computer Aided Design (ICCAD), San Jose (CA), ACM (2009)
21. An Extension of the Davis-Putnam Procedure and its Application to Preprocessing in SMT, Bruttomesso, R. , 7th International Workshop on Satisfiability Modulo Theories (SMT), Montreal, Canada, ACM (2009)
22. An Efficient and Flexible Approach to Resolution Proof Reduction Rollini, S.F.; Bruttomesso, R.; Sharygina, N. , Haifa Verification Conference (HVC), Haifa, Israel, Springer (2010)
23. Flexible Interpolation with Local Proof Transformations Bruttomesso, R.; Rollini, S.F.; Sharygina, N.; Tsitovich, A. , International Conference of Computer Aided Design (ICCAD), San Jose, USA, IEEE Computer Society (2010)