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 RepairSepideh Asadi, Martin Blicha, Antti E. J. Hyvärinen, Grigory Fedyukovich, Natasha Sharygina, FMCAD 2020: 77-82
  2. Farkas-Based Tree InterpolationSepideh 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-InductionMartin Blicha, Antti E. J. Hyvärinen, Matteo Marescotti, Natasha Sharygina, VMCAI 2020: 270-292
  4. Decomposing Farkas InterpolantsMartin Blicha, Antti E. J. Hyvärinen, Jan Kofron, Natasha Sharygina, TACAS (1) 2019: 3-20
  5. Sepideh Asadi, Martin Blicha, Grigory Fedyukovich, Antti E. J. Hyvärinen, Karine Even-Mendoza, Natasha Sharygina, Hana Chockler, LPAR 2018: 56-75
  6. Lookahead-Based SMT SolvingAntti E. J. Hyvärinen, Matteo Marescotti, Parvin Sadigova, Hana Chockler, Natasha Sharygina, LPAR 2018: 418-434
  7. SMTS: Distributed, Visualized Constraint SolvingMatteo Marescotti, Antti E. J. Hyvärinen, Natasha Sharygina, LPAR 2018: 534-542
  8. Duality-based interpolation for quantifier-free equalities and uninterpreted functionsLeonardo Alt, Antti Eero Johannes Hyvärinen, Sepideh Asadi, Natasha Sharygina, FMCAD 2017: 39-46
  9. LRA Interpolants from No Man's LandLeonardo Alt, Antti E. J. Hyvärinen, Natasha Sharygina, Haifa Verification Conference 2017: 195-210
  10. Theory Refinement for Program VerificationAntti E. J. Hyvärinen, Sepideh Asadi, Karine Even-Mendoza, Grigory Fedyukovich, Hana Chockler, Natasha Sharygina, SAT 2017: 347-363
  11. HiFrog: SMT-based Function Summarization for Software VerificationLeonardo Alt, Sepideh Asadi, Hana Chockler, Karine Even-Mendoza, Grigory Fedyukovich, Antti E. J. Hyvärinen, Natasha Sharygina, TACAS (2) 2017: 207-213
  12. Clause Sharing and Partitioning for Cloud-Based SMT SolvingMatteo Marescotti, Antti E. J. Hyvärinen, Natasha Sharygina, ATVA 2016: 428-443
  13. PVAIR: Partial Variable Assignment InterpolatoRPavel Jancík, Leonardo Alt, Grigory Fedyukovich, Antti E. J. Hyvärinen, Jan Kofron, Natasha Sharygina, FASE 2016: 419-434
  14. OpenSMT2: An SMT Solver for Multi-core and Cloud ComputingAntti E. J. Hyvärinen, Matteo Marescotti, Leonardo Alt, Natasha Sharygina, SAT 2016: 547-553
  15. Symbolic Detection of Assertion Dependencies for Bounded Model CheckingGrigory Fedyukovich, Andrea Callia D'Iddio, Antti E. J. Hyvärinen, Natasha Sharygina, FASE 2015: 186-201
  16. Flexible Interpolation for Efficient Model CheckingAntti E. J. Hyvärinen, Leonardo Alt, Natasha Sharygina, MEMICS 2015: 11-22
  17. Search-Space Partitioning for Parallelizing SMT SolversAntti E. J. Hyvärinen, Matteo Marescotti, Natasha Sharygina, SAT 2015: 369-386
  18. A Proof-Sensitive Approach for Small Propositional InterpolantsLeonardo Alt, Grigory Fedyukovich, Antti E. J. Hyvärinen, Natasha Sharygina, VSTTE 2015: 1-18
  19. Optimizing Function Summaries Through Interpolation. Validation of Evolving Software 2015Simone Fulvio Rollini, Leonardo Alt, Grigory Fedyukovich, Antti Eero Johannes Hyvärinen, Natasha Sharygina, Validation of Evolving Software 2015: 73-82
  20. PeRIPLO: A Framework for Producing Effective Interpolants in SAT-Based Software VerificationSimone Fulvio Rollini, Leonardo Alt, Grigory Fedyukovich, Antti Eero Johannes Hyvärinen, Natasha Sharygina, LPAR 2013: 683-693
  21. A Scalable Decision Procedure for Fixed-Width Bit-VectorsBruttomesso, R.; Sharygina, N. , International Conference of Computer Aided Design (ICCAD), San Jose (CA), ACM (2009)
  22. 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)
  23. An Efficient and Flexible Approach to Resolution Proof ReductionRollini, S.F.; Bruttomesso, R.; Sharygina, N. , Haifa Verification Conference (HVC), Haifa, Israel, Springer (2010)
  24. Flexible Interpolation with Local Proof TransformationsBruttomesso, R.; Rollini, S.F.; Sharygina, N.; Tsitovich, A. , International Conference of Computer Aided Design (ICCAD), San Jose, USA, IEEE Computer Society (2010)