Partial Order Reduction for Rewriting Semantics of Programming Languages

Farzan, Azadeh; Meseguer, José

Permalink

https://hdl.handle.net/2142/11040 Copy

Description

Title

Partial Order Reduction for Rewriting Semantics of Programming Languages

Author(s)

• Farzan, Azadeh
• Meseguer, José

Issue Date

2005-06

Keyword(s)

programming languages

Abstract

Partial order reduction (POR) capabilities are typically added by extending a model checking algorithm supporting analysis of programs in a given programming language. In this paper we propose a generic method to generate a model checker with POR capabilities for any programming language of interest. The method is based on giving a formal executable specification of the semantics of a programming language L as a rewrite theory R_L, and then exploiting the efficient execution, search, and LTL model checking capabilities of the Maude rewriting logic language to generate a model checker for L essentially for free. The key idea is to achieve the desired POR reduction by means of a theory transformation that transforms the theory R_L into a semantically equivalent theory which is then used to explore the POR-reduced state space. This can be done for a language L with relatively little effort and has the advantage of not requiring any changes in the underlying model checker. Our experiments with the JVM and with a Promela-like language indicate that significant state space reductions and time speedups can be gained for the tools generated this way.

Type of Resource

text

Permalink

http://hdl.handle.net/2142/11040

Copyright and License Information

You are granted permission for the non-commercial reproduction, distribution, display, and performance of this technical report in any format, BUT this permission is only for a period of 45 (forty-five) days from the most recent time that you verified that this technical report is still available from the University of Illinois at Urbana-Champaign Computer Science Department under terms that include this permission. All other rights are reserved by the author(s).

Owning Collections