University of Sussex
Browse
paper.pdf (262.43 kB)

Concurrent program verification with invariant-guided underapproximation

Download (262.43 kB)
conference contribution
posted on 2023-06-09, 07:30 authored by Sumanth Prabhu, Peter Schrammel, Srivas Mandayam, Michael Tautschnig, Yeolekar Anand
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.

History

Publication status

  • Published

File Version

  • Accepted version

Journal

Automated Technology for Verification and Analysis

Publisher

Springer

Page range

241-248

Event name

Fifteenth International Symposium on Automated Technology for Verification and Analysis

Event location

Pune, India

Event type

conference

Event date

3-6 October 2017

ISBN

9783319681665

Series

Lecture notes in computer science

Department affiliated with

  • Informatics Publications

Full text available

  • Yes

Peer reviewed?

  • Yes

Legacy Posted Date

2017-08-02

First Open Access (FOA) Date

2017-10-16

First Compliant Deposit (FCD) Date

2017-08-01

Usage metrics

    University of Sussex (Publications)

    Categories

    No categories selected

    Exports

    RefWorks
    BibTeX
    Ref. manager
    Endnote
    DataCite
    NLM
    DC