| Title: |
Abstract Lipschitz Continuity: Combining Semantic and Quantitative Approximations |
| Authors: |
Campion, Marco; Mastroeni, Isabella; Pasqua, Michele; Urban, Caterina |
| Contributors: |
Analyse Statique par Interprétation Abstraite (ANTIQUE); Département d'informatique - ENS-PSL (DI-ENS); École normale supérieure - Paris (ENS-PSL); Université Paris Sciences et Lettres (PSL)-Université Paris Sciences et Lettres (PSL)-Institut National de Recherche en Informatique et en Automatique (Inria)-Centre National de la Recherche Scientifique (CNRS)-École normale supérieure - Paris (ENS-PSL); Université Paris Sciences et Lettres (PSL)-Université Paris Sciences et Lettres (PSL)-Institut National de Recherche en Informatique et en Automatique (Inria)-Centre National de la Recherche Scientifique (CNRS)-Centre Inria de Paris; Institut National de Recherche en Informatique et en Automatique (Inria); Université Paris Sciences et Lettres (PSL)-Université Paris Sciences et Lettres (PSL)-Institut National de Recherche en Informatique et en Automatique (Inria)-Centre National de la Recherche Scientifique (CNRS); Centre Inria de Paris; Algorithmes, Programmes et Résolution (APR); LIP6; Sorbonne Université (SU)-Centre National de la Recherche Scientifique (CNRS)-Sorbonne Université (SU)-Centre National de la Recherche Scientifique (CNRS); Università degli studi di Verona = University of Verona (UNIVR); ANR-23-PEIA-0006,SAIF,Safe AI through Formal Methods(2023) |
| Source: |
https://inria.hal.science/hal-04935306 ; 2026. |
| Publisher Information: |
CCSD |
| Publication Year: |
2026 |
| Subject Terms: |
Abstract Lipschitz Continuity; Abstract Interpretation; Partial Completeness; Partial Abstract Non-Interference; Abstract Robustness; [INFO]Computer Science [cs] |
| Description: |
International audience ; We introduce Abstract Lipschitz Continuity (ALC), an extensional (i.e., input/output) property that ensures proportionally bounded differences in the semantic approximations of the output of a function (e.g., a program semantics) when the semantic approximations of the input differ slightly. ALC explicitly discerns between two complementary notions of approximation: quantitative differences, expressed via pre-metrics, and qualitative (or semantic) differences, captured through upper closure operators. This explicit separation of approximations has two main advantages. First, it enables ALC to be related to other important extensional program properties, including partial abstract non-interference in language-based security, partial completeness in abstract interpretation, and abstract robustness in machine learning. Second, ALC enables reasoning about its validity for programs through inductive reasoning on their syntax and on the chosen semantic abstractions. To this end, we propose a sound deductive system, parameterized by the quantitative and semantic approximations of interest, for proving ALC of programs. This proof system makes explicit the assumptions required for ALC, thereby ensuring a compositional proof approach. |
| Document Type: |
report |
| Language: |
English |
| Availability: |
https://inria.hal.science/hal-04935306; https://inria.hal.science/hal-04935306v4/document; https://inria.hal.science/hal-04935306v4/file/Abstract%20Lipschitz%20Continuity%3A%20Combining%20Semantic%20and%20Quantitative%20Approximations.pdf |
| Rights: |
https://creativecommons.org/licenses/by/4.0/ ; info:eu-repo/semantics/OpenAccess |
| Accession Number: |
edsbas.291B4206 |
| Database: |
BASE |