Verifying Evolving Software

In this project, we are addressing this challenge by developing and evaluating algorithms for propagating verification results through human- and machine-generated evolution. We build on the recent advancements in proof-based verification, regression verification, and upgrade checking [Albarghouthi 2013, Godlin 2013, Fedyukovich 2013, Sery 2012]. Our key insight is that current proof-based analysis techniques generate explicit proofs, also known as, verification certificates, (as inductive invariants in First Order Logic) that can be migrated across evolution boundaries.