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
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

Fingerprint

Reachability
Semantics
Systems analysis
Acoustic waves
Logic
Distributed Systems
Experiments
Unification
System Design
Prototype
Verify
Invariant
Range of data
Experiment
Language

Keywords

  • Program verification
  • Reachability logic
  • Rewriting logic

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

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. https://doi.org/10.1007/978-3-319-94460-9_12

A constructor-based reachability logic for rewrite theories. / Skeirik, Stephen; Stefanescu, Andrei; Meseguer, José.

Logic-Based Program Synthesis and Transformation - 27th International Symposium, LOPSTR 2017, Revised Selected Papers. ed. / Fabio Fioravanti; John P. Gallagher. Springer-Verlag, 2018. p. 201-217 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 10855 LNCS).

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

Skeirik, S, Stefanescu, A & Meseguer, J 2018, A constructor-based reachability logic for rewrite theories. in F Fioravanti & JP Gallagher (eds), Logic-Based Program Synthesis and Transformation - 27th International Symposium, LOPSTR 2017, Revised Selected Papers. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 10855 LNCS, Springer-Verlag, pp. 201-217, 27th International Symposium on Logic-Based Program Synthesis and Transformation, LOPSTR 2017, Namur, Belgium, 10/10/17. https://doi.org/10.1007/978-3-319-94460-9_12
Skeirik S, Stefanescu A, Meseguer J. A constructor-based reachability logic for rewrite theories. In Fioravanti F, Gallagher JP, editors, Logic-Based Program Synthesis and Transformation - 27th International Symposium, LOPSTR 2017, Revised Selected Papers. Springer-Verlag. 2018. p. 201-217. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). https://doi.org/10.1007/978-3-319-94460-9_12
Skeirik, Stephen ; Stefanescu, Andrei ; Meseguer, José. / A constructor-based reachability logic for rewrite theories. Logic-Based Program Synthesis and Transformation - 27th International Symposium, LOPSTR 2017, Revised Selected Papers. editor / Fabio Fioravanti ; John P. Gallagher. Springer-Verlag, 2018. pp. 201-217 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).
@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",
year = "2018",
month = "1",
day = "1",
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-Verlag",
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",

}

TY - GEN

T1 - A constructor-based reachability logic for rewrite theories

AU - Skeirik, Stephen

AU - Stefanescu, Andrei

AU - Meseguer, José

PY - 2018/1/1

Y1 - 2018/1/1

N2 - 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.

AB - 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.

KW - Program verification

KW - Reachability logic

KW - Rewriting logic

UR - http://www.scopus.com/inward/record.url?scp=85050347410&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=85050347410&partnerID=8YFLogxK

U2 - 10.1007/978-3-319-94460-9_12

DO - 10.1007/978-3-319-94460-9_12

M3 - Conference contribution

AN - SCOPUS:85050347410

SN - 9783319944593

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 201

EP - 217

BT - Logic-Based Program Synthesis and Transformation - 27th International Symposium, LOPSTR 2017, Revised Selected Papers

A2 - Fioravanti, Fabio

A2 - Gallagher, John P.

PB - Springer-Verlag

ER -