Abstract
This paper presents a language-independent proof system for reachability properties of programs written in non-deterministic (e.g. concurrent) languages, referred to as all-path reachability logic. It derives partial-correctness properties with all-path semantics (a state satisfying a given precondition reaches states satisfying a given postcondition on all terminating execution paths). The proof system takes as axioms any unconditional operational semantics, and is sound (partially correct) and (relatively) complete, independent of the object language; the soundness has also been mechanized (Coq). This approach is implemented in a tool for semantics-based verification as part of the \(\mathbb K\) framework.
Full version of this paper, with proofs, available at http://hdl.handle.net/2142/46296
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Nipkow, T.: Winskel is (almost) right: Towards a mechanized semantics textbook. Formal Aspects of Computing 10, 171–186 (1998)
Jacobs, B.: Weakest pre-condition reasoning for Java programs with JML annotations. J. Logic and Algebraic Programming 58(1-2), 61–88 (2004)
Appel, A.W.: Verified software toolchain. In: Barthe, G. (ed.) ESOP 2011. LNCS, vol. 6602, pp. 1–17. Springer, Heidelberg (2011)
Roşu, G., Ştefănescu, A.: Checking reachability using matching logic. In: OOPSLA, pp. 555–574. ACM (2012)
Roşu, G., Ştefănescu, A.: From hoare logic to matching logic reachability. In: Giannakopoulou, D., Méry, D. (eds.) FM 2012. LNCS, vol. 7436, pp. 387–402. Springer, Heidelberg (2012)
Roşu, G., Ştefănescu, A.: Towards a unified theory of operational and axiomatic semantics. In: Czumaj, A., Mehlhorn, K., Pitts, A., Wattenhofer, R. (eds.) ICALP 2012, Part II. LNCS, vol. 7392, pp. 351–363. Springer, Heidelberg (2012)
Roşu, G., Ştefănescu, A., Ciobâcă, C., Moore, B.M.: One-path reachability logic. In: LICS 2013. IEEE (2013)
Roşu, G., Ellison, C., Schulte, W.: Matching logic: An alternative to hoare/Floyd logic. In: Johnson, M., Pavlovic, D. (eds.) AMAST 2010. LNCS, vol. 6486, pp. 142–162. Springer, Heidelberg (2011)
Roşu, G., Şerbănută, T.F.: An overview of the K semantic framework. J. Logic and Algebraic Programming 79(6), 397–434 (2010)
Ellison, C., Roşu, G.: An executable formal semantics of C with applications. In: POPL, pp. 533–544. ACM (2012)
Felleisen, M., Findler, R.B., Flatt, M.: Semantics Engineering with PLT Redex. MIT (2009)
Berry, G., Boudol, G.: The chemical abstract machine. Theoretical Computer Science 96(1), 217–248 (1992)
Matthews, J., Findler, R.B.: An operational semantics for Scheme. JFP 18(1), 47–86 (2008)
Ştefănescu, A., Ciobâcă, C., Moore, B.M., Şerbănuţă, T.F., Roşu, G.: Reachability Logic in K. Technical Report. University of Illinois (November 2013), http://hdl.handle.net/2142/46296
Filaretti, D., Maffeis, S.: An executable formal semantics of php. In: ECOOP. LNCS (to appear, 2014)
de Moura, L., Bjørner, N.S.: Z3: An efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337–340. Springer, Heidelberg (2008)
Hoare, C.A.R.: An axiomatic basis for computer programming. Communications of the ACM 12(10), 576–580 (1969)
Owicki, S.S., Gries, D.: Verifying properties of parallel programs: An axiomatic approach. Communications of the ACM 19(5), 279–285 (1976)
Jones, C.B.: Specification and design of (parallel) programs. In: Mason, R.E.A. (ed.) Information Processing 1983: World Congress Proceedings, pp. 321–332. Elsevier (1984)
O’Hearn, P.W.: Resources, concurrency, and local reasoning. Theoretical Computer Science 375(1-3), 271–307 (2007)
Reynolds, J.C.: Separation logic: A logic for shared mutable data structures. In: LICS, pp. 55–74. IEEE (2002)
Feng, X.: Local rely-guarantee reasoning. In: POPL, pp. 315–327. ACM (2009)
Vafeiadis, V., Parkinson, M.J.: A marriage of rely/guarantee and separation logic. In: Caires, L., Vasconcelos, V.T. (eds.) CONCUR 2007. LNCS, vol. 4703, pp. 256–271. Springer, Heidelberg (2007)
Reddy, U.S., Reynolds, J.C.: Syntactic control of interference for separation logic. In: POPL, pp. 323–336. ACM (2012)
Hayman, J.: Granularity and concurrent separation logic. In: Katoen, J.-P., König, B. (eds.) CONCUR 2011. LNCS, vol. 6901, pp. 219–234. Springer, Heidelberg (2011)
Bae, K., Escobar, S., Meseguer, J.: Abstract logical model checking of infinite-state systems using narrowing. In: RTA, pp. 81–96 (2013)
Rocha, C., Meseguer, J.: Proving safety properties of rewrite theories. In: Corradini, A., Klin, B., Cîrstea, C. (eds.) CALCO 2011. LNCS, vol. 6859, pp. 314–328. Springer, Heidelberg (2011)
Rocha, C., Meseguer, J., Muñoz, C.A.: Rewriting modulo smt and open system analysis. In: WRLA. LNCS (to appear, 2014)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2014 Springer International Publishing Switzerland
About this paper
Cite this paper
Ştefănescu, A., Ciobâcă, Ş., Mereuta, R., Moore, B.M., Şerbănută, T.F., Roşu, G. (2014). All-Path Reachability Logic. In: Dowek, G. (eds) Rewriting and Typed Lambda Calculi. RTA TLCA 2014 2014. Lecture Notes in Computer Science, vol 8560. Springer, Cham. https://doi.org/10.1007/978-3-319-08918-8_29
Download citation
DOI: https://doi.org/10.1007/978-3-319-08918-8_29
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-08917-1
Online ISBN: 978-3-319-08918-8
eBook Packages: Computer ScienceComputer Science (R0)