POPL 2024
Sun 14 - Sat 20 January 2024 London, United Kingdom

Hyperproperties are properties that relate multiple execution traces of one or more programs. A notable subclass, known as k-safety, is capable of expressing practically important properties like program equivalence and non-interference. Furthermore, hyperproperties beyond k-safety, including generalized non-interference (GNI) and co-termination, have significant applications in security.

Automating verification of hyperproperties is challenging, as it involves finding an appropriate alignment of multiple execution traces for successful verification. Merely reasoning about each program copy’s executions separately, or analyzing states from running multiple copies in lock-step, can sometimes lead to failure. Therefore, it necessitates synthesizing a scheduler that dictates when and which program copies move, to ensure an appropriate alignment of multiple traces. With this alignment, synthesizing relational invariants maintained by the aligned states enables us to prove k-safety. Additionally, verifying GNI and co-termination requires synthesis of Skolem functions and ranking functions, respectively.

In this talk, I will explain and compare two approaches for automating relational verification. The first approach is constraint-based, reducing the synthesis problem into a constraint solving problem within a class that extends Constrained Horn Clauses (CHCs). The second approach is based on proof search within an inductive proof system for a first-order fixpoint logic modulo theories.

Tue 16 Jan

Displayed time zone: London change

09:00 - 10:30
Session 5: keynote, Program and System VerificationVMCAI at Marconi Room
Chair(s): Ori Lahav Tel Aviv University
Automating Relational Verification of Infinite-State Programs
Hiroshi Unno University of Tsukuba
Deductive Verification of Parameterized Embedded Systems modeled in SystemC
Philip Tasche University of Twente, Raúl E. Monti University of Twente, Stefanie Eva Drerup University of Münster, Pauline Blohm Uni Münster, Paula Herber University of Munster, Germany, Marieke Huisman University of Twente
Automatically Enforcing Rust Trait Properties
Twain Byrnes Carnegie Mellon University, Yoshiki Takashima Carnegie Mellon University, Limin Jia Carnegie Mellon University