Lustre program verification: the tool Lesar

  • Nicolas Halbwachs
Part of the The Springer International Series in Engineering and Computer Science book series (SECS, volume 215)


As noted in the introduction, reactive systems often concern critical applications, and thus program verification is a key issue. However, many practitioners in the field are skeptical about the use of formal verification methods, and convincing arguments need to be provided in order to support the claim that such methods are indeed of practical interest. This is the object of the following discussion.


Model Check State Graph Safety Property Reachable State Boolean Formula 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

Copyright information

© Springer Science+Business Media Dordrecht 1993

Authors and Affiliations

  • Nicolas Halbwachs
    • 1
  1. 1.IMAG InstituteGrenobleFrance

Personalised recommendations