jeannet00b

B. Jeannet. partitionnement Dynamique dans l'Analyse de Relations Linéraires et Application à la Vérification de Programmes Synchrones. PhD Thesis Institut National Polytechnique de Grenoble, September 2000.

Download [help]

Download paper: Gziped Postscript

Copyright notice: This material is presented to ensure timely dissemination of scholarly and technical work. Copyright and all rights therein are retained by authors or by other copyright holders. All persons copying this information are expected to adhere to the terms and constraints invoked by each author's copyright. These works may not be reposted without the explicit permission of the copyright holder.
This page is automatically generated by bib2html v216, © INRIA 2002-2007, Projet Lagadic

Abstract

This works deals with the verification by algorithmic methods of safety properties of synchronous systems, or more generally reactive systems, that exhibit both Boolean and numerical aspects. It proposes an original technique that allows the size of verified systems to be noticeably augmented. We first recall the theoretical framework we use, which is the abstract interpretation theory, and one of its applications, the linear relation analysis, that discovers linear relations linking numerical variables of a program in each of its control points. This analysis was applied to the verification of numerical synchronous programs and linear hybrid systems. In this context, two problems arise: the first one is that the explicit control structure of these systems is often of prohibitive size, and the second one is that the analysis is not precise enough for the proof of some properties. These two problems are in fact related, and we propose a solution to obtain a suitable tradeoff between complexity and precision. We use an abstract domain combining Boolean and numerical properties, and we exploit a control structure to adjust the precision of the analysis. The analysis uses the property to be proved in order to automatically refine an initial rough control structure, until the obtained precision enables the proof of the property. A verification tool based on these principles was implemented and experimented on several and significative examples, some of which being unaffordable with other automatic verification techniques

Contact

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

BibTex Reference

@PhdThesis{jeannet00b,
   Author = {Jeannet, B.},
   Title = {partitionnement Dynamique dans l'Analyse de Relations Linéraires et Application à la Vérification de Programmes Synchrones},
   School = {Institut National Polytechnique de Grenoble},
   Month = {September},
   Year = {2000}
}

EndNote Reference [help]

Get EndNote Reference (.ref)