loops. Soon after our first paper on this topic (and before
our subsequent work on Lipschitz continuity of programs), Reed and Pierce18 gave a type system that can verify the Lipschitz continuity of functional programs. This
system can seamlessly handle functional data structures
such as lists and maps; however, unlike our method, it
cannot reason about discontinuous control flow, and
would consider any program with a conditional branch
to have a Lipschitz constant of ∞.
More recently, Jha and Raskhodnikova have taken a
property testing approach to estimating the Lipschitz constant
of a program. Given a program, this method determines,
with a level of probabilistic certainty, whether it is either
1-Lipschitz or -far (defined in a suitable way) from being
1-Lipschitz. While the class of programs allowed by the
method is significantly more restricted than what is investigated here or by Reed and Pierce 13, the appeal of the method
lies in its crisp completeness guarantees, and also in that it
only requires blackbox access to the program.
Robustness is a standard correctness property in control
theory, 16, 17 and there is an entire subfield of control studying the design and analysis of robust controllers. However,
the systems studied by this literature are abstractly defined
using differential equations and hybrid automata rather
than programs. The systematic modeling and analysis of
robustness of programs was first proposed by us in the context of general software, and by Majumdar and Saha14 in the
context of control software.
In addition, there are many efforts in the abstract interpretation literature that, while not verifying continuity or
robustness explicitly, reason about the uncertainty in a program’s behavior due to floating-point rounding and sensor
errors. 6, 7, 10 Other related literature includes work on automatic differentiation (AD), 1 where the goal is to transform
a program P into a program that returns the derivative of P
where it exists. Unlike the work described here, AD does not
attempt verification—no attempt is made to certify a program as differentiable or Lipschitz.
In this paper, we have argued for the adoption of analytical properties like continuity and Lipschitz continuity
as correctness properties of programs. These properties
are relevant as they can serve as useful definitions of
robustness of programs to uncertainty. Also, they raise
some fascinating technical issues. Perhaps counterin-tuitively, some of the classic algorithms of computer
science satisfy continuity or Lipschitz continuity, and
the problem of systematic reasoning about these properties demands a nontrivial combination of analytical
and logical insights.
We believe that the work described here is a first step
toward an extension of the classical calculus to a symbolic
mathematics where programs form a first-class represen-
tation of functions and dynamical systems. From a practi-
cal perspective, this is important as physical systems are
increasingly controlled by software, and as even applied
mathematicians increasingly reason about functions that
are not written in the mathematical notation of textbooks,
but as code. Speaking more philosophically, the classical
calculus focuses on the computational aspects of real anal-
ysis, and the notation of calculus texts has evolved primar-
ily to facilitate symbolic computation by hand. However, in
our era, most mathematical computations are carried out
by computers, and a calculus for our age should not ignore
the notation that computers can process most easily: pro-
grams. This statement has serious implications—it opens
the door not only to the study of continuity or derivatives
but also to, say, Fourier transforms, differential equations,
and mathematical optimization of code. Some efforts in
these directions4, 5, 9 are already under way; others will no
doubt appear in the years to come.
This research was supported by NSF CAREER Award
#1156059 (“Robustness Analysis of Uncertain Programs:
Theory, Algorithms, and Tools”).
1. bucker, m., Corliss, g., hovland, p.,
naumann, u., norris, b. automatic
Differentiation: applications, theory
and Implementations, birkhauser,
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
4. Chaudhuri, s., solar-lezama, a.
smooth interpretation. In PLDI
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),
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),
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).
Swarat Chaudhuri ( firstname.lastname@example.org),
Department of Computer science, rice
university, houston, tX.
Sumit Gulwani ( email@example.com),
microsoft research, redmond, Wa.
11. gulwani, s., Zuleger, f. the
reachability-bound problem. In PLDI
12. hamlet, D. Continuity in software
systems. In ISS TA (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),
15. parnas, D. software aspects of
strategic defense systems.
Commun. ACM 28, 12 (1985),
16. pettersson, s., lennartson, b. stability
and robustness for hybrid systems.
In Decision and Control (Dec 1996),
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
19. strichman, o. regression
verification: proving the equivalence
of similar programs. In CAV
20. Zhu, Z., misailovic, s., kelner, j.,
rinard, m. randomized accuracy-aware program transformations for
efficient approximate computations.
In POPL (2012).
Roberto Lublinerman ( firstname.lastname@example.org),
Department of Computer science and
engineering, pennsylvania state university,
university park, pa.