Deductive program verification tools based on Floyd-Hoare logic prove program safety by generating verification conditions (VCs) and proving the validity of these VCs using an automated theorem prover. While this process is mostly automatic, deductive verifiers typically rely on program annotations (e.g., loop invariants) to generate verification conditions. In this talk, we will describe how abductive reasoning can be used to automatically infer relevant program annotations. Specifically, we will talk about logical abduction and how it can be combined with backtracking search to automatically generate loop invariants that are necessary for proving program safety.

Isil Dillig is an Associate Professor of Computer Science at the University of Texas at Austin where she leads the UToPiA research group. Her main research area is programming languages, with a specific emphasis on static analysis, verification, and program synthesis. The techniques developed by her group aim to make software systems more reliable, secure, and easier to build in a robust way. Dr. Dillig is a Sloan Fellow and a recipient of the NSF CAREER award. She obtained all her degrees (BS, MS, and PhD) from Stanford University.