*********************************
There is now a CONTENT FREEZE for Mercury while we switch to a new platform. It began on Friday, March 10 at 6pm and will end on Wednesday, March 15 at noon. No new content can be created during this time, but all material in the system as of the beginning of the freeze will be migrated to the new platform, including users and groups. Functionally the new site is identical to the old one. webteam@gatech.edu
*********************************
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).
