Semantics-based program verifiers for all languages

Andrei Stefanescu, Daejun Park, Shijiao Yuwen, Yilong Li, Grigore Roşu

Research output: Contribution to journalArticlepeer-review

Abstract

We present a language-independent verification framework that can be instantiated with an operational semantics to automatically generate a program verifier. The framework treats both the operational semantics and the program correctness specifications as reachability rules between matching logic patterns, and uses the sound and relatively complete reachability logic proof system to prove the specifications using the semantics. We instantiate the framework with the semantics of one academic language, KernelC, as well as with three recent semantics of real-world languages, C, Java, and JavaScript, developed independently of our verification infrastructure. We evaluate our approach empirically and show that the generated program verifiers can check automatically the full functional correctness of challenging heap-manipulating programs implementing operations on list and tree data structures, like AVL trees. This is the first approach that can turn the operational semantics of real-world languages into correct-by-construction automatic verifiers.

Original languageEnglish (US)
Pages (from-to)74-91
Number of pages18
JournalACM SIGPLAN Notices
Volume51
Issue number10
DOIs
StatePublished - Oct 19 2016

Keywords

  • K framework
  • matching logic
  • reachability logic

ASJC Scopus subject areas

  • Computer Science(all)

Fingerprint

Dive into the research topics of 'Semantics-based program verifiers for all languages'. Together they form a unique fingerprint.

Cite this