A constructor-based reachability logic for rewrite theories

Stephen Skeirik, Andrei Stefanescu, José Meseguer

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


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
Number of pages17
ISBN (Print)9783319944593
StatePublished - 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


Other27th International Symposium on Logic-Based Program Synthesis and Transformation, LOPSTR 2017


  • Program verification
  • Reachability logic
  • Rewriting logic

ASJC Scopus subject areas

  • Theoretical Computer Science
  • General Computer Science


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

Cite this