Scalable Analysis of Linear Systems using Mathematical ProgrammingSriram Sankaranarayanan , Henny Sipma, Zohar Manna |
|
We present a method for generating linear invariants for large
systems. The method performs forward propagation in an abstract domain
consisting of arbitrary polyhedra of a predefined fixed shape. The basic
operations on the domain like abstraction, intersection, join and
inclusion tests are all posed as linear optimization queries, which can be
solved efficiently by existing LP solvers. The number and dimensionality
of the LP queries are polynomial in the program dimensionality, size and
the number of target invariants. The method generalizes similar analyses
in the interval, octagon, and octahedra domains, without resorting to
polyhedral manipulations. We demonstrate the performance of our method on
some benchmark programs.
|
| Verification, Model Checking, and Abstract Interpretation (VMCAI 2005), Volume 3385 of Lecture Notes in Computer Science, pages 21-47. |
| © 2005, Springer Verlag |
| Our prototype is available from here. |