One-path reachability logic

Grigore Rosu, Andrei Stefanescu, Stefan Ciobaca, Brandon M. Moore

Research output: Contribution to journalConference article

Abstract

This paper introduces(one-path) reach ability logic, a language-independent proof system for program verification, which takes an operational semantics as axioms and derivesreach ability rules, which generalize Hoare triples. This system improves on previous work by allowing operational semantics given withconditional* rewrite rules, which are known to support all major styles of operational semantics. In particular, Kahn's big-step and Plot kin's small-step semantic styles are now supported. The reach ability logic proof system is shown sound (i.e., partially correct) and (relatively) complete. Reach ability logic thus eliminates the need to independently define an axiomatic and an operational semantics for each language, and the non-negligible effort to prove the former sound and complete w.r.t. the latter. The soundness result has also been formalized in Coq, allowing reach ability logic derivations to serve as formal proof certificates that rely only on the operational semantics.

Original languageEnglish (US)
Article number6571568
Pages (from-to)358-367
Number of pages10
JournalProceedings - Symposium on Logic in Computer Science
DOIs
StatePublished - Sep 9 2013
Event2013 28th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2013 - New Orleans, LA, United States
Duration: Jun 25 2013Jun 28 2013

Fingerprint

Operational Semantics
Reachability
Semantics
Logic
Path
Proof System
Program Verification
Acoustic waves
Formal Proof
Certificate
Soundness
Axioms
Eliminate
Generalise
Style
Sound
Language

Keywords

  • Hoare logic
  • axiomatic semantics
  • logic
  • operational semantics
  • program verification

ASJC Scopus subject areas

  • Software
  • Mathematics(all)

Cite this

One-path reachability logic. / Rosu, Grigore; Stefanescu, Andrei; Ciobaca, Stefan; Moore, Brandon M.

In: Proceedings - Symposium on Logic in Computer Science, 09.09.2013, p. 358-367.

Research output: Contribution to journalConference article

Rosu, Grigore ; Stefanescu, Andrei ; Ciobaca, Stefan ; Moore, Brandon M. / One-path reachability logic. In: Proceedings - Symposium on Logic in Computer Science. 2013 ; pp. 358-367.
@article{fe42645895b143bca6dc35a8b3999aa1,
title = "One-path reachability logic",
abstract = "This paper introduces(one-path) reach ability logic, a language-independent proof system for program verification, which takes an operational semantics as axioms and derivesreach ability rules, which generalize Hoare triples. This system improves on previous work by allowing operational semantics given withconditional* rewrite rules, which are known to support all major styles of operational semantics. In particular, Kahn's big-step and Plot kin's small-step semantic styles are now supported. The reach ability logic proof system is shown sound (i.e., partially correct) and (relatively) complete. Reach ability logic thus eliminates the need to independently define an axiomatic and an operational semantics for each language, and the non-negligible effort to prove the former sound and complete w.r.t. the latter. The soundness result has also been formalized in Coq, allowing reach ability logic derivations to serve as formal proof certificates that rely only on the operational semantics.",
keywords = "Hoare logic, axiomatic semantics, logic, operational semantics, program verification",
author = "Grigore Rosu and Andrei Stefanescu and Stefan Ciobaca and Moore, {Brandon M.}",
year = "2013",
month = "9",
day = "9",
doi = "10.1109/LICS.2013.42",
language = "English (US)",
pages = "358--367",
journal = "Proceedings - Symposium on Logic in Computer Science",
issn = "1043-6871",
publisher = "Institute of Electrical and Electronics Engineers Inc.",

}

TY - JOUR

T1 - One-path reachability logic

AU - Rosu, Grigore

AU - Stefanescu, Andrei

AU - Ciobaca, Stefan

AU - Moore, Brandon M.

PY - 2013/9/9

Y1 - 2013/9/9

N2 - This paper introduces(one-path) reach ability logic, a language-independent proof system for program verification, which takes an operational semantics as axioms and derivesreach ability rules, which generalize Hoare triples. This system improves on previous work by allowing operational semantics given withconditional* rewrite rules, which are known to support all major styles of operational semantics. In particular, Kahn's big-step and Plot kin's small-step semantic styles are now supported. The reach ability logic proof system is shown sound (i.e., partially correct) and (relatively) complete. Reach ability logic thus eliminates the need to independently define an axiomatic and an operational semantics for each language, and the non-negligible effort to prove the former sound and complete w.r.t. the latter. The soundness result has also been formalized in Coq, allowing reach ability logic derivations to serve as formal proof certificates that rely only on the operational semantics.

AB - This paper introduces(one-path) reach ability logic, a language-independent proof system for program verification, which takes an operational semantics as axioms and derivesreach ability rules, which generalize Hoare triples. This system improves on previous work by allowing operational semantics given withconditional* rewrite rules, which are known to support all major styles of operational semantics. In particular, Kahn's big-step and Plot kin's small-step semantic styles are now supported. The reach ability logic proof system is shown sound (i.e., partially correct) and (relatively) complete. Reach ability logic thus eliminates the need to independently define an axiomatic and an operational semantics for each language, and the non-negligible effort to prove the former sound and complete w.r.t. the latter. The soundness result has also been formalized in Coq, allowing reach ability logic derivations to serve as formal proof certificates that rely only on the operational semantics.

KW - Hoare logic

KW - axiomatic semantics

KW - logic

KW - operational semantics

KW - program verification

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

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

U2 - 10.1109/LICS.2013.42

DO - 10.1109/LICS.2013.42

M3 - Conference article

AN - SCOPUS:84883333346

SP - 358

EP - 367

JO - Proceedings - Symposium on Logic in Computer Science

JF - Proceedings - Symposium on Logic in Computer Science

SN - 1043-6871

M1 - 6571568

ER -