Speaker: Aws Albarghouthi

Title: From Bounded to Unbounded Proofs of Correctness

Abstract: Automatically proving correctness of software systems is a fundamental problem that has never seemed more important, given the increasing complexity of software systems and our absolute reliance on them. In this talk, I will describe generic, automated, push-button techniques for verifying safety of software systems, that is, proving that every execution of a program does not cause a crash (e.g., via division by zero) and satisfies intended functionality (e.g., programmer-supplied assertions). Since a program can have infinitely many possible executions, verifying each execution separately is impossible. Instead, I focus on examining a small number of program executions and using Craig interpolation to devise hypotheses explaining why the whole program might be safe. I will present new techniques for computing "good" hypotheses (interpolants) and discuss our success with verifying (and finding bugs in) large C programs, including Linux device drivers.

Bio: Aws Albarghouthi is a graduating PhD candidate at the University of Toronto, where he works with Marsha Chechik. Aws's overarching research goal is ensuring correctness, reliability, and security of software systems by arming developers with efficient tools and techniques for reasoning about their programs. His research has contributed to the areas of verification and program analysis, automated theorem proving, as well as program synthesis. Notably, his automated verification tool UFO won the largest number of verification categories in the recent International Software Verification Competition (SV-COMP'13).