ETAPS 2019
Sat 6 - Thu 11 April 2019 Prague, Czech Republic
Thu 11 Apr 2019 11:00 - 11:30 at SUN II - Program Analysis and Automated Verification Chair(s): Stephanie Balzer

We present an abstract domain able to infer invariants on programs manipulating trees. Trees considered in the article are defined over a finite alphabet and can contain unbounded numeric values at their leaves. Our domain can infer the possible shapes of the tree values of each variable and find numeric relations between: the values at the leaves as well as the size and depth of the tree values of different variables. The abstract domain is described as a product of (1) a symbolic domain based on a tree automata representation and (2) a numerical domain lifted, for the occasion, to describe numerical maps with potentially infinite and heterogeneous definition set. In addition to abstract set operations and widening we define concrete and abstract transformers on these environments. We present possible applications, such as the ability to describe memory zones, or track symbolic equalities between program variables. We implemented our domain in a static analysis platform and present preliminary results analyzing a tree-manipulating toy-language.

Thu 11 Apr
Times are displayed in time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

10:30 - 12:30: Program Analysis and Automated VerificationESOP at SUN II
Chair(s): Stephanie BalzerCarnegie Mellon University
10:30 - 11:00
Talk
Data-Races and Static Analysis for Interrupt-Driven Kernels
ESOP
Link to publication
11:00 - 11:30
Talk
An abstract domain for trees with numeric relations
ESOP
Matthieu Journault, Antoine MinéUPMC, France, Abdelraouf OuadjaoutSorbonne Université
Link to publication
11:30 - 12:00
Talk
A static higher-order dependency pair framework
ESOP
Carsten FuhsBirkbeck, University of London, Cynthia KopRadboud University Nijmegen
Link to publication
12:00 - 12:30
Talk
Coinduction in Uniform: Foundations for Corecursive Proof Search with Horn Clauses
ESOP
Henning BasoldCNRS & ENS Lyon, Ekaterina KomendantskayaHeriot-Watt University, UK, Yue LiHeriot-Watt University, UK
Link to publication