B. Jeannet. Dynamic Partitioning In Linear Relation Analysis. Application To The Verification Of Reactive Systems. Formal Methods in System Design, 23(1):5-37, July 2003.
We apply linear relation analysis 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 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
Bertrand Jeannet http://pop-art.inrialpes.fr/people/bjeannet/
@article{jeannet03a,
Author = {Jeannet, B.},
Title = {Dynamic Partitioning In Linear Relation Analysis. Application To The Verification Of Reactive Systems},
Journal = {Formal Methods in System Design},
Volume = {23},
Number = {1},
Pages = {5--37},
Publisher = {Kluwer},
Month = {July},
Year = {2003}
}
Get EndNote Reference (.ref)