Sep 28, 2015
Nadia Polikarpova: A Fully Verified Container Library
The comprehensive functionality and flexible design of general-purpose container libraries pose nontrivial challenges to formal verification. In this talk I will present our experience using the AutoProof program verifier to prove full functional correctness of a realistic container library. I will discuss the key ingredients of AutoProof’s methodology, which made the verification possible with moderate annotation overhead and good performance.