Symbolic model checking of concurrent programs using partial orders and on-the-fly transactions

Vineet Kahlon, Aarti Gupta, Nishant Sinha

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

24 Scopus citations

Abstract

The state explosion problem is one of the core bottlenecks in the model checking of concurrent software. We show how to ameliorate the problem by combining the ability of partial order techniques to reduce the state space of the concurrent program with the power of symbolic model checking to explore large state spaces. Our new verification methodology involves translating the given concurrent program into a circuit-based model which gives us the flexibility to then employ any model checking technique of choice - either SAT or BDD-based - for verifying a broad range of linear time properties, not just safety. The reduction in the explored state-space is obtained by statically augmenting the symbolic encoding of the program by additional constraints. These constraints restrict the scheduler to choose from a minimal conditional stubborn set of transitions at each state. Another key contribution of the paper, is a new method for detecting transactions on-the-fly which takes into account patterns of lock acquisition and yields better reductions than existing methods which rely on a lockset based analysis. Moreover unlike existing techniques, identifying on-the-fly transactions does not require the program to follow a lock discipline in accessing shared variables. We have applied our techniques to the Daisy test bench and shown the existence of several bugs.

Original languageEnglish (US)
Title of host publicationComputer Aided Verification - 18th International Conference, CAV 2006, Proceedings
PublisherSpringer Verlag
Pages286-299
Number of pages14
ISBN (Print)354037406X, 9783540374060
DOIs
StatePublished - 2006
Event18th International Conference on Computer Aided Verification, CAV 2006 - Seattle, WA, United States
Duration: Aug 17 2006Aug 20 2006

Publication series

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

Other

Other18th International Conference on Computer Aided Verification, CAV 2006
Country/TerritoryUnited States
CitySeattle, WA
Period8/17/068/20/06

All Science Journal Classification (ASJC) codes

  • Theoretical Computer Science
  • General Computer Science

Fingerprint

Dive into the research topics of 'Symbolic model checking of concurrent programs using partial orders and on-the-fly transactions'. Together they form a unique fingerprint.

Cite this