This program is tentative and subject to change.

Tue 16 Jun 2026 10:50 - 11:15 at Meadows CD - Array Programming and Verification Chair(s): Jubi Taneja

Relational verification establishes properties that re late two executions of a program, such as robustness, non-interference, sensitivity, and relational cost bounds. While existing techniques can verify unary safety properties of array programs, relational properties of array programs remain largely out of reach for automated tools. We present relational cell morphing, which tracks a small number of distinguished array cells across two executions simultaneously, reducing relational verification of array programs to constrained Horn clause (CHC) solving over scalar variables without requiring array theories. A dynamic cell reselection mechanism, combined with universally quantified prophecy variables, enables tight relational cost bounds parameterized by the number of positions where two arrays agree. A merged asynchronous scheduler further extends the approach to programs with different iteration structures, where type-based relational cost analysis produces only loose bounds. We evaluate on 65 encodings spanning 8 property classes, all verified in seconds to minutes by PCSat.

This program is tentative and subject to change.

Tue 16 Jun

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

10:30 - 12:10
Array Programming and VerificationARRAY at Meadows CD
Chair(s): Jubi Taneja Gimlet Labs
10:30
20m
Talk
Refined Remora: Constraining Array Shapes
ARRAY
Vadym Matviichuk Northeastern University, Olin Shivers Northeastern University
10:50
25m
Talk
Relational Cell Morphing: Automated Verification of Relational Properties of Array Programs
ARRAY
Weihao Qu Monmouth University, Marco Gaboardi Boston University, Hiroshi Unno Tohoku University, Eric Koskinen Stevens Institute of Technology
11:15
25m
Talk
Graded Monoids for Dependently Typed Array Programming
ARRAY
Juuso Haavisto University of Oxford, Jeremy Gibbons Department of Computer Science, University of Oxford
11:40
20m
Talk
Portable Anomaly Detection for Distributed PGAS Programs based on Array Mapping Abstractions
ARRAY
Raneem Abu-Yosef Ohio State University, Thomas Huddleston The Ohio State University, Kirshanthan Sundararajah Virginia Tech, Martin Kong Ohio State University
12:00
10m
Live Q&A
Mini Panel
ARRAY