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

Invariant inference algorithms such as interpolation-based inference and IC3/PDR show that it is feasible, in practice, to find inductive invariants for many interesting systems, but non-trivial upper bounds on the computational complexity of such algorithms are scarce, and limited to simple syntactic forms of invariants. In this paper we achieve invariant inference algorithms, in the domain of propositional transition systems, with emph{provable upper bounds} on the number of SAT calls. We do this by building on the emph{monotone theory}, developed by Bshouty for exact learning Boolean formulas. We prove results for two invariant inference frameworks: (i) emph{model-based interpolation}, where we show an algorithm that, under certain conditions about reachability, efficiently infers invariants when they have both short CNF and DNF representations (transcending previous results about monotone invariants); and (ii) emph{abstract interpretation} in a domain based on the monotone theory that was previously studied in relation to emph{property-directed reachability}, where we propose an efficient implementation of the best abstract transformer, leading to overall complexity bounds on the number of SAT calls. These results build on a novel procedure for computing least monotone overapproximations.

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