| Title | : | Towards scalable fully automatic program verification |
| Speaker | : | Hari Govind V K (University of Waterloo, Canada) |
| Details | : | Tue, 28 Nov, 2023 11:00 AM @ SSB 334 |
| Abstract: | : | Formal verification is the rigorous process of mathematically demonstrating that code adheres to its specified requirements. A central challenge in 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. APV tools facilitate the 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 abstractions 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. |
