Mathematical Analysis of Programs

Опубликовано 6 сентября 2016, 5:31

Numerical programs are imperative programs over integer and real quantities. Such programs are ubiquitous. Common examples include scientific and systems programs, models of control systems such as timed and hybrid automata, and models of biological systems such as biochemical reaction mechanisms and gene regulatory networks. Static analyses of these programs automatically infer properties about the systems' runtime behaviours, for example, the reachability of a target set of states, deadlock freedom, and bounds on variables. In this talk, I demonstrate powerful analyses for both linear and nonlinear numerical programs using computational tools from algebra and geometry. I first consider analyses for linear systems. Traditional polyhedra-based analyses do not scale due to the high complexity of polyhedral operations. I present a scalable polynomial time analysis that works by posing many linear programming queries, which can be solved by algorithms such as Simplex. The resulting analysis is precise and scales well on benchmark examples. Next, I present an analysis for nonlinear systems. Using computational tools from algebraic geometry such as Groebner bases, the method infers invariants for many classes of nonlinear systems, including hybrid systems. I demonstrate the technique and its applications on a few examples.