Software Research Seminar: Talk 2

  • Newell-Simon Hall
  • Mauldin Auditorium 1305
  • Ph.D. Student
  • Ph.D. Program in Software Engineering, Institute for Software Research
  • Carnegie Mellon University

Gradual Verification of Recursive Heap Data Structures

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. Our work extends the prior approach to gradual verification to support the specification and verification of programs that use basic recursive data structures like trees or lists. This talk outlines work in progress on this extension and highlights research challenges and proposes solutions to them. 

For More Information, Please Contact: