Write a Blog >>
Sun 20 - Fri 25 October 2019 Athens, Greece
Wed 23 Oct 2019 11:00 - 11:22 at Olympia - Modular Verification Chair(s): Friedrich Steimann

The correctness of many algorithms and data structures depends on reachability properties, that is, on the existence of chains of references between objects in the heap. Reasoning about reachability is difficult for two main reasons. First, any heap modification may affect an unbounded number of reference chains, which complicates modular verification, in particular, framing. Second, general graph reachability is not supported by first-order SMT solvers, which impedes automatic verification.

In this paper, we present a modular specification and verification technique for reachability properties in separation logic. For each method, we specify reachability only locally within the fragment of the heap on which the method operates. We identify relative convexity, a novel relation between the heap fragments of a client and a callee, which enables (first-order) reachability framing, that is, extending reachability properties from the heap fragment of a callee to the larger fragment of its client, enabling precise procedure-modular reasoning. Our technique supports practically important heap structures, namely acyclic graphs with a bounded outdegree as well as (potentially cyclic) graphs with at most one path (modulo cycles) between each pair of nodes. The integration into separation logic allows us to reason about reachability and other properties in a uniform way, to verify concurrent programs, and to automate our technique via existing separation logic verifiers. We demonstrate that our verification technique is amenable to SMT-based verification by encoding a number of benchmark examples into the Viper verification infrastructure.

Modular Verification of Heap Reachability Properties in Separation Logic - Slides v1.7 (presentation-1.7.pdf)2.54MiB

Wed 23 Oct
Times are displayed in time zone: Beirut change

11:00 - 12:30: Modular VerificationOOPSLA at Olympia
Chair(s): Friedrich SteimannFernuni Hagen
11:00 - 11:22
Research paper
Modular Verification of Heap Reachability Properties in Separation Logic
Link to publication DOI Pre-print File Attached
11:22 - 11:45
Modular Verification of Web Page Layout
Pavel PanchekhaUniversity of Utah, Michael D. ErnstUniversity of Washington, USA, Zachary TatlockUniversity of Washington, Seattle, Shoaib KamilAdobe
11:45 - 12:07
Modular Verification for Almost-Sure Termination of Probabilistic Programs
Mingzhang HuangShanghai Jiao Tong University, Hongfei FuShanghai Jiao Tong University, Krishnendu ChatterjeeIST Austria, Amir Kafshdar GoharshadyIST Austria
12:07 - 12:30
Leveraging Rust Types for Modular Specification and Verification
Vytautas AstrauskasETH Zurich, Switzerland, Peter MüllerETH Zurich, Federico PoliETH Zurich, Switzerland, Alexander J. SummersETH Zurich
DOI Pre-print