SPLASH 2020
Sun 15 - Sat 21 November 2020 Online Conference
Fri 20 Nov 2020 13:20 - 13:40 at SPLASH-III - F-4B Chair(s): Aviral Goel, Ton Chanh Le
Sat 21 Nov 2020 01:20 - 01:40 at SPLASH-III - F-4B

Lighthouse projects like CompCert, seL4, IronFleet, and DeepSpec have demonstrated that full system verification is feasible by establishing a refinement between an abstract system specification and an executable implementation. Existing approaches however impose severe restrictions on the abstract system specifications due to their limited expressiveness or versatility, or on the executable code due to their use of suboptimal code extraction or inexpressive program logics. We propose a novel methodology that combines the compositional refinement of event-based models of distributed systems with the verification of full-fledged program code using expressive separation logics, which support features of realistic programming languages like heap data structures and concurrency. Our main technical contribution is a formal framework that soundly relates event-based system models to program specifications in separation logics. This enables protocol development tools to soundly interoperate with program verifiers to establish a refinement between the model and the code. We formalized our framework, Igloo, in Isabelle/HOL. We report on three case studies, a leader election protocol, a replication protocol, and a security protocol, for which we refine formal requirements into program specifications that we implement in Java and Python and prove correct using the VeriFast and Nagini tools.

Fri 20 Nov
Times are displayed in time zone: Central Time (US & Canada) change

13:00 - 14:20: F-4BOOPSLA at SPLASH-III +12h
Chair(s): Aviral GoelNortheastern University, Ton Chanh LeStevens Institute of Technology
13:00 - 13:20
Talk
OOPSLA
Cyril SixKalray / Grenoble Alps University / CNRS / Grenoble INP / VERIMAG, Sylvain BoulméGrenoble Alps University / CNRS / Grenoble INP / VERIMAG, David MonniauxGrenoble Alps University / CNRS / Grenoble INP / VERIMAG
Link to publication DOI Media Attached
13:20 - 13:40
Talk
OOPSLA
Christoph SprengerETH Zurich, Tobias KlenzeETH Zurich, Marco EilersETH Zurich, Felix A. WolfETH Zurich, Peter MüllerETH Zurich, Martin ClochardETH Zurich, David BasinETH Zurich
Link to publication DOI Media Attached
13:40 - 14:00
Talk
OOPSLA
Yaniv DavidTechnion, Uri AlonTechnion, Eran YahavTechnion
Link to publication DOI Pre-print Media Attached
14:00 - 14:20
Talk
OOPSLA
Fei HeTsinghua University, Jitao HanTsinghua University
Link to publication DOI Media Attached

Sat 21 Nov
Times are displayed in time zone: Central Time (US & Canada) change