Seminars

View all Seminars  |  Download ICal for this event

Towards scalable fully automatic program verification

Series: Department Seminar

Speaker: Hari Govind V. K. Fourth-year Ph.D. student, University of Waterloo, Canada

Date/Time: Nov 23 11:30:00

Location: CSA Class (Room No. 252, First Floor)

Abstract:
Formal verification is the rigorous process of mathematically demonstrating that code adheres to its specified requirements. A central challenge in this formal verification is constructing loop invariants and function summaries capable of summarizing all possible code behaviors. However, manually devising these invariants can be a laborious task, often acting as a significant deterrent for those who are not experts in the field. This presentation delves into the realm of automatic program verification (APV) tools, which have the capacity to systematically generate these essential invariants without necessitating the involvement of a domain expert. This innovation serves as a catalyst for broader adoption of formal verification methods. Currently, the best method for APV is SMT-based infinite state model checking, especially based on the IC3 algorithm. In this talk, I explore two key struggles in such algorithms and our attempts to overcome them. The first problem is generalizing lemmas, learned locally while proving sub-goals, into an invariant of the whole system. We address the problem by coming up with a framework to generalize lemmas using lemmas learned previously. The second problem with such algorithms is that they get stuck in complicated code fragments. As a first step towards overcoming this, we add the capability to reason about uninterpreted functions in our algorithm. We implement our solutions in Spacer, the default model-checking engine inside Z3 -- an open-source SMT solver. Our solutions improve the performance of Spacer on a wide variety of benchmarks.

Speaker Bio:
Hari Govind is a fourth-year Ph.D. student advised by Arie Gurfinkel at the University of Waterloo, Canada. His primary research interest is in developing scalable tools for program verification. His practical contributions are in improving the Spacer CHC solver inside Microsofts Z3 SMT solver and is a regular contributer to Z3. To complement practice, he also works on theoretical aspects of program verification and formal methods. Hari Govind is a recipient of the Microsoft PhD Fellowship in 2021, and a Distinguished Paper award at CAV 2023.

Host Faculty: Prof. Deepak DSouza