Don't sweat the small stuff: formal verification of C code without the pain
PLDI, pp. 429-439, 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 soundnes...More
PPT (Upload PPT)