In this tutorial we will present the challenges and progress in specifying and verifying systems software written in C using Satisfiability Modulo Theories (SMT) solvers. Reasoning about such programs require dealing with pointer arithmetic, type-unsafety and dynamic data structures such as lists. In this tutorial, we will be present the challenges faced in verifying real-life software such as device drivers and kernel components. We will report on the progress we have made in using SMT solvers to perform precise (few false alarms), automated (no proof scripts) and scalable (can be applied to modules with several thousands of lines) verification of such code bases. In particular, we will address the following:
Novel type-safety checker for C using SMT solvers.
Logic and decision procedure for the linked lists and restricted quantified facts using SMT solvers.
Call invariants: a new approach to the frame rule for precise interprocedural reasoning with SMT logics.
Intra-module inference: annotation inference for large modules guided by module invariants.
These ideas are implemented in a tool HAVOC (Heap Aware Verifier fOr C). The webpage (http://research.microsoft.com/projects/HAVOC/) will have links to most of relevant papers for the tutorial.