Efficient Strongly Relational Polyhedral AnalysisSriram Sankaranarayanan , Michael Colon , Henny Sipma, Zohar Manna |
|
Polyhedral analysis infers invariant linear equalities and
inequalities of imperative programs. However, the exponential
complexity of polyhedral operations such as image computation and
convex hull limits the applicability of polyhedral analysis. Weakly
relational domains such as intervals and octagons address the
scalability issue by considering polyhedra whose constraints are
drawn from a restricted, user-specified class. On the other hand,
these domains rely solely on candidate expressions provided by the
user. Therefore, they often fail to produce strong invariants.
We propose a polynomial time approach to strongly relational analysis. We provide efficient implementations of join and post condition operations, achieving a trade off between performance and accuracy. We have implemented a strongly relational polyhedral analyzer for a subset of the C language. Initial experimental results on benchmark examples are encouraging.
|
| Verification, Model Checking, and Abstract Interpretation (VMCAI 2006), To Appear. |