Blogs (9) >>
Sun 30 October - Fri 4 November 2016 Amsterdam, Netherlands
Wed 2 Nov 2016 10:30 - 10:55 at Matterhorn 2 - Semantics and Verification Chair(s): Jonathan Aldrich

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.

Wed 2 Nov
Times are displayed in time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

10:30 - 12:10: Semantics and VerificationOOPSLA at Matterhorn 2
Chair(s): Jonathan AldrichCarnegie Mellon University
10:30 - 10:55
Semantics-Based Program Verifiers for All LanguagesAECDistinguished Paper Award
Andrei StefanescuUniversity of Illinois at Urbana-Champaign, Daejun ParkUniversity of Illinois at Urbana-Champaign, Shijiao YuwenUniversity of Illinois at Urbana-Champaign, Yilong LiRuntime Verification, Inc., Grigore RoşuUniversity of Illinois at Urbana-Champaign
DOI Media Attached
10:55 - 11:20
Hoare-Style Specifications as Correctness Conditions for Non-linearizable Concurrent ObjectsAEC
Ilya SergeyUniversity College London, Aleksandar NanevskiIMDEA Software Institute, Anindya BanerjeeIMDEA Software Institute, Germán Andrés DelbiancoIMDEA Software Institute
DOI Pre-print Media Attached File Attached
11:20 - 11:45
An Operational Semantics for C/C++11 ConcurrencyAEC
Kyndylan NienhuisUniversity of Cambridge, Kayvan MemarianUniversity of Cambridge, Peter SewellUniversity of Cambridge
11:45 - 12:10
Modeling and Analysis of Remote Memory Access ProgrammingAECDistinguished Paper Award
Andrei Marian DanETH Zurich, Patrick LamUniversity of Waterloo, Canada, Torsten HoeflerETH Zurich, Martin VechevETH Zurich
DOI Pre-print Media Attached