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

PDF - Accepted Version Download (268kB)

Abstract

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:	Publisher
Depositing User:	Peter Schrammel
Date Deposited:	02 Aug 2017 09:21
Last Modified:	03 Nov 2017 12:30
URI:	http://srodev.sussex.ac.uk/id/eprint/69531

View download statistics for this item

📧 Request an update