A Verification Logic for Rewriting Logic

This paper proposes the development of a logic for verifying properties of programs in rewriting logic. Rewriting logic is primarily a logic of change, in which deduction corresponds directly to computation, and not a logic to talk about change in a more indirect and global manner, such as the diffe...

Full description

Saved in:
Bibliographic Details
Published in:Journal of logic and computation 2005-06, Vol.15 (3), p.317-352
Main Authors: Martí-Oliet, Narciso, Pita, Isabel, Fiadeiro, José Luiz, Meseguer, José, Maibaum, Tom
Format: Article
Language:English
Subjects:
modal action logic
Rewriting logic
specification
temporal logic
verification
Citations: Items that cite this one
Online Access:Get full text
Tags: Add Tag
No Tags, Be the first to tag this record!
Description
Summary:This paper proposes the development of a logic for verifying properties of programs in rewriting logic. Rewriting logic is primarily a logic of change, in which deduction corresponds directly to computation, and not a logic to talk about change in a more indirect and global manner, such as the different modal and temporal logics that can be found in the literature. We start by defining a modal action logic (VLRL) in which rewrite rules are captured as actions. The main novelty of this logic is a topological modality associated with state constructors that allows us to reason about the structure of states, stating that the current state can be decomposed into regions satisfying certain properties. Then, on top of the modal logic, we define a temporal logic for reasoning about properties of the computations generated from rewrite theories, and demonstrate its potential by means of several examples.
ISSN:0955-792X
1465-363X
DOI:10.1093/logcom/exi015