Semantics-based program verifiers for all languages
- 19 October 2016
- conference paper
- conference paper
- Published by Association for Computing Machinery (ACM) in Proceedings of the 2016 ACM SIGPLAN International Conference on Generative Programming: Concepts and Experiences
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
Funding Information
- National Science Foundation (CCF- 1218605, CCF-1318191, CCF-1421575)
- Defense Advanced Research Projects Agency (FA8750-12-C-0284)
This publication has 51 references indexed in Scilit:
- Checking reachability using matching logicACM SIGPLAN Notices, 2012
- Specification and verificationCommunications of the ACM, 2011
- An overview of the K semantic frameworkThe Journal of Logic and Algebraic Programming, 2010
- jStarACM SIGPLAN Notices, 2008
- Verifying properties of well-founded linked listsACM SIGPLAN Notices, 2006
- Weakest pre-condition reasoning for Java programs with JML annotationsThe Journal of Logic and Algebraic Programming, 2004
- The pointer assertion logic engineACM SIGPLAN Notices, 2001
- A needed narrowing strategyJournal of the ACM, 2000
- The chemical abstract machineTheoretical Computer Science, 1992
- Dynamic LogicPublished by Springer Science and Business Media LLC ,1984