Completeness Thresholds for Memory Safety: Unbounded Guarantees via Bounded Proofs (Extended Abstract)

Tobias ReinhardJustus FasseBart Jacobs

Sep 2023

0被引用

0笔记

开学季活动火爆进行中，iPad、蓝牙耳机、拍立得、键盘鼠标套装等你来拿

摘要原文

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. 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.

展开全部

机器翻译

AI理解论文&经典十问