Thu 16 Jun 2022 11:20 - 11:40 at Toucan - Analysis Chair(s): Xiaokang Qiu
Thu 16 Jun 2022 23:20 - 23:40 at Toucan - Analysis

Abstract interpretation is a sound-by-construction method for program verification: any erroneous program will raise some alarm. However, the verification of correct programs may yield false-alarms, namely it may be incomplete. Ideally, one would like to perform the analysis on the most abstract domain that is precise enough to avoid false-alarms. We show how to exploit a weaker notion of completeness, called local completeness, to optimally refine abstract domains and thus enhance the precision of program verification. Our main result establishes necessary and sufficient conditions for the existence of an optimal, locally complete refinement, called pointed shell. On top of this, we define two repair strategies to remove all false-alarms along a given abstract computation: the first proceeds forward, along with the concrete computation, while the second moves backward within the abstract computation. Our results pave the way for a novel modus operandi for automating program verification that we call Abstract Interpretation Repair (AIR): instead of choosing beforehand the right abstract domain, we can start in any abstract domain and progressively repair its local incompleteness as needed. In this regard, AIR is for abstract interpretation what CEGAR is for abstract model checking.

Thu 16 Jun

Displayed time zone: Pacific Time (US & Canada) change

10:40 - 12:00
AnalysisPLDI at Toucan +12h
Chair(s): Xiaokang Qiu Purdue University, USA
10:40
20m
Talk
CycleQ: an efficient basis for cyclic equational reasoning
PLDI
Eddie Jones University of Bristol, C.-H. Luke Ong University of Oxford, Steven Ramsay University of Bristol
DOI
11:00
20m
Talk
Finding the Dwarf: Recovering Precise Types from WebAssembly Binaries
PLDI
Daniel Lehmann University of Stuttgart, Michael Pradel University of Stuttgart
DOI Pre-print
11:20
20m
Talk
Abstract Interpretation Repair
PLDI
Roberto Bruni University of Pisa, Roberto Giacobazzi University of Verona, Roberta Gori University of Pisa, Francesco Ranzato University of Padova
DOI Pre-print
11:40
20m
Talk
Differential Cost Analysis with Simultaneous Potentials and Anti-potentials
PLDI
Đorđe Žikelić IST Austria, Pauline Bolignano Amazon, Bor-Yuh Evan Chang University of Colorado Boulder & Amazon, Franco Raimondi Amazon & Middlesex University
DOI Pre-print
22:40 - 00:00
AnalysisPLDI at Toucan
22:40
20m
Talk
CycleQ: an efficient basis for cyclic equational reasoning
PLDI
Eddie Jones University of Bristol, C.-H. Luke Ong University of Oxford, Steven Ramsay University of Bristol
DOI
23:00
20m
Talk
Finding the Dwarf: Recovering Precise Types from WebAssembly Binaries
PLDI
Daniel Lehmann University of Stuttgart, Michael Pradel University of Stuttgart
DOI Pre-print
23:20
20m
Talk
Abstract Interpretation Repair
PLDI
Roberto Bruni University of Pisa, Roberto Giacobazzi University of Verona, Roberta Gori University of Pisa, Francesco Ranzato University of Padova
DOI Pre-print
23:40
20m
Talk
Differential Cost Analysis with Simultaneous Potentials and Anti-potentials
PLDI
Đorđe Žikelić IST Austria, Pauline Bolignano Amazon, Bor-Yuh Evan Chang University of Colorado Boulder & Amazon, Franco Raimondi Amazon & Middlesex University
DOI Pre-print