Blogs (1) >>
POPL 2019
Sun 13 - Sat 19 January 2019 Cascais, Portugal
Fri 18 Jan 2019 15:43 - 16:05 at Sala II - Program Analysis I Chair(s): Michael D. Adams

We introduce the abstract domain of correlations to denote equality relations between parts of inputs and outputs of programs. We formalise the theory of correlations, and mechanically verify their semantic properties. We design a static inter-procedural dataflow analysis for automatically inferring correlations for programs written in a first-order language equipped with algebraic data-types and arrays. The analysis, its precision and execution cost, have been evaluated on the code and functional specification of an industrial-size micro-kernel. We exploit the inferred correlations to automatically discharge two thirds of the proof obligations related to the preservation of invariants for this micro-kernel.

Slides (popl19_talk.pdf)553KiB

Fri 18 Jan

Displayed time zone: Belfast change

15:21 - 16:27
Program Analysis IResearch Papers at Sala II
Chair(s): Michael D. Adams University of Utah
15:21
22m
Talk
Decidable Verification of Uninterpreted Programs
Research Papers
Umang Mathur University of Illinois at Urbana-Champaign, P. Madhusudan University of Illinois at Urbana-Champaign, Mahesh Viswanathan University of Illinois at Urbana-Champaign
Link to publication DOI Pre-print Media Attached File Attached
15:43
22m
Talk
Inferring Frame Conditions with Static Correlation Analysis
Research Papers
Oana-Fabiana Andreescu Internet of Trust, Thomas P. Jensen INRIA Rennes, Stéphane Lescuyer Prove & Run, Benoît Montagu Prove & Run
Link to publication DOI Pre-print Media Attached File Attached
16:05
22m
Talk
Context-, Flow- and Field-Sensitive Data-Flow Analysis using Synchronized Pushdown SystemsDistinguished Paper
Research Papers
Johannes Späth Fraunhofer IEM, Karim Ali University of Alberta, Eric Bodden Heinz Nixdorf Institut, Paderborn University and Fraunhofer IEM
Link to publication DOI Pre-print Media Attached File Attached