Concurrent program verification with invariant-guided underapproximation

Prabhu, Sumanth, Schrammel, Peter, Mandayam, Srivas, Tautschnig, Michael and Anand, Yeolekar (2017) Concurrent program verification with invariant-guided underapproximation. Fifteenth International Symposium on Automated Technology for Verification and Analysis, Pune, India, 3-6 October 2017. Published in: Automated Technology for Verification and Analysis. 241-248. Springer ISBN 9783319681665

[img] PDF - Accepted Version
Download (268kB)


Automatic verification of concurrent programs written in low-level languages like ANSI-C is an important task as multi-core architectures are gaining widespread adoption. Formal verification, although very valuable for this domain, rapidly runs into the state-explosion problem due to multiple thread interleavings. Recently, Bounded Model Checking (BMC) has been used for this purpose, which does not scale in practice. In this work, we develop a method to further constrain the search space for BMC techniques using underapproximations of data flow of shared memory and lazy demand-driven refinement of the approximation. A novel contribution of our method is that our underapproximation 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 benchmark examples show potential performance benefit.

Item Type: Conference Proceedings
Keywords: verification, concurrency, bounded model checking
Schools and Departments: School of Engineering and Informatics > Informatics
Subjects: Q Science > QA Mathematics > QA0075 Electronic computers. Computer science
Related URLs:
Depositing User: Peter Schrammel
Date Deposited: 02 Aug 2017 09:21
Last Modified: 03 Nov 2017 12:30

View download statistics for this item

📧 Request an update