Open AccessDynamic Partitioning in Linear Relation Analysis. Application to the Verification of Synchronous Programs
Author(s) -
Bertrand Jeannet
Publication year - 2000
Publication title -
brics report series
Language(s) - English
Resource type - Journals
eISSN - 1601-5355
pISSN - 0909-0878
DOI - 10.7146/brics.v7i38.20204
Subject(s) - relation (database) , computer science , property (philosophy) , exponential function , algorithm , abstract interpretation , state (computer science) , interpretation (philosophy) , mathematics , theoretical computer science , programming language , data mining , mathematical analysis , philosophy , epistemology
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