Blogs (9) >>
SPLASH 2016
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
Talk
Semantics-Based Program Verifiers for All LanguagesAECDistinguished Paper Award
OOPSLA
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
Talk
Hoare-Style Specifications as Correctness Conditions for Non-linearizable Concurrent ObjectsAEC
OOPSLA
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
Talk
An Operational Semantics for C/C++11 ConcurrencyAEC
OOPSLA
Kyndylan NienhuisUniversity of Cambridge, Kayvan MemarianUniversity of Cambridge, Peter SewellUniversity of Cambridge
DOI
11:45 - 12:10
Talk
Modeling and Analysis of Remote Memory Access ProgrammingAECDistinguished Paper Award
OOPSLA
Andrei Marian DanETH Zurich, Patrick LamUniversity of Waterloo, Canada, Torsten HoeflerETH Zurich, Martin VechevETH Zurich
DOI Pre-print Media Attached