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 language | English (US) |
---|---|
Pages (from-to) | 61-78 |
Number of pages | 18 |
Journal | Electronic Notes in Theoretical Computer Science |
Volume | 176 |
Issue number | 4 |
DOIs | |
State | Published - 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)