Relating Distances and Abstractions: An Abstract Interpretation Perspective
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 OctDisplayed 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 20mTalk | 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 20mTalk | 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 20mTalk | 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 20mTalk | Contextual Equality Saturation SAS | ||
17:20 20mTalk | 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 | ||