Program verification using reachability logic

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

Research output: Chapter in Book/Report/Conference proceedingConference 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 languageEnglish (US)
Title of host publicationRewriting Logic and Its Applications - 11th International Workshop, WRLA 2016 Held as a Satellite Event of ETAPS 2016, Revised Selected Papers
EditorsDorel Lucanu
PublisherSpringer
ISBN (Print)9783319448015
StatePublished - Jan 1 2016
Event11th 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 2016Apr 3 2016

Publication series

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

Other

Other11th 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/TerritoryNetherlands
CityEindhoven
Period4/2/164/3/16

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

Fingerprint

Dive into the research topics of 'Program verification using reachability logic'. Together they form a unique fingerprint.

Cite this