Overview

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.