Compositionality entails sequentializability

Pranav Garg, P. Madhusudan

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

Abstract

We show that any concurrent program that is amenable to compositional reasoning can be effectively translated to a sequential program. More precisely, we give a reduction from the verification problem for concurrent programs against safety specifications to the verification of sequential programs against safety specifications, where the reduction is parameterized by a set of auxiliary variables A, such that the concurrent program compositionally satisfies its specification using auxiliary variables A iff the sequentialization satisfies its specification. Existing sequentializations for concurrent programs work only for underapproximations like bounded context-switching, while our sequentialization has the salient feature that it can prove concurrent programs entirely correct, as long as it has a compositional proof. The sequentialization allows us to use sequential verification tools (including deductive verification tools and predicate abstraction tools) to analyze and prove concurrent programs correct. We also report on our experience in the deductive verification of concurrent programs by proving their sequential counterparts using the program verifier Boogie.

Original languageEnglish (US)
Title of host publicationTools and Algorithms for the Construction and Analysis of Systems - 17th Int. Conf., TACAS 2011, Held as Part of the Joint European Conf. on Theory and Practice of Software, ETAPS 2011, Proceedings
Pages26-40
Number of pages15
DOIs
StatePublished - 2011
Event17th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2011, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2011 - Saarbrucken, Germany
Duration: Mar 26 2011Apr 3 2011

Publication series

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

Other

Other17th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2011, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2011
CountryGermany
CitySaarbrucken
Period3/26/114/3/11

Keywords

  • compositional verification
  • concurrent programs
  • sequentialization

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

Fingerprint Dive into the research topics of 'Compositionality entails sequentializability'. Together they form a unique fingerprint.

Cite this