Jump to : Note | Abstract | Contact | BibTex reference | EndNote reference |

Note on this paper

available at http://ipsapp008.kluweronline.com/ips/frames/toc.asp?J=4715&I=39

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
Bertrand.Jeannet@irisa.fr

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)