Dynamic Partitioning in Linear Relation Analysis. Application to the Verification of Synchronous Programs

Bertrand Jeannet


We apply linear relation analysis [CH78, HPR97] to the verification
of declarative synchronous programs [Hal98]. 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.

Keywords and Phrases: Abstract Interpretation, Partitioning,
Linear Relation Analysis, Reactive Systems, Program Verification

Full Text:


DOI: http://dx.doi.org/10.7146/brics.v7i38.20204
This website uses cookies to allow us to see how the site is used. The cookies cannot identify you or any content at your own computer.

ISSN: 0909-0878 

Hosted by the Royal Danish Library and Aarhus University Library