Effective and flexible SMT-streamlined software model checking

Staff - Faculty of Informatics

Date: 6 April 2023 / 15:00 - 18:00

USI East Campus

You are cordially invited to attend the PhD Dissertation Defence of Sepideh Asadi on Thursday 6 April 2023 at 15:00 on Teams.

Formal verification by model checking is an award-winning (Turing award, 2007) technology to verify systems exhaustively and automatically in order to increase the degree of confidence that a program would perform correctly. Symbolic verification techniques such as bounded model checking (BMC) supported by highly efficient Boolean satisfiability (SAT) solvers have advanced the state of the art in model checking substantially. Nevertheless, scalability issues persist in these techniques due to the state-space explosion problem. The goal of this thesis is to address such scalability issues of model checking of software. We base the proposed solutions on Satisfiability Modulo Theories (SMT) as a logical representation of programs. Although SMT reasoning framework is one of the most successful approaches to verifying software in a scalable way, it poses new challenges to verification. The main issue of SMT is that it offers little direct support for adapting the constraint language to the task at hand. Another issue with SMT encoding of programs is that the light-weight theories are often imprecise. This means if a program is encoded in SMT, it may not be a ready-to-use solution for verification; it would require various (sometimes major) tuning to find a level of abstraction suitable for efficient symbolic model checking. This thesis addresses such challenges and trade-offs. This thesis draws together a range of techniques and combines them in a novel way so that not only improves scalability but also enables flexibility by allowing different levels of SMT abstractions. A new verification technique is proposed based on SMT-based model checking that verifies programs incrementally, reusing the computational history of a program, namely function summaries. In addition to the provided reusability supported by the incremental approach, the technique allows adjusting the precision with different levels of SMT encodings. Overall, this thesis extends the state of the art by (i) designing a verification technique that interleaves the SMT reasoning with model checking, (ii) introducing an incremental verification approach where it reuses the computation history of related verification tasks, and (iii) exploring the trade-offs between program encoding {\em precision} and solving {\em efficiency} using a novel theory-aware abstraction refinement approach that models a program using the lightest theories and strengthens locally on demand if the precision is not sufficient for verification needs. This thesis considers two application domains: (i) efficiently verifying a single program with a sequence of safety properties (i.e., no assertion failure in the program), and (ii) incrementally verifying program revisions with respect to the same safety property. The effectiveness of the proposed approaches has been validated by developing two new SMT-based model checking frameworks: HiFrog and UpProver. These frameworks have been integrated into the interpolating SMT solver OpenSMT. This thesis presents real-world model checking experiments using the proposed verification tools, demonstrating the viability and strengths of the techniques.

Dissertation Committee:

  • Prof. Natasha Sharygina, Università della Svizzera italiana, Switzerland (Research Advisor)
  • Prof. Kai Hormann, Università della Svizzera italiana, Switzerland (Internal Member)
  • Prof. Evanthia Papadopoulou, Università della Svizzera italiana, Switzerland (Internal Member)
  • Prof. Ken McMillan, The University of Texas at Austin, USA (External Member)
  • Prof. Roberto Sebastiani, University of Trento (External Member)