This talk will introduce the basic principles underlying deductive program verifiers, which are frequently used to prove important functional correctness properties of software. While deductive verifiers are completely push-button for loop- and recursion-free code, they traditionally require a human to provide annotations in the form of loop invariants and method contracts for arbitrary code. After introducing the basic principles of program verification, the talk will then introduce the concept of abductive reasoning and will describe how abduction can be used to automatically infer the kinds of annotations required by deductive program verifiers. The talk will be a mix of basic background knowledge on program verification as well as recent research on the use of abductive reasoning for proof automation.

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.