[Invited Talk] Completeness Thresholds for Memory Safety: Unbounded Guarantees Via Bounded Proofs

Bounded proofs are convenient to use due to the high degree of automation that exhaustive checking affords. However, they fall short of providing the robust assurances offered by unbounded proofs. In this invited talk, we sketch how completeness thresholds serve as a bridge, allowing us to derive unbounded guarantees from bounded proofs. Using a bubble sort implementation as example, we demonstrate that a bounded proof only needs to consider a few specific inputs to yield unbounded guarantees.

[Slides]

This invited talk was part of an invited research visit of the Programming Group @ HSG, St Gallen in Switzerland.

Our research on completeness thresholds for program verification is part of an ongoing project. For more information, check out my dissertation and our other publications:

• [Dissertation]
  Semi-Automated Modular Formal Verification of Critical Software: Liveness and Completeness Thresholds,
  KU Leuven 2024
  [Lirias (KU Leuven)] [arXiv]
• [Poster]
  Completeness Thresholds for Memory Safety: Unbounded Guarantees Via Bounded Proofs
  SPLASH 2023
  [Zenodo]
• [Extended Abstract]
  Completeness Thresholds for Memory Safety: Unbounded Guarantees via Bounded Proofs
  arXiv 2023
  [arXiv]
• [Paper] Completeness Thresholds for Memory Safety of Array Traversing Programs
  SOAP 2023
  [ACM] / [arXiv]
• [Technical Report]
  Completeness Thresholds for Memory Safety of Array Traversing Programs: Early Technical Report
  arXiv 2023
  [arXiv]