Files in this item



application/pdfstefanescu-ciob ... serbanuta-rosu-2013-tr.pdf (237kB)
(no description provided)PDF


Title:Reachability Logic in K
Author(s):Stefanescu, Andrei; Ciobaca, Stefan; Moore, Brandon; Serbanuta, Traian Florin; Rosu, Grigore
Subject(s):program verification
operational semantics
axiomatic semantics
Abstract:This paper presents a language-independent proof system for reachability properties of programs written in non-deterministic (concurrent) languages, referred to as reachability logic. The proof system derives partial-correctness properties with either all-path or one-path semantics, i.e., that states satisfying a given precondition reach states satisfying a given postcondition on all execution paths, respectively on one execution path. Reachability logic takes as axioms any unconditional operational semantics, and is sound (i.e., partially correct) and (relatively) complete, independent of the object language; the soundness has also been mechanized. The proof system is implemented in a tool for semantics-based verification as part of the K framework, and evaluated on a few examples.
Issue Date:2013-11
Citation Info:@inproceedings{stefanescu-ciobaca-moore-serbanuta-rosu-2013-tr, author = {Andrei \c{S}tef\u{a}nescu and \c{S}tefan Ciob\^{a}c\u{a} and Brandon M. Moore and Traian Florin \c{S}erb\u{a}nu\c{t}\u{a} and Grigore Ro\c{s}u}, title = {Reachability Logic in K}, institution = {University of Illinois}, month = {Nov}, year = {2013}, }
Genre:Technical Report
Publication Status:unpublished
Peer Reviewed:not peer reviewed
Date Available in IDEALS:2013-11-22

This item appears in the following Collection(s)

Item Statistics