A PVS Proof Obligation Generator for Lustre Programs
7th International Conference on Logic for Programming and Reasonning,
LPAR2000, La Réunion, November 2000
This paper presents a tool for proving safety properties of Lustre
programs in PVS, based on continuous induction. The tool applies off-line
a repeated induction strategy and generates proof obligations left to PVS.
We show on examples how it avoids some drawbacks of co-induction which
needs to consider ``absent elements'' in the case of clocked streams.
@InProceedings{lpar,
author = {C. Dumas and P. Caspi},
title = {A {P}{V}{S} Proof Obligation Generator for {L}ustre
Programs},
booktitle = {7th International Conference on Logic for
Programming and Automated Reasoning },
year = 2000,
volume = 1955,
series = {Lecture Notes in Artificial Intelligence}
}
Postscript