Tehran Institute for Advanced Studies (TEIAS)

/ SMT-based Software Model Checking __ Sepideh Asadi


SMT-based Software Model Checking

Sepideh Asadi

August 04, 2021
(13 Mordad, 1400)



This Talk is online

Registration Deadline

August 03, 2021

You may need a VPN to start the talk.


Sepideh Asadi

Ph.D. student at USI Lugano Formal Verification and Security Lab


Formal verification using model checking and related logic-based reasoning is a popular though highly non-trivial approach when it comes to reasoning about software correctness. It often requires ingenuity both from the verification tools developers and their users. In this talk, she will present an approach which interleaves SMT-based reasoning with the basic model checking tasks thus enabling scalable verification and simplifying the use of the tools for non-experts. The integrated development of a model checker backed up by the efficient SMT solver is the key; SMT solving is used not only as a computational engine of reasoning as in most existing tools, but also for system modeling and the automated adjustment of its precision necessary for scalable verification. She will illustrate the integrated approach using function-summarization-based model checker using SMT as the modeling and summarization language. The presentation will be complemented by a demo which will demonstrate the practical impact the different SMT precisions have on program verification.


Sepideh Asadi is a final-year Ph.D. student at Formal Verification and Security Lab of University of Lugano, Switzerland, under the supervision of Prof. Natasha Sharygina. She completed her M.Sc. at Iran University of Science and Technology (2013). The main focus of her research is in Software Verification with a specific focus on Symbolic Model Checking, Incremental Verification, and SMT solving. She has contributed to developing of UpProver, a bounded model checker for incrementally verifying software revisions. She has also contributed to the design of HiFrog, an SMT-based BMC with theory refinement algorithm.