The ever growing pervasiveness of software systems in modern days technology results in an increasing need of \emph{software/program correctness proofs}. The latter, allow developers to spot software failures before production, hence preventing potentially catastrophic repercussions on our society, as in the case of safety-critical infrastructures. Unfortunately, correctness proofs may fail (even when software is actually correct) due to program analysis imprecision: program analysis sacrifices precision in order to gain decidability. In standard abstract interpretation-based static analyses, such imprecision is ``measured'' in terms of \emph{completeness} of the chosen observation (i.e., of the chosen abstract domain) w.r.t. the programming language semantics. In this setting, fixed the language language, it is crucial to have decidable techniques to determine whether the chosen abstraction is sufficiently precise to analyze the program under consideration. In this paper, we characterize abstract domain precision from a novel point of view, providing a formal framework for \emph{characterizing} and (statically) \emph{verifying} abstract domain precision, that can be adopted also in the case of ``weakened'', i.e., Galois Connection-less, static analysis frameworks. Distinctive examples adopting such frameworks are the Convex Polyhedra and Automata domains, for which standard approaches to reason about analysis precision (i.e., completeness) cannot be applied.

Domain Precision in Galois Connection-Less Abstract Interpretation

Isabella Mastroeni;Michele Pasqua
2023-01-01

Abstract

The ever growing pervasiveness of software systems in modern days technology results in an increasing need of \emph{software/program correctness proofs}. The latter, allow developers to spot software failures before production, hence preventing potentially catastrophic repercussions on our society, as in the case of safety-critical infrastructures. Unfortunately, correctness proofs may fail (even when software is actually correct) due to program analysis imprecision: program analysis sacrifices precision in order to gain decidability. In standard abstract interpretation-based static analyses, such imprecision is ``measured'' in terms of \emph{completeness} of the chosen observation (i.e., of the chosen abstract domain) w.r.t. the programming language semantics. In this setting, fixed the language language, it is crucial to have decidable techniques to determine whether the chosen abstraction is sufficiently precise to analyze the program under consideration. In this paper, we characterize abstract domain precision from a novel point of view, providing a formal framework for \emph{characterizing} and (statically) \emph{verifying} abstract domain precision, that can be adopted also in the case of ``weakened'', i.e., Galois Connection-less, static analysis frameworks. Distinctive examples adopting such frameworks are the Convex Polyhedra and Automata domains, for which standard approaches to reason about analysis precision (i.e., completeness) cannot be applied.
2023
978-3-031-44244-5
Abstract interpretation, Abstract Non-Interference, Completeness, Hyperproperties, (Hyper) Static analysis
File in questo prodotto:
Non ci sono file associati a questo prodotto.

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/11562/1111909
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus ND
  • ???jsp.display-item.citation.isi??? ND
social impact