A constructor-based reachability logic for rewrite theories

Stephen Skeirik, Andrei Stefanescu, José Meseguer

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

Abstract

Reachability logic has been applied to K rewrite-rule-based language definitions as a language-generic logic of programs. To be able to verify not just code but also distributed system designs, a new rewrite-theory-generic reachability logic is presented and proved sound for a wide class of rewrite theories. Constructor-based semantic unification, matching, and satisfiability procedures greatly increase the range of decidable background theories that can be used in reachability logic proofs. New methods for proving invariants of possibly never terminating distributed systems are developed, and experiments with a prototype implementation illustrating the new proof methods are presented.

Original languageEnglish (US)
Title of host publicationLogic-Based Program Synthesis and Transformation - 27th International Symposium, LOPSTR 2017, Revised Selected Papers
EditorsFabio Fioravanti, John P. Gallagher
PublisherSpringer-Verlag Berlin Heidelberg
Pages201-217
Number of pages17
ISBN (Print)9783319944593
DOIs
StatePublished - Jan 1 2018
Event27th International Symposium on Logic-Based Program Synthesis and Transformation, LOPSTR 2017 - Namur, Belgium
Duration: Oct 10 2017Oct 12 2017

Publication series

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

Other

Other27th International Symposium on Logic-Based Program Synthesis and Transformation, LOPSTR 2017
CountryBelgium
CityNamur
Period10/10/1710/12/17

Keywords

  • Program verification
  • Reachability logic
  • Rewriting logic

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

Fingerprint Dive into the research topics of 'A constructor-based reachability logic for rewrite theories'. Together they form a unique fingerprint.

  • Cite this

    Skeirik, S., Stefanescu, A., & Meseguer, J. (2018). A constructor-based reachability logic for rewrite theories. In F. Fioravanti, & J. P. Gallagher (Eds.), Logic-Based Program Synthesis and Transformation - 27th International Symposium, LOPSTR 2017, Revised Selected Papers (pp. 201-217). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 10855 LNCS). Springer-Verlag Berlin Heidelberg. https://doi.org/10.1007/978-3-319-94460-9_12