paper.pdf (262.43 kB)
Concurrent program verification with invariant-guided underapproximation
conference contribution
posted on 2023-06-09, 07:30 authored by Sumanth Prabhu, Peter Schrammel, Srivas Mandayam, Michael Tautschnig, Yeolekar AnandAutomatic 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.
History
Publication status
- Published
File Version
- Accepted version
Journal
Automated Technology for Verification and AnalysisPublisher
SpringerExternal DOI
Page range
241-248Event name
Fifteenth International Symposium on Automated Technology for Verification and AnalysisEvent location
Pune, IndiaEvent type
conferenceEvent date
3-6 October 2017ISBN
9783319681665Series
Lecture notes in computer scienceDepartment affiliated with
- Informatics Publications
Full text available
- Yes
Peer reviewed?
- Yes
Legacy Posted Date
2017-08-02First Open Access (FOA) Date
2017-10-16First Compliant Deposit (FCD) Date
2017-08-01Usage metrics
Categories
No categories selectedLicence
Exports
RefWorks
BibTeX
Ref. manager
Endnote
DataCite
NLM
DC