This program is tentative and subject to change.

Tue 16 Jun 2026 11:40 - 12:00 at Meadows CD - Array Programming and Verification Chair(s): Jubi Taneja

The Partitioned Global Address Space (PGAS) execution model is a promising competing model to MPI. PGAS implementations offer several programmability advantages over their MPI counterparts while preserving the appeal of high-performance communication libraries. Among existing PGAS instances, the Chapel compiler and programming language is one of the most robust and well-supported implementations. Being around for nearly two decades, Chapel has evolved into a mature PGAS implementation, with several compiler and run-time features. Unfortunately, despite multiple advances, the error detection support in Chapel has been largely ignored. In this work, we propose new static analyses to detect various distributed, multi-locale anomalies in Chapel programs. We leverage constraint formulae that model Chapel semantics together with anomaly-specific constraints that encapsulate triggering conditions of the anomaly. Generated models are then checked with Z3 SMT solver to decide the existence of anomalies. While our implementation targets Chapel, the underlying approach generalizes to other PGAS languages, as we illustrate through a construct mapping to UPC. We demonstrate the effectiveness of our analyses on well-known scientific operators and communication patterns, comparing against native Chapel analyses and MPI debugging tools targeting lowered Chapel code. We further validate our approach with an evaluation on UPC programs.

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