Program verification using reachability logic

Grigore Roşu; Andrei Ştefănescu; Ştefan Ciobâcă

Program verification using reachability logic

Grigore Roşu, Andrei Ştefănescu, Ştefan Ciobâcă

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

Abstract

Matching logic is a logic for reasoning about program configuration properties in a language-parametric manner. On top of matching logic we define reachability logic and equivalence logic. Reachability logic enables reasoning about the correctness of both deterministic programs (one-path reachability logic) and non-deterministic programs (all-path reachability logic). Equivalence logic enables reasoning about program equivalence. We introduce K, a semantics framework which has been used to define the operational semantics of real-world languages such as C, Java, and JavaScript. We show how the logics above are integrated in K. In particular, we show how the semantics of C, Java, and JavaScript yield automatic program verifiers for the respective languages. The verifiers can check the full functional correctness of challenging heap manipulation programs implementing the same data-structures in these languages (e.g. AVL trees). We also show how to reason about program equivalence using semantics defined in K.

Original language	English (US)
Title of host publication	Rewriting Logic and Its Applications - 11th International Workshop, WRLA 2016 Held as a Satellite Event of ETAPS 2016, Revised Selected Papers
Editors	Dorel Lucanu
Publisher	Springer
ISBN (Print)	9783319448015
State	Published - 2016
Event	11th International Workshop on Rewriting Logic and its Applications, WRLA 2016 held as a Satellite Event of European Joint Conferences on Theory and Practice of Software, ETAPS 2016 - Eindhoven, Netherlands Duration: Apr 2 2016 → Apr 3 2016

Publication series

Name	Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume	9942 LNCS
ISSN (Print)	0302-9743
ISSN (Electronic)	1611-3349

Other

Other	11th International Workshop on Rewriting Logic and its Applications, WRLA 2016 held as a Satellite Event of European Joint Conferences on Theory and Practice of Software, ETAPS 2016
Country/Territory	Netherlands
City	Eindhoven
Period	4/2/16 → 4/3/16

ASJC Scopus subject areas

Theoretical Computer Science
General Computer Science

Library availability

Discover UIUC Full Text

Cite this

Roşu, G., Ştefănescu, A., & Ciobâcă, Ş. (2016). Program verification using reachability logic. In D. Lucanu (Ed.), Rewriting Logic and Its Applications - 11th International Workshop, WRLA 2016 Held as a Satellite Event of ETAPS 2016, Revised Selected Papers (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 9942 LNCS). Springer.

Program verification using reachability logic. / Roşu, Grigore; Ştefănescu, Andrei; Ciobâcă, Ştefan.
Rewriting Logic and Its Applications - 11th International Workshop, WRLA 2016 Held as a Satellite Event of ETAPS 2016, Revised Selected Papers. ed. / Dorel Lucanu. Springer, 2016. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 9942 LNCS).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

Roşu, G, Ştefănescu, A & Ciobâcă, Ş 2016, Program verification using reachability logic. in D Lucanu (ed.), Rewriting Logic and Its Applications - 11th International Workshop, WRLA 2016 Held as a Satellite Event of ETAPS 2016, Revised Selected Papers. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 9942 LNCS, Springer, 11th International Workshop on Rewriting Logic and its Applications, WRLA 2016 held as a Satellite Event of European Joint Conferences on Theory and Practice of Software, ETAPS 2016, Eindhoven, Netherlands, 4/2/16.

Roşu G, Ştefănescu A, Ciobâcă Ş. Program verification using reachability logic. In Lucanu D, editor, Rewriting Logic and Its Applications - 11th International Workshop, WRLA 2016 Held as a Satellite Event of ETAPS 2016, Revised Selected Papers. Springer. 2016. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).

Roşu, Grigore ; Ştefănescu, Andrei ; Ciobâcă, Ştefan. / Program verification using reachability logic. Rewriting Logic and Its Applications - 11th International Workshop, WRLA 2016 Held as a Satellite Event of ETAPS 2016, Revised Selected Papers. editor / Dorel Lucanu. Springer, 2016. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).

