Monotonic partial order reduction: An optimal symbolic partial order reduction technique

Vineet Kahlon, Chao Wang, Aarti Gupta

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

63 Scopus citations

Abstract

We present a new technique called Monotonic Partial Order Reduction (MPOR) that effectively combines dynamic partial order reduction with symbolic state space exploration for model checking concurrent software. Our technique hinges on a new characterization of partial orders defined by computations of a concurrent program in terms of quasi-monotonic sequences of thread-ids. This characterization, which is of independent interest, can be used both for explicit or symbolic model checking. For symbolic model checking, MPOR works by adding constraints to allow automatic pruning of redundant interleavings in a SAT/SMT solver based search by restricting the interleavings explored to the set of quasi-monotonic sequences. Quasi-monotonicity guarantees both soundness (all necessary interleavings are explored) and optimality (no redundant interleaving is explored) and is, to the best of our knowledge, the only known optimal symbolic POR technique.

Original languageEnglish (US)
Title of host publicationComputer Aided Verification - 21st International Conference, CAV 2009, Proceedings
Pages398-413
Number of pages16
DOIs
StatePublished - Oct 27 2009
Externally publishedYes
Event21st International Conference on Computer Aided Verification, CAV 2009 - Grenoble, France
Duration: Jun 26 2009Jul 2 2009

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume5643 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Other

Other21st International Conference on Computer Aided Verification, CAV 2009
CountryFrance
CityGrenoble
Period6/26/097/2/09

All Science Journal Classification (ASJC) codes

  • Theoretical Computer Science
  • Computer Science(all)

Fingerprint Dive into the research topics of 'Monotonic partial order reduction: An optimal symbolic partial order reduction technique'. Together they form a unique fingerprint.

  • Cite this

    Kahlon, V., Wang, C., & Gupta, A. (2009). Monotonic partial order reduction: An optimal symbolic partial order reduction technique. In Computer Aided Verification - 21st International Conference, CAV 2009, Proceedings (pp. 398-413). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 5643 LNCS). https://doi.org/10.1007/978-3-642-02658-4_31