**Date: **
Tuesday, December 13, 2011

**Speaker: **
Azadeh Farzan

**Venue: **IST Austria

Applications in many different areas of computer science are required to make discrete decisions under uncertainty. Under uncertainty, the individual decisions made by a program are inevitably nondeterministic. A serious implication of this is that the decisions made by the program at different points of an execution may not even be consistent with each other. As a result, a program that is otherwise correct may execute along paths that would not be executed {em on any input} in the program’s usual semantics, and violate essential program invariants on the way.The property of em robustness asserts that a decision-making program does not suffer from the above kind of violations. In this paper, we present a program analysis to verify that a program P is robust in this sense. Our analysis constructs a decision monitor that observes the decisions made along executions of P and derives every corollary of these decisions. The problem of proving P robust is reduced to assertion checking in the product of P and this monitor.We apply our analysis to the domain of geometric computations, where typical programs make boolean decisions in the presence of numerical uncertainty. Robustness is known to be a critical and frequently-violated correctness property in this domain—for example, violation of robustness can cause everyday algorithms for computing convex hulls or triangulations to crash, go into infinite loops, or violate essential postconditions. While there is alarge body of work on robust geometric computation, ours is the first attempt at static verification of robustness of geometric programs. An evaluation using a suite of well-known geometric algorithms demonstrates the utility of our method.