@inproceedings{bacf907a0d1d4e2697996722177fc826,
title = "A constructor-based reachability logic for rewrite theories",
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.",
keywords = "Program verification, Reachability logic, Rewriting logic",
author = "Stephen Skeirik and Andrei Stefanescu and Jos{\'e} Meseguer",
note = "Publisher Copyright: {\textcopyright} 2018, Springer International Publishing AG, part of Springer Nature.; 27th International Symposium on Logic-Based Program Synthesis and Transformation, LOPSTR 2017 ; Conference date: 10-10-2017 Through 12-10-2017",
year = "2018",
doi = "10.1007/978-3-319-94460-9_12",
language = "English (US)",
isbn = "9783319944593",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
publisher = "Springer",
pages = "201--217",
editor = "Fabio Fioravanti and Gallagher, {John P.}",
booktitle = "Logic-Based Program Synthesis and Transformation - 27th International Symposium, LOPSTR 2017, Revised Selected Papers",
address = "Germany",
}