Concurrent program verification with invariant-guided underapproximation

Sumanth, Prabhu S, Schrammel, Peter, Mandayam, Srivas, Tautschnig, Michael and Anand, Yeolekar (2017) Concurrent program verification with invariant-guided underapproximation. Published in: Automated Technology for Verification and Analysis. Springer (Accepted)

[img] PDF - Accepted Version
Restricted to SRO admin only

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
Q Science > QA Mathematics > QA0076 Computer software
Depositing User: Peter Schrammel
Date Deposited: 02 Aug 2017 09:21
Last Modified: 02 Aug 2017 09:21
URI: http://sro.sussex.ac.uk/id/eprint/69531

View download statistics for this item

📧 Request an update