Files in this item

FilesDescriptionFormat

application/pdf

application/pdfPartial Order R ... Programming Languages.pdf (189kB)
(no description provided)PDF

Description

Title:Partial Order Reduction for Rewriting Semantics of Programming Languages
Author(s):Farzan, Azadeh; Meseguer, José
Subject(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.
Issue Date:2005-06
Genre:Technical Report
Type:Text
URI:http://hdl.handle.net/2142/11040
Rights 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).
Date Available in IDEALS:2009-04-17


This item appears in the following Collection(s)

Item Statistics