We are inviting IDEALS users, both people looking for materials in IDEALS and those who want to deposit their work, to give us feedback on improving this service through an interview. Participants will receive a $20 VISA gift card. Please sign up via webform.

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