Continuity and robustness of programs

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.

References

1. Bucker, M., Corliss, G., Hovland, P., Naumann, U., Norris, B. Automatic Differentiation: Applications, Theory and Implementations, Birkhauser, 2006.
2. Chaudhuri, S., Gulwani, S., Lublinerman, R. Continuity analysis of programs. In POPL (2010), 57--70.
3. Chaudhuri, S., Gulwani, S., Lublinerman, R., Navidpour, S. Proving programs robust. In FSE (2011), 102--112.
4. Chaudhuri, S., Solar-Lezama, A. Smooth interpretation. In PLDI (2010), 279--291.
5. Chaudhuri, S., Solar-Lezama, A. Smoothing a program soundly and robustly. In CAV (2011), 277--292.
6. Chen, L., Miné, A., Wang, J., Cousot, P. Interval polyhedra: An abstract domain to infer interval linear relationships. In SAS (2009), 309--325.
7. Cousot, P., Cousot, R., Feret, J., Mauborgne, L., Miné, A., Monniaux, D., Rival, X. The ASTREÉ analyzer. In ESOP (2005), 21--30.
8. de Moura, L. M. Bjørner, N. Z3: An effcient smt solver. In TACAS (2008), 337--340.
9. Girard, A., Pappas, G. Approximate bisimulation: A bridge between computer science and control theory. Eur. J. Contr. 17, 5 (2011), 568.
10. Goubault, E. Static analyses of the precision of floating-point operations. In SAS (2001).
11. Gulwani, S., Zuleger, F. The reachability-bound problem. In PLDI (2010), 292--304.
12. Hamlet, D. Continuity in software systems. In ISSTA (2002).
13. Jha, M., Raskhodnikova, S. Testing and reconstruction of lipschitz functions with applications to data privacy. In FOCS (2011), 433--442.
14. Majumdar, R., Saha, I. Symbolic robustness analysis. In RTSS (2009), 355--363.
15. Parnas, D. Software aspects of strategic defense systems. Commun. ACM 28, 12 (1985), 1326--1335.
16. Pettersson, S., Lennartson, B. Stability and robustness for hybrid systems. In Decision and Control (Dec 1996), 1202--1207.
17. Podelski, A., Wagner, S. Model checking of hybrid systems: From reachability towards stability. In HSCC (2006), 507--521.
18. Reed, J., Pierce, B. Distance makes the types grow stronger: A calculus for differential privacy. In ICFP (2010).
19. Strichman, O. Regression verification: Proving the equivalence of similar programs. In CAV (2009).
20. Zhu, Z., Misailovic, S., Kelner, J., Rinard, M. Randomized accuracy-aware program transformations for efficient approximate computations. In POPL (2012).

Index Terms

• Theory of computation

  • Logic

  • Semantics and reasoning

    • Program reasoning

    • Program semantics