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

Local Completeness Logic (LCL) has been put forward as a program logic for proving both the correctness and incorrectness of program specifications. LCL is an abstract logic, parameterized by an abstract domain that allows combining over- and under-approximations of program behaviors. It turns out that LCL instantiated to the trivial singleton abstraction boils down to O’Hearn incorrectness logic, which allows us to prove the presence of program bugs. It has been recently proved that suitable extensions of Kleene algebra with tests (KAT) allow representing both O’Hearn incorrectness and Hoare correctness program logics within the same equational framework. In this work, we generalize this result by showing how KATs extended either with a modal diamond operator or with a top element are able to represent the local completeness logic LCL. This is achieved by studying how these extended KATs can be endowed with an abstract domain so as to define the validity of correctness/incorrectness LCL triples and to show that the LCL proof system is logically sound and, under some hypotheses, complete.

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