Access Restriction

Author Chaudhuri, Swarat ♦ Lublinerman, Roberto ♦ Gulwani, Sumit
Source ACM Digital Library
Content type Text
Publisher Association for Computing Machinery (ACM)
File Format PDF
Language English
Abstract 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.
Description Affiliation: Microsoft Research, Redmond, WA (Gulwani, Sumit) || Pennsylvania State University, University Park, PA (Lublinerman, Roberto) || Rice University, Houston, TX (Chaudhuri, Swarat)
Age Range 18 to 22 years ♦ above 22 year
Educational Use Research
Education Level UG and PG
Learning Resource Type Article
Publisher Date 2005-08-01
Publisher Place New York
Journal Communications of the ACM (CACM)
Volume Number 55
Issue Number 8
Page Count 9
Starting Page 107
Ending Page 115

Open content in new tab

   Open content in new tab
Source: ACM Digital Library