Software Engineering Seminar: Aws Albarghouthi, University of Toronto

Event Details
  • Date/Time:
    • Monday November 25, 2013
      2:00 pm
  • Location: Klaus 1116W
  • Phone:
  • URL:
  • Email:
  • Fee(s):
  • Extras:


Summary Sentence: No summary sentence submitted.

Full Summary: No summary paragraph submitted.

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).

Additional Information

In Campus Calendar

College of Computing, School of Computer Science

Invited Audience
Undergraduate students, Faculty/Staff, Graduate students
No keywords were submitted.
  • Created By: Elizabeth Ndongi
  • Workflow Status: Published
  • Created On: Nov 11, 2013 - 7:12am
  • Last Updated: Apr 13, 2017 - 5:23pm