Efficient modeling of concurrent systems in BMC

Malay K. Ganai, Aarti Gupta

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

24 Scopus citations


We present an efficient method for modeling multi-threaded concurrent systems with shared variables and locks in Bounded Model Checking (BMC), and use it to improve the detection of safety properties such as data races. Previous approaches based on synchronous modeling of interleaving semantics do not scale up well due to the inherent asynchronism in those models. Instead, in our approach, we first create independent (uncoupled) models for each individual thread in the system, then explicitly add additional synchronization variables and constraints, incrementally, and only where such synchronization is needed to guarantee the (chosen) concurrency semantics (based on sequential consistency). We describe our modeling in detail and report verification results to demonstrate the efficacy of our approach on a complex case study.

Original languageEnglish (US)
Title of host publicationModel Checking Software - 15th International SPIN Workshop, Proceedings
Number of pages20
StatePublished - 2008
Event15th International SPIN Workshop on Model Checking of Software, SPIN 2008 - Los Angeles, CA, United States
Duration: Aug 10 2008Aug 12 2008

Publication series

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


Other15th International SPIN Workshop on Model Checking of Software, SPIN 2008
Country/TerritoryUnited States
CityLos Angeles, CA

All Science Journal Classification (ASJC) codes

  • Theoretical Computer Science
  • General Computer Science


Dive into the research topics of 'Efficient modeling of concurrent systems in BMC'. Together they form a unique fingerprint.

Cite this