@inproceedings{7b5a9d0b321b4a6c89e53a6e30444d94,
title = "Semantics-based program verifiers for all languages",
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.",
keywords = "K framework, Matching logic, Reachability logic",
author = "Andrei Stef{\'a}nescu and Daejun Park and Shijiao Yuwen and Yilong Li and Grigore Rosu",
note = "Publisher Copyright: {\textcopyright} 2016 ACM.; 2016 ACM SIGPLAN International Conference on Object-Oriented Programming, Systems, Languages, and Applications, OOPSLA 2016 ; Conference date: 31-10-2016 Through 01-11-2016",
year = "2016",
month = oct,
day = "19",
doi = "10.1145/2983990.2984027",
language = "English (US)",
series = "Proceedings of the Conference on Object-Oriented Programming Systems, Languages, and Applications, OOPSLA",
publisher = "Association for Computing Machinery",
pages = "74--91",
editor = "Eelco Visser and Yannis Smaragdakis",
booktitle = "OOPSLA 2016 - Proceedings of the 2016 ACM SIGPLAN International Conference on Object-Oriented Programming, Systems, Languages, and Applications",
address = "United States",
}