文章基本信息

标题：A Theory AB Toolbox
本地全文：下载
作者：Marco Gaboardi ; Justin Hsu
期刊名称：LIPIcs : Leibniz International Proceedings in Informatics
电子版ISSN：1868-8969
出版年度：2015
卷号：32
页码：129-139
DOI：10.4230/LIPIcs.SNAPL.2015.129
出版社：Schloss Dagstuhl -- Leibniz-Zentrum fuer Informatik
摘要：Randomized algorithms are a staple of the theoretical computer science literature. By careful use of randomness, algorithms can achieve properties that are simply not possible with deterministic algorithms. Today, these properties are proved on paper, by theoretical computer scientists; we investigate formally verifying these proofs. The main challenges are two: proofs about algorithms can be quite complex, using various facts from probability theory; and proofs are highly customized - two proofs of the same property for two algorithms can be completely different. To overcome these challenges, we propose taking inspiration from paper proofs, by building common tools - abstractions, reasoning principles, perhaps even notations - into a formal verification toolbox. To give an idea of our approach, we consider three common patterns in paper proofs: the union bound, concentration bounds, and martingale arguments.
关键词：Verification; randomized algorithms