Dynamic Partitioning in Linear Relation Analysis: Application to the
Verification of Synchronous Programs
Bertrand Jeannet December 2000 |
Abstract:
Linear relation analysis is an abstract interpretation
technique that computes linear constraints satisfied by the numerical
variables of a program. We apply it to the verification of declarative
synchronous programs. In this approach, state partitioning plays an
important role: on one hand the precision of the results highly depends on
the fineness of the partitioning; on the other hand, a too much detailed
partitioning may result in an exponential explosion of the analysis. In this
paper we propose to consider very general partitions of the state space and
to dynamically select a suitable partitioning according to the property to be
proved. The presented approach is quite general and can be applied to other
abstract interpretations
Available as PostScript, PDF. |