SAS 2022
Mon 5 - Wed 7 December 2022 Auckland, New Zealand
co-located with SPLASH 2022
Tue 6 Dec 2022 14:30 - 15:00 at AMRF Auditorium - Logic and Completeness Chair(s): Roberto Giacobazzi

Abstract interpretation provides an over-approximation of program behaviours that is used to prove the absence of bugs. When the computed approximation in the chosen abstract domain is as precise as possible, we say the analysis is complete and false alarms cannot arise. Unfortunately for any non trivial abstract domain there is some program whose analysis is incomplete. In this paper we want to characterize the classes of complete programs on some non-trivial abstract domains for studying their expressiveness. To this aim we introduce the notion of bounded domains for posets with ascending chains of bounded length only. We show that any complete program on bounded domains can be rewritten in an equivalent canonical form without nontrivial loops. This result proves that program termination on the class of complete programs on bounded domain is decidable. Moreover, semantic equivalence between programs in the above class can be reduced to determining the equivalence of a set of guarded statements. We show how our approach can be applied to a quite large class of programs. Indeed, abstract domains defined on Boolean abstractions that are complete for the same functions can be composed by preserving boundedness and completeness also w.r.t. any expressible guard. This suggests that new complete bounded abstract domains can be tailored on the guards and functions appearing in the program. Their existence is sufficient to prove decidability of termination and program equivalence for such programs.

Tue 6 Dec

Displayed time zone: Auckland, Wellington change

13:30 - 15:00
Logic and CompletenessSAS at AMRF Auditorium
Chair(s): Roberto Giacobazzi University of Verona
13:30
30m
Talk
Invariant Inference With Provable Complexity From the Monotone Theory
SAS
Yotam M. Y. Feldman Tel Aviv University, Sharon Shoham Tel Aviv University
14:00
30m
Talk
Local Completeness Logic on Kleene Algebra with Tests
SAS
Marco Milanese Dipartimento di Matematica, University of Padova, Italy, Francesco Ranzato University of Padova
14:30
30m
Talk
Deciding program properties via complete abstractions on bounded domains
SAS
Roberto Bruni University of Pisa, Roberta Gori University of Pisa, Nicolas Manini IMDEA Software Institute