SPLASH 2025
Sun 12 - Sat 18 October 2025 Singapore
co-located with ICFP/SPLASH 2025

This program is tentative and subject to change.

Mon 13 Oct 2025 16:20 - 16:40 at Orchid East - Abstraction and Proofs Chair(s): Xavier Rival

We present AURA, a novel abstract interpretation for obtaining sound, precise bounds on the posterior distributions computed by probabilistic programs. AURA allows programmers to specify interval bounds that capture uncertainty or perturbations of the observed data. AURA abstractly computes the infinite set of posteriors that would result from performing inference for any possible data value in the specified perturbation range. AURA then certifies precise bounds on probabilistic queries over that set of posteriors. AURA’s precision stems from a novel gradient-based optimization leveraging the structure of probabilistic programs. Our evaluation across 11 benchmarks with data perturbation shows that AURA improves precision by an order of magnitude (12.8x on average) over the interval-based abstract interpreter, within a run time of 3.1 seconds (geomean), using a GPU parallel implementation.

This program is tentative and subject to change.

Mon 13 Oct

Displayed time zone: Perth change

16:00 - 17:40
Abstraction and ProofsSAS at Orchid East
Chair(s): Xavier Rival Inria; ENS; CNRS; PSL University
16:00
20m
Talk
Relating Distances and Abstractions: An Abstract Interpretation Perspective
SAS
Marco Campion INRIA & ENS Paris | Université PSL, Isabella Mastroeni University of Verona, Caterina Urban Inria & ENS | PSL
16:20
20m
Talk
Precise Abstract Interpretation of Probabilistic Programs with Interval Data Uncertainty
SAS
Zixin Huang University of Illinois at Urbana-Champaign, USA, Jacob Laurel Georgia Institute of Technology, Saikat Dutta University of Illinois at Urbana-Champaign, Sasa Misailovic University of Illinois at Urbana-Champaign
16:40
20m
Talk
Specifying and Verifying Future Conditions
SAS
Yahui Song Standard Chartered Bank, Darius Foo National University of Singapore, Wei-Ngan Chin National University of Singapore
17:00
20m
Talk
Contextual Equality Saturation
SAS
17:20
20m
Talk
Abstracting Concolic Execution for Soft Contract Verification
SAS
Bram Vandenbogaerde , Quentin Stiévenart Université du Québec à Montréal, Coen De Roover Vrije Universiteit Brussel
Pre-print