jeannet03a

B. Jeannet. Dynamic Partitioning In Linear Relation Analysis. Application To The Verification Of Reactive Systems. Formal Methods in System Design, available at http://ipsapp008.kluweronline.com/ips/frames/toc.asp?J=4715&I=39, 23(1):5-37, July 2003.

Abstract

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

Contact

Bertrand Jeannet http://www.irisa.fr/prive/bjeannet

BibTex Reference

@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}
}

EndNote Reference [help]

Get EndNote Reference (.ref)