| Faculty name: | Azadeh Farzan |
|---|---|
| Research area: | Formal Methods and Geometric Algorithms |
| Campus address: | BA 3252 |
| Campus phone: | (416) 946-3983 |
| Email address: |
azadeh [at] cs.toronto.edu
|
| Number of students: | 1 |
| Skills required: |
|
This project attempts to formalize the "robustness" problem for algorithms that use imprecise computations, such as using floating point variables, and make discrete decisions based on the results of those computations. Since these computations over floating point values are very error-prone (effects of rounding, and other limitations of having a limited amount of bits to represent a real number in a computer), these decisions are effectively made with some amount of "uncertainty". 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 on any input in the program's usual semantics, and violate essential program invariants on the way.
The property of robustness asserts that a decision-making program does not suffer from the above kind of violations. Our goal is to develop techniques to test and verify a program P for robustness in this sense. We focus our attention to the domain of geometric computations, where typical programs make boolean decisions in the presence of numerical uncertainy. 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. Or, as another example, almost any "ray tracing" code that is written in a computer graphics text book will not properly execute if it is implemented as it is written in the book, since special considerations have to be made to take care of floating point-related errors.
If you are interested in working on a very new and fresh problem, which brings two or more subareas of computer science together, this is the project for you. A knowledge of logic, automata theory, compilers, graphics and geometric computations, and most importantly good programming will be very helpful.