2:00PM, Lecture Hall 1
M.Sc Thesis Defence
Concurrent Program Verification Using Invariants-guided Under-approximations: A Method and Tool
Sumanth Prabhu
Chennai Mathematical Institute.
28-04-17

---

Abstract

Automatic verification of concurrent programs written in low level languages like ANSI-C or C11 is an important task as multi-core architecture is gaining widespread adoption. Formal verification, although very valuable for this domain, rapidly runs into the state-explosion problem due to multiple thread interleavings. Recently, several people have looked at using Bounded Model Checking (BMC) for this purpose by using unwinding depth (CBMC), number of context-switches (KISS), or number of writes (MuCseq, Conseq) as a bounding parameter to restrict search space and manage complexity. Even so, these BMC techniques do not scale very far in practice. In this work, we develop a method to further restrict proof search-space for these BMC techniques using under-approximations of possible thread interleavings and lazy need-based refinement of the approximation. The novel contribution of our method is that our under-approximation is guided by likely data-flow invariants mined from dynamic analysis and our refinement is based on proof-based learning. We have implemented our method in a prototype tool Initial experiments on bench-mark examples show potential performance benefit.