Continuity Analysis of Programs

9 years 7 months ago
Continuity Analysis of Programs
We present an analysis to automatically determine if a program represents a continuous function, or equivalently, if infinitesimal changes to its inputs can only cause infinitesimal changes to its outputs. The analysis can be used to verify the robustness of programs whose inputs can have small amounts of error and uncertainty-e.g., embedded controllers processing slightly unreliable sensor data, or handheld devices using slightly stale satellite data. Continuity is a fundamental notion in mathematics. However, it is difficult to apply continuity proofs from real analysis to functions that are coded as imperative programs, especially when they use diverse data types and features such as assignments, branches, and loops. We associate data types with metric spaces as opposed to just sets of values, and continuity of typed programs is phrased in terms of these spaces. Our analysis reduces questions about continuity to verification conditions that do not refer to infinitesimal changes and...
Swarat Chaudhuri, Sumit Gulwani, Roberto Lublinerm
Added 01 Mar 2010
Updated 02 Mar 2010
Type Conference
Year 2010
Where POPL
Authors Swarat Chaudhuri, Sumit Gulwani, Roberto Lublinerman
Comments (0)