Program verification by coinduction

Brandon Moore, Lucas Peña, Grigore Rosu

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Abstract

We present a novel program verification approach based on coinduction, which takes as input an operational semantics. No intermediates like program logics or verification condition generators are needed. Specifications can be written using any state predicates. We implement our approach in Coq, giving a certifying language-independent verification framework. Our proof system is implemented as a single module imported unchanged into language-specific proofs. Automation is reached by instantiating a generic heuristic with language-specific tactics. Manual assistance is also smoothly allowed at points the automation cannot handle. We demonstrate the power and versatility of our approach by verifying algorithms as complicated as Schorr-Waite graph marking and instantiating our framework for object languages in several styles of semantics. Finally, we show that our coinductive approach subsumes reachability logic, a recent language-independent sound and (relatively) complete logic for program verification that has been instantiated with operational semantics of languages as complex as C, Java and JavaScript.

Original languageEnglish (US)
Title of host publicationProgramming Languages and Systems - 27th European Symposium on Programming, ESOP 2018, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2018, Proceedings
EditorsAmal Ahmed
PublisherSpringer-Verlag Berlin Heidelberg
Pages589-618
Number of pages30
ISBN (Print)9783319898834
DOIs
StatePublished - Jan 1 2018
Event27th European Symposium on Programming, ESOP 2018 Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2018 - Thessaloniki, Greece
Duration: Apr 14 2018Apr 20 2018

Publication series

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

Other

Other27th European Symposium on Programming, ESOP 2018 Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2018
CountryGreece
CityThessaloniki
Period4/14/184/20/18

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

Fingerprint Dive into the research topics of 'Program verification by coinduction'. Together they form a unique fingerprint.

  • Cite this

    Moore, B., Peña, L., & Rosu, G. (2018). Program verification by coinduction. In A. Ahmed (Ed.), Programming Languages and Systems - 27th European Symposium on Programming, ESOP 2018, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2018, Proceedings (pp. 589-618). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 10801 LNCS). Springer-Verlag Berlin Heidelberg. https://doi.org/10.1007/978-3-319-89884-1_21