Write a Blog >>
Sat 25 Jan 2020 15:35 - 16:07 at Orleans - Analysis, verification, blame Chair(s): Niki Vazou

Static verification tools for recursive heap data structures impose significant annotation burden on developers. This is true even when verifying a simple function that inserts an element at the end of a linked list. Gradual verification was introduced to allow developers to deal with this burden incrementally, if at all. It draws from research on gradual typing to produce a verification system that supports imprecise specifications along a continuum. However, current gradual verification technology can only support a simple first-order specification logic. This paper outlines work in progress on an extension to gradual verification that supports implicit dynamic frames and recursive abstract predicates using examples. This paper also highlights challenges and proposes solutions to verifying such examples.

Sat 25 Jan

Displayed time zone: Saskatchewan, Central America change

15:35 - 17:45
Analysis, verification, blameWGT at Orleans
Chair(s): Niki Vazou IMDEA Software Institute
15:35
32m
Talk
Gradual Verification of Recursive Heap Data Structures
WGT
Jenna DiVincenzo (Wise) Carnegie Mellon University, Johannes Bader Facebook, Jonathan Aldrich Carnegie Mellon University, Éric Tanter University of Chile, Joshua Sunshine Carnegie Mellon University
Pre-print
16:07
33m
Talk
Gradual Program Analysis
WGT
Samuel Estep Liberty University, Jenna DiVincenzo (Wise) Carnegie Mellon University, Jonathan Aldrich Carnegie Mellon University, Éric Tanter University of Chile, Johannes Bader Facebook, Joshua Sunshine Carnegie Mellon University
Pre-print
16:40
10m
Break
Minibreak
WGT

16:50
30m
Talk
Blame tracking at higher fidelity
WGT
Jakub Zalewski University of Edinburgh, James McKinna University of Edinburgh, J. Garrett Morris University of Kansas, USA, Philip Wadler University of Edinburgh, UK
Pre-print
17:20
25m
Day closing
Discussion on gradual typing and WGT21
WGT