SPLASH 2023
Sun 22 - Fri 27 October 2023 Cascais, Portugal
Fri 27 Oct 2023 11:36 - 11:54 at Room I - verification 1 Chair(s): Gowtham Kaki

Program logics for bug-finding (such as the recently introduced Incorrectness Logic) have framed correctness and incorrectness as dual concepts requiring different logical foundations. In this paper, we argue that a single unified theory can be used for both correctness and incorrectness reasoning. We present Outcome Logic (OL), a novel generalization of Hoare Logic that is both monadic (to capture computational effects) and monoidal (to reason about outcomes and reachability). OL is guaranteed to find true bugs, while retaining correctness reasoning abilities as well. To formalize the applicability of OL to both correctness and incorrectness, we prove that any false OL specification can be disproven in OL itself. We also use our framework to reason about new types of incorrectness in non-deterministic and probabilistic programs. Given these advances, we advocate for OL as a new foundational theory of correctness and incorrectness.

Fri 27 Oct

Displayed time zone: Lisbon change

11:00 - 12:30
verification 1OOPSLA at Room I
Chair(s): Gowtham Kaki University of Colorado at Boulder
11:00
18m
Talk
Solving Conditional Linear Recurrences for Program Verification: The Periodic Case
OOPSLA
Chenglin Wang Hong Kong University of Science and Technology, Fangzhen Lin Hong Kong University of Science and Technology
DOI
11:18
18m
Talk
Melocoton: A Program Logic for Verified Interoperability Between OCaml and C
OOPSLA
Armaël Guéneau Université Paris-Saclay - CNRS - ENS Paris-Saclay - Inria, Johannes Hostert ETH Zurich, Simon Spies MPI-SWS, Michael Sammler MPI-SWS, Lars Birkedal Aarhus University, Derek Dreyer MPI-SWS
Link to publication DOI
11:36
18m
Talk
Outcome Logic: A Unifying Foundation for Correctness and Incorrectness Reasoning
OOPSLA
Noam Zilberstein Cornell University, Derek Dreyer MPI-SWS, Alexandra Silva Cornell University
DOI Pre-print
11:54
18m
Talk
Formal Abstractions for Packet SchedulingDistinguished Paper
OOPSLA
Anshuman Mohan Cornell University, Yunhe Liu Cornell University, Nate Foster Cornell University, Tobias Kappé Open University of the Netherlands; University of Amsterdam, Dexter Kozen Cornell University
Link to publication DOI
12:12
18m
Talk
P4R-Type: A Verified API for P4 Control Plane Programs
OOPSLA
Jens Kanstrup Larsen DTU, Roberto Guanciale KTH Royal Institute of Technology, Philipp Haller KTH Royal Institute of Technology, Alceste Scalas DTU
DOI Pre-print Media Attached