Fri 17 Jun 2022 13:50 - 14:10 at Kon-Tiki - Verification I Chair(s): Ralf Jung
Sat 18 Jun 2022 01:50 - 02:10 at Kon-Tiki - Verification I

Fine-grained concurrent programs are difficult to get right, yet play an important role in modern-day computers. We want to prove strong specifications of such programs, with minimal user effort, in a trustworthy way. In this paper, we present Diaframe—an automated and foundational verification tool for fine-grained concurrent programs.

Diaframe is built on top of the Iris framework for higher-order concurrent separation logic in Coq, which already has a foundational soundness proof and the ability to give strong specifications, but lacks automation. Diaframe equips Iris with strong automation using a novel, extendable, goal-directed proof search strategy, using ideas from linear logic programming and bi-abduction. A benchmark of 24 examples from the literature shows that the proof burden of Diaframe is competitive with existing non-foundational tools, while its expressivity and soundness guarantees are stronger.

Fri 17 Jun

Displayed time zone: Pacific Time (US & Canada) change

13:30 - 14:50
Verification IPLDI at Kon-Tiki +12h
Chair(s): Ralf Jung MPI-SWS
13:30
20m
Talk
Compass: Strong and Compositional Library Specifications in Relaxed Memory Separation Logic
PLDI
Hoang-Hai Dang MPI-SWS, Jaehwang Jung KAIST, South Korea, Jaemin Choi KAIST, Duc-Than Nguyen University of Illinois at Chicago, William Mansky University of Illinois at Chicago, Jeehoon Kang KAIST, Derek Dreyer MPI-SWS
DOI
13:50
20m
Talk
Diaframe: Automated Verification of Fine-Grained Concurrent Programs in Iris
PLDI
Ike Mulder Radboud University Nijmegen, Robbert Krebbers Radboud University Nijmegen, Herman Geuvers Radboud University Nijmegen, Netherlands
Link to publication DOI Pre-print
14:10
20m
Talk
Islaris: Verification of Machine Code Against Authoritative ISA Semantics
PLDI
Michael Sammler MPI-SWS, Angus Hammond University of Cambridge, Rodolphe Lepigre MPI-SWS, Brian Campbell University of Edinburgh, Jean Pichon-Pharabod Aarhus University, Derek Dreyer MPI-SWS, Deepak Garg MPI-SWS, Peter Sewell University of Cambridge
DOI
14:30
20m
Talk
RustHornBelt: A Semantic Foundation for Functional Verification of Rust Programs with Unsafe Code
PLDI
Yusuke Matsushita The University of Tokyo, Xavier Denis Université Paris-Saclay, CNRS, ENS Paris-Saclay, INRIA, Laboratoire Méthodes Formelles, Jacques-Henri Jourdan Université Paris-Saclay, CNRS, ENS Paris-Saclay, Laboratoire Méthodes Formelles, Derek Dreyer MPI-SWS
DOI

Sat 18 Jun

Displayed time zone: Pacific Time (US & Canada) change

01:30 - 02:50
Verification IPLDI at Kon-Tiki
01:30
20m
Talk
Compass: Strong and Compositional Library Specifications in Relaxed Memory Separation Logic
PLDI
Hoang-Hai Dang MPI-SWS, Jaehwang Jung KAIST, South Korea, Jaemin Choi KAIST, Duc-Than Nguyen University of Illinois at Chicago, William Mansky University of Illinois at Chicago, Jeehoon Kang KAIST, Derek Dreyer MPI-SWS
DOI
01:50
20m
Talk
Diaframe: Automated Verification of Fine-Grained Concurrent Programs in Iris
PLDI
Ike Mulder Radboud University Nijmegen, Robbert Krebbers Radboud University Nijmegen, Herman Geuvers Radboud University Nijmegen, Netherlands
Link to publication DOI Pre-print
02:10
20m
Talk
Islaris: Verification of Machine Code Against Authoritative ISA Semantics
PLDI
Michael Sammler MPI-SWS, Angus Hammond University of Cambridge, Rodolphe Lepigre MPI-SWS, Brian Campbell University of Edinburgh, Jean Pichon-Pharabod Aarhus University, Derek Dreyer MPI-SWS, Deepak Garg MPI-SWS, Peter Sewell University of Cambridge
DOI
02:30
20m
Talk
RustHornBelt: A Semantic Foundation for Functional Verification of Rust Programs with Unsafe Code
PLDI
Yusuke Matsushita The University of Tokyo, Xavier Denis Université Paris-Saclay, CNRS, ENS Paris-Saclay, INRIA, Laboratoire Méthodes Formelles, Jacques-Henri Jourdan Université Paris-Saclay, CNRS, ENS Paris-Saclay, Laboratoire Méthodes Formelles, Derek Dreyer MPI-SWS
DOI