Guest Talk: Completeness Thresholds for Memory Safety

You are all invited to this guest lecture.

Title: Completeness Thresholds for Memory Safety: Unbounded Guarantees via Bounded Proofs
Speaker: Tobias Reinhard, TU Darmstadt, Germany
Time: Tue 21 May @ 11:05
Place: Seminarrom Perl

Abstract:
We present the first study of completeness thresholds (CTs) for infinite state systems.
Any bounded proof reaching its CT is sound. Thereby, CTs allow us to reduce unbounded proofs to bounded ones.
Specifically, we focus on memory safety proofs for programs that iterate over arbitrarily large data structures in a memory-layout-preserving way. Meanwhile, many of the results straightforwardly apply to arbitrary correctness properties.
We present a generic approach to extract CTs from a program's verification condition and show that it scales. Moreover, we demonstrate that we can characterise CTs for interesting classes of array traversing programs.