@inproceedings{15ea9c8f0ff14ba7b2094de977e753fa,

title = "Program verification using reachability logic",

abstract = "Matching logic is a logic for reasoning about program configuration properties in a language-parametric manner. On top of matching logic we define reachability logic and equivalence logic. Reachability logic enables reasoning about the correctness of both deterministic programs (one-path reachability logic) and non-deterministic programs (all-path reachability logic). Equivalence logic enables reasoning about program equivalence. We introduce K, a semantics framework which has been used to define the operational semantics of real-world languages such as C, Java, and JavaScript. We show how the logics above are integrated in K. In particular, we show how the semantics of C, Java, and JavaScript yield automatic program verifiers for the respective languages. The verifiers can check the full functional correctness of challenging heap manipulation programs implementing the same data-structures in these languages (e.g. AVL trees). We also show how to reason about program equivalence using semantics defined in K.",

author = "Grigore Ro{\c s}u and Andrei {\c S}tef{\u a}nescu and {\c S}tefan Ciob{\^a}c{\u a}",

note = "Publisher Copyright: {\textcopyright} Springer International Publishing Switzerland 2016.; 11th International Workshop on Rewriting Logic and its Applications, WRLA 2016 held as a Satellite Event of European Joint Conferences on Theory and Practice of Software, ETAPS 2016 ; Conference date: 02-04-2016 Through 03-04-2016",

year = "2016",

language = "English (US)",

isbn = "9783319448015",

series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

publisher = "Springer",

editor = "Dorel Lucanu",

booktitle = "Rewriting Logic and Its Applications - 11th International Workshop, WRLA 2016 Held as a Satellite Event of ETAPS 2016, Revised Selected Papers",

address = "Germany",

}

TY - GEN

T1 - Program verification using reachability logic

AU - Roşu, Grigore

AU - Ştefănescu, Andrei

AU - Ciobâcă, Ştefan

PY - 2016

Y1 - 2016

N2 - Matching logic is a logic for reasoning about program configuration properties in a language-parametric manner. On top of matching logic we define reachability logic and equivalence logic. Reachability logic enables reasoning about the correctness of both deterministic programs (one-path reachability logic) and non-deterministic programs (all-path reachability logic). Equivalence logic enables reasoning about program equivalence. We introduce K, a semantics framework which has been used to define the operational semantics of real-world languages such as C, Java, and JavaScript. We show how the logics above are integrated in K. In particular, we show how the semantics of C, Java, and JavaScript yield automatic program verifiers for the respective languages. The verifiers can check the full functional correctness of challenging heap manipulation programs implementing the same data-structures in these languages (e.g. AVL trees). We also show how to reason about program equivalence using semantics defined in K.

AB - Matching logic is a logic for reasoning about program configuration properties in a language-parametric manner. On top of matching logic we define reachability logic and equivalence logic. Reachability logic enables reasoning about the correctness of both deterministic programs (one-path reachability logic) and non-deterministic programs (all-path reachability logic). Equivalence logic enables reasoning about program equivalence. We introduce K, a semantics framework which has been used to define the operational semantics of real-world languages such as C, Java, and JavaScript. We show how the logics above are integrated in K. In particular, we show how the semantics of C, Java, and JavaScript yield automatic program verifiers for the respective languages. The verifiers can check the full functional correctness of challenging heap manipulation programs implementing the same data-structures in these languages (e.g. AVL trees). We also show how to reason about program equivalence using semantics defined in K.

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

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

M3 - Conference contribution

AN - SCOPUS:84986230439

SN - 9783319448015

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

BT - Rewriting Logic and Its Applications - 11th International Workshop, WRLA 2016 Held as a Satellite Event of ETAPS 2016, Revised Selected Papers

A2 - Lucanu, Dorel

PB - Springer

T2 - 11th International Workshop on Rewriting Logic and its Applications, WRLA 2016 held as a Satellite Event of European Joint Conferences on Theory and Practice of Software, ETAPS 2016

Y2 - 2 April 2016 through 3 April 2016

ER -

Program verification using reachability logic

Abstract

Publication series

Other

ASJC Scopus subject areas

Library availability

Related links

Fingerprint

Cite this