Symbolic pruning of concurrent program executions

Chao Wang, Swarat Chaudhuri, Aarti Gupta, Yu Yang

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

35 Scopus citations

Abstract

We propose a new algorithm for verifying concurrent programs, which uses concrete executions to partition the program into a set of lean partitions called concurrent trace programs (CTPs), and symbolically verifies each CTP using a satisfiability solver. A CTP, derived from a concrete execution trace, implicitly captures all permutations of the trace that also respect the control flow of the program. We show that a CTP, viewed as a coarser equivalence class than the popular (Mazurkiewicz) trace equivalence in partial order reduction (POR) literature, leads to more effective pruning of the search space during model checking. While classic POR can prune away redundant interleavings within each trace equivalence class, the pruning in POR is not property driven. We use symbolic methods to achieve property-driven pruning. The effort of exploration is distributed between a symbolic component (verification of a particular CTP) and an enumerative component (exploration of the space of CTPs). We show that the proposed method facilitates more powerful pruning of the search space during the enumerative exploration.

Original languageEnglish (US)
Title of host publicationESEC-FSE'09 - Proceedings of the Joint 12th European Software Engineering Conference and 17th ACM SIGSOFT Symposium on the Foundations of Software Engineering
Pages23-32
Number of pages10
DOIs
StatePublished - Dec 1 2009
Externally publishedYes
EventJoint 12th European Software Engineering Conference and 17th ACM SIGSOFT Symposium on the Foundations of Software Engineering, ESEC-FSE'09 - Amsterdam, Netherlands
Duration: Aug 24 2009Aug 28 2009

Publication series

NameESEC-FSE'09 - Proceedings of the Joint 12th European Software Engineering Conference and 17th ACM SIGSOFT Symposium on the Foundations of Software Engineering

Other

OtherJoint 12th European Software Engineering Conference and 17th ACM SIGSOFT Symposium on the Foundations of Software Engineering, ESEC-FSE'09
CountryNetherlands
CityAmsterdam
Period8/24/098/28/09

All Science Journal Classification (ASJC) codes

  • Computational Theory and Mathematics
  • Software

Keywords

  • Concurrency
  • Partial order reduction
  • Pruning
  • SAT

Fingerprint Dive into the research topics of 'Symbolic pruning of concurrent program executions'. Together they form a unique fingerprint.

  • Cite this

    Wang, C., Chaudhuri, S., Gupta, A., & Yang, Y. (2009). Symbolic pruning of concurrent program executions. In ESEC-FSE'09 - Proceedings of the Joint 12th European Software Engineering Conference and 17th ACM SIGSOFT Symposium on the Foundations of Software Engineering (pp. 23-32). (ESEC-FSE'09 - Proceedings of the Joint 12th European Software Engineering Conference and 17th ACM SIGSOFT Symposium on the Foundations of Software Engineering). https://doi.org/10.1145/1595696.1595702