Don't sweat the small stuff
David Greenaway, Japheth Lim, June Andronick, Gerwin Klein · 2014
We present an approach for automatically generating provably correct abstractions from C source code that are useful for practical implementation verification. The abstractions are easier for a human verification engineer to reason about than the implementation and increase the productivity of interactive code proof. We guarantee soundness by automatically generating proofs that the abstractions are correct.