Software now dominates almost every aspect of our life: from wrist watches to the stock markets, and from thermostats to surgeons. And this proliferation is unlikely to slow down any time soon; in fact, it appears that we are merely witnessing the very beginning of the software revolution. Society is ever more reliant on highly complex and interconnected software systems, and this has made software safety, security, and privacy a first-class societal concern.
To formally and mathematically reason about complex software systems, automated verification and program analysis techniques have proven powerful over the past decade, thanks to a plethora of advances in the area. However, most non-trivial programs and correctness properties of interest remain out of reach for automated verification techniques. The project investigates new automated software verification techniques and tools, that are more efficient and applicable to a wider range of programs and properties. Specifically, the project develops novel techniques for computing Craig interpolants, which are logical means for synthesizing proofs of correctness. The emphasis is on exploring the question of computing optimal interpolants---the simplest possible ones. The work is motivated by the observation that simpler interpolants are more likely to generalize to a proof of correctness. The goal of the project is to develop an algorithmic foundation for efficient verification of complex programs and correctness properties, thus expanding the applicability of formal verification techniques.
