Lustre program verification: the tool Lesar
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.
KeywordsModel Check State Graph Safety Property Reachable State Boolean Formula
Unable to display preview. Download preview PDF.