Towards a verification logic for rewriting logic

José Luis Fiadeiro, Tom Maibaum, Narciso Martí-Oliet, Jose Meseguer, Isabel Pita

Research output: Chapter in Book/Report/Conference proceedingConference contribution

19 Citations (Scopus)

Abstract

This paper is an initial step in 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 two simple examples.

Original languageEnglish
Title of host publicationRecent Trends in Algebraic Development Techniques - 14th International Workshop, WADT 1999, Selected Papers
EditorsDidier Bert, Christine Choppy, Peter Mosses
PublisherSpringer Verlag
Pages438-458
Number of pages21
Volume1827
ISBN (Print)3540678980, 9783540678984
Publication statusPublished - 2000
Event14th International Workshop on Algebraic Development Techniques, WADT 1999 - Chateau de Bonas, France
Duration: 15 Sep 199918 Sep 1999

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume1827
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Conference

Conference14th International Workshop on Algebraic Development Techniques, WADT 1999
CountryFrance
CityChateau de Bonas
Period15/09/9918/09/99

Fingerprint Dive into the research topics of 'Towards a verification logic for rewriting logic'. Together they form a unique fingerprint.

  • Cite this

    Fiadeiro, J. L., Maibaum, T., Martí-Oliet, N., Meseguer, J., & Pita, I. (2000). Towards a verification logic for rewriting logic. In D. Bert, C. Choppy, & P. Mosses (Eds.), Recent Trends in Algebraic Development Techniques - 14th International Workshop, WADT 1999, Selected Papers (Vol. 1827, pp. 438-458). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 1827). Springer Verlag.