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: | |
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