SPLASH 2025
Sun 12 - Sat 18 October 2025 Singapore
co-located with ICFP/SPLASH 2025
Mon 13 Oct 2025 16:00 - 16:20 at Orchid East - Abstraction and Proofs Chair(s): Xavier Rival

We establish a formal relation between quantitative and semantic approximations—formalized by pre-metrics and upper closure operators (ucos), respectively—by means of Galois connections. This connection reveals that it is far from trivial for a pre-metric to uniquely identify a uco, highlighting the structural constraints and, more generally, the distinct identity inherent to semantic approximations.

Building on this foundation, we introduce a general composition of semantic and quantitative approximations. This allows us to define a new confidentiality property, called Partial Abstract Non-Interference, that measures bounded variations in program behavior over abstract properties of data. We then relate this property to Partial Completeness in abstract interpretation, revealing a deeper connection between static analysis precision and security guarantees.

Mon 13 Oct

Displayed time zone: Perth change

16:00 - 17:40
Abstraction and ProofsSAS at Orchid East
Chair(s): Xavier Rival Inria - CNRS - Ecole Normale Superieure de Paris - PSL University
16:00
20m
Talk
Relating Distances and Abstractions: An Abstract Interpretation Perspective
SAS
Marco Campion Sorbonne Université, 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 Software Languages Lab, Vrije Universiteit Brussel, Quentin Stiévenart Université du Québec à Montréal, Coen De Roover Vrije Universiteit Brussel
Pre-print