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
Times are displayed in time zone: (GMT-06:00) Saskatchewan, Central America change

15:35 - 17:45: WGT - Analysis, verification, blame at Orleans
Chair(s): Niki VazouIMDEA Software Institute
wgt-2020-papers15:35 - 16:07
Jenna WiseCarnegie Mellon University, Johannes BaderFacebook, Jonathan AldrichCarnegie Mellon University, Éric TanterUniversity of Chile, Joshua SunshineCarnegie Mellon University
wgt-2020-papers16:07 - 16:40
Samuel EstepLiberty University, Jenna WiseCarnegie Mellon University, Jonathan AldrichCarnegie Mellon University, Éric TanterUniversity of Chile, Johannes BaderFacebook, Joshua SunshineCarnegie Mellon University
wgt-2020-papers16:40 - 16:50
wgt-2020-papers16:50 - 17:20
Jakub ZalewskiUniversity of Edinburgh, James McKinnaUniversity of Edinburgh, J. Garrett MorrisUniversity of Kansas, USA, Philip WadlerUniversity of Edinburgh, UK
wgt-2020-papers17:20 - 17:45
Day closing