Access Restriction

Author Stefănescu, Andrei ♦ Yuwen, Shijiao ♦ Li, Yilong ♦ Roşu, Grigore ♦ Park, Daejun
Source ACM Digital Library
Content type Text
Publisher Association for Computing Machinery (ACM)
File Format PDF
Language English
Subject Domain (in DDC) Computer science, information & general works ♦ Computer programming, programs & data
Subject Keyword Reachability logic ♦ K framework ♦ Matching logic
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.
Description Affiliation: University of Illinois at Urbana-Champaign, USA (Stefănescu, Andrei; Park, Daejun; Yuwen, Shijiao; Roşu, Grigore) || Runtime Verification, USA (Li, Yilong)
Age Range 18 to 22 years ♦ above 22 year
Educational Use Research
Education Level UG and PG
Learning Resource Type Article
Publisher Date 1983-05-01
Publisher Place New York
Journal ACM SIGPLAN Notices (SIGP)
Volume Number 51
Issue Number 10
Page Count 18
Starting Page 74
Ending Page 91

Open content in new tab

   Open content in new tab
Source: ACM Digital Library