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 language | English (US) |
|---|---|
| Article number | 6571568 |
| Pages (from-to) | 358-367 |
| Number of pages | 10 |
| Journal | Proceedings - Symposium on Logic in Computer Science |
| DOIs | |
| State | Published - Sep 9 2013 |
| Event | 2013 28th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2013 - New Orleans, LA, United States Duration: Jun 25 2013 → Jun 28 2013 |
Fingerprint
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 journal › Conference article
}
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 -