Partial Order Reduction for Rewriting Semantics of Programming Languages

Azadeh Farzan, José Meseguer

Research output: Contribution to journalArticlepeer-review

Abstract

Software model checkers are typically language-specific, require substantial development efforts, and are hard to reuse for other languages. Adding partial order reduction (POR) capabilities to such tools typically requires sophisticated changes to the tool's model checking algorithms. This paper proposes a new method to make software model checkers language-independent and improving their performance through POR. Getting the POR capabilities does not require making any changes to the underlying model checking algorithms: for each language L, they are instead achieved through a theory transformationRL {mapping} RL + P O R of L's formal semantics, rewrite theory RL. Under very minimal assumptions, this can be done for any language L with relatively little effort. Our experiments with the JVM, a Promela-like language and Maude indicate that significant state space reductions and time speedups can be gained for tools generated this way.

Original languageEnglish (US)
Pages (from-to)61-78
Number of pages18
JournalElectronic Notes in Theoretical Computer Science
Volume176
Issue number4
DOIs
StatePublished - Jul 28 2007

Keywords

  • Maude
  • Partial order reduction
  • model checking
  • programming language semantics
  • rewriting logic

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

Fingerprint Dive into the research topics of 'Partial Order Reduction for Rewriting Semantics of Programming Languages'. Together they form a unique fingerprint.

Cite this