From SMT Solvers to Verifiers

Presented as part of the 2013 HCSS conference.

ABSTRACT

We describe automated techniques for proving program safety, that is, proving that every execution of a program does not cause a crash (e.g., via division by zero) and satisfies intended functionality (e.g., a programmer-supplied assertion). The core idea underlying our approach is that by examining a bounded version of the program, with a finite number of execution paths, we can generalize the proof of correctness to the whole program. Our generalization capitalizes on advances in SMT solving for path enumeration, novel interpolant generation techniques for DAGs of formulas, and a tight integration with abstract domains in order to improve interpolant "quality". Our approach forms the basis of UFO, a C verifier we built in LLVM, that has recently won numerous categories in the 2013 Competition on Software Verification (SV-COMP).