Verification of concurrent programs using trace abstraction refinement

Franck Cassez*, Frowin Ziegler

*Corresponding author for this work

Research output: Chapter in Book/Report/Conference proceedingConference proceeding contribution

4 Citations (Scopus)

Abstract

Verifying concurrent programs is notoriously hard due to the state explosion problem: (1) the data state space can be very large as the variables can range over very large sets, and (2) the control state space is the Cartesian product of the control state space of the concurrent components and thus grows exponentially in the number of components. On the one hand, the most successful approaches to address the control state explosion problem are based on assume-guarantee reasoning or model checking coupled with partial order reduction. On the other hand, the most successful techniques to address the data space explosion problem for sequential programs verification are based on the abstraction/refinement paradigm which consists in refining an abstract over-approximation of a program via predicate refinement. In this paper, we show that we can combine partial order reduction techniques with trace abstraction refinement. We apply our approach to standard benchmarks and show that it matches current state-of-the-art analysis techniques.

Original languageEnglish
Title of host publicationLogic for Programming, Artificial Intelligence, and Reasoning
Subtitle of host publication20th International Conference, LPAR-20 2015, Suva, Fiji, November 24-28, 2015, Proceedings
EditorsMartin Davis, Ansgar Fehnker, Annabelle McIver, Andrei Voronkov
Place of PublicationHeidelberg
PublisherSpringer, Springer Nature
Pages233-248
Number of pages16
ISBN (Electronic)9783662488997
ISBN (Print)9783662488980
DOIs
Publication statusPublished - 2015
Event20th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning, LPAR 2015 - Suva, Fiji
Duration: 24 Nov 201528 Nov 2015

Publication series

NameLecture Notes in Computer Science
PublisherSpringer Berlin Heidelberg
Volume9450
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Other

Other20th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning, LPAR 2015
CountryFiji
CitySuva
Period24/11/1528/11/15

Fingerprint Dive into the research topics of 'Verification of concurrent programs using trace abstraction refinement'. Together they form a unique fingerprint.

Cite this