Continuity Analysis of Programs, Swarat Chaudhuri, Sumit Galwani, and Roberto Lublinerman. POPL 2010.

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 can be discharged using off-the-shelf SMT solvers. Challenges arise in proving continuity of programs with branches and loops, as a small perturbation in the value of a variable often leads to divergent control-flow that can lead to large changes in values of variables. Our proof rules identify appropriate â€œsynchronization pointsâ€ between executions and their perturbed counterparts, and establish that values of certain variables converge back to the original results in spite of temporary divergence.

We prove our analysis sound with respect to the traditional epsilon-delta definition of continuity. We demonstrate the precision of our analysis by applying it to a range of classic algorithms, including algorithms for array sorting, shortest paths in graphs, minimum spanning trees, and combinatorial optimization. A prototype implementation based on the Z3 SMT-solver is also presented.

Another fun paper from POPL this year. I've seen metric spaces used to solve domain equations before, but the idea of actually considering a metric on the outputs was a new one to me.

## Recent comments

5 days 21 hours ago

6 days 16 hours ago

6 days 21 hours ago

6 days 21 hours ago

6 days 22 hours ago

6 days 22 hours ago

6 days 23 hours ago

6 days 23 hours ago

1 week 4 hours ago

1 week 4 hours ago