Don't sweat the small stuff: formal verification of C code without the pain

PLDI, pp. 429-439, 2014.

Cited by: 37|Bibtex|Views77|DOI:https://doi.org/10.1145/2594291.2594296
EI
Other Links: dl.acm.org|dblp.uni-trier.de|academic.microsoft.com

Abstract:

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

Code:

Data:

Full Text
Your rating :
0

 

Tags
Comments