Due to the ubiquity of software and the increasingly disruptive nature of program bugs, techniques for guaranteeing software reliability are more important now than ever before. This project studies program verification techniques that achieve the right trade-off between expressiveness and automation, thereby allowing the verification of a diverse class of software. The key idea is to use abductive reasoning to automate the correctness proof as much as possible by automatically synthesizing lemmas needed in a compositional proof. Another key idea is to automatically diagnose failed proof attempts and provide constructive feedback to users.
The broader impact of the project is to enable mostly-automated, user-friendly verification of interesting properties that are too hard to prove using traditional deductive verifiers but beyond the reach of fully-automated program analyzers. Another important goal is to uncover deeper and more subtle software defects than those that can be identified using testing and program analysis technology today.
