Title:A PVS Proof Obligation Generator for Lustre Programs
Authors:Cecile Canovas-Dumas, Paul Caspi 

Abstract:

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.