Mathematical Techniques for Program Analysis

Systematic reasoning about a program's runtime behavior requires
specific knowledge of the numbers and numerical operations within the
program. The necessary information includes invariants, ranking
functions, and pre-/post-conditions. We demonstrate novel techniques
for program analysis based on algorithms using convex polyhedra,
optimization, and algebraic geometry to infer facts about a given
program automatically, and in a sound manner. The application of
these techniques, in practice, to detect run-time errors in C/C++
programs such as buffer overflows, null-pointer dereferences, C string
usage, memory leaks, floating point errors, race conditions, and other
user-defined properties will be presented.

Subsequently, we present techniques for the analysis of cyber-physical
control systems, wherein a software-based discrete controller
interacts with a continuously evolving physical environment. These
systems are common in domains such as automobiles, health care,
avionics, and space systems. We demonstrate techniques to analyze
continuous dynamical systems, defined by means of ordinary differential
equations, and also hybrid systems that combine discrete and
continuous state transformations. We conclude by presenting our recent
experiences on applying these techniques to the analysis of
Simulink/Stateflow(tm) diagrams.
Sriram Sankaranarayanan is currently a researcher in computer
science at NEC Laboratories America in Princeton, NJ. His research
focuses on the analysis of programs using mathematical techniques from
algebra, geometry and optimization, and statistical techniques
including sampling, estimation, and machine
learning. Dr. Sankaranarayanan received his PhD from Stanford
University in 2005. He is the recipient of
awards including the NEC technology commercialization award (NEC Labs,
2007), Siebel Scholarship (Stanford University, 2005), and the
President's Gold Medal (Indian Inst. of Technology, Kharagpur, 2000)