期刊
COMMUNICATIONS OF THE ACM
卷 55, 期 8, 页码 107-115出版社
ASSOC COMPUTING MACHINERY
DOI: 10.1145/2240236.2240262
关键词
-
类别
资金
- NSF CAREER Award [1156059]
- Division of Computing and Communication Foundations
- Direct For Computer & Info Scie & Enginr [1156059] Funding Source: National Science Foundation
Computer scientists have long believed that software is different from physical systems in one fundamental way: while the latter have continuous dynamics, the former do not. In this paper, we argue that notions of continuity from mathematical analysis are relevant and interesting even for software. First, we demonstrate that many everyday programs are continuous (i.e., arbitrarily small changes to their inputs only cause arbitrarily small changes to their outputs) or Lipschitz continuous (i.e., when their inputs change, their outputs change at most proportionally). Second, we give an mostly-automatic framework for verifying that a program is continuous or Lipschitz, showing that traditional, discrete approaches to proving programs correct can be extended to reason about these properties. An immediate application of our analysis is in reasoning about the robustness of programs that execute on uncertain inputs. In the longer run, it raises hopes for a toolkit for reasoning about programs that freely combines logical and analytical mathematics.
作者
我是这篇论文的作者
点击您的名字以认领此论文并将其添加到您的个人资料中。
推荐
暂无数据