University of Sussex
Browse
swarm-ASE2017.pdf (290.06 kB)

Parallel bug-finding in concurrent programs via reduced interleaving instances

Download (290.06 kB)
conference contribution
posted on 2023-06-09, 07:54 authored by Truc L Nguyen, Peter Schrammel, Bernd Fischer, Salvatore La Torre, Gennaro Parlato
Concurrency poses a major challenge for program verification, but it can also offer an opportunity to scale when subproblems can be analysed in parallel. We exploit this opportunity here and use a parametrizable code-to-code translation to generate a set of simpler program instances, each capturing a reduced set of the original program’s interleavings. These instances can then be checked independently in parallel. Our approach does not depend on the tool that is chosen for the final analysis, is compatible with weak memory models, and amplifies the effectiveness of existing tools, making them find bugs faster and with fewer resources. We use Lazy-CSeq as an off-the-shelf final verifier to demonstrate that our approach is able, already with a small number of cores, to find bugs in the hardest known concurrency benchmarks in a matter of minutes, whereas other dynamic and static tools fail to do so in hours.

History

Publication status

  • Published

File Version

  • Accepted version

Journal

Automated Software Engineering

ISSN

0928-8910

Publisher

Association for Computing Machinery

Page range

753-764

Event name

The 32nd IEEE/ACM International Conference on Automated Software Engineering

Event location

University of Illinois

Event type

conference

Event date

30th October - 3rd November

ISBN

9781538626849

Department affiliated with

  • Informatics Publications

Full text available

  • Yes

Peer reviewed?

  • Yes

Legacy Posted Date

2017-09-14

First Open Access (FOA) Date

2018-05-31

First Compliant Deposit (FCD) Date

2017-09-13

Usage metrics

    University of Sussex (Publications)

    Categories

    No categories selected

    Exports

    RefWorks
    BibTeX
    Ref. manager
    Endnote
    DataCite
    NLM
    DC