Proving Invariants: How Many Times a System Should Be Unfolded?
Centre Equation 2, av. de Vignate, 38610 Gieres, FRANCE
We present the problem of proving invariant properties of
closed systems. An induction-based proof technique is proposed,
parameterized by an easy-to-find characteristic of the system. We
present a real-world example which is significantly easier to prove
by our technique than by classical ones. We conclude by inspecting
possible future developments.
- C. Dumas and P. Caspi, A PVS Proof Obligation Generator for Lustre Programs, 7th International Conference on Logic for Programming and Automated Reasoning, 2000, in Lecture Notes in Artificial Intelligence vol. 1955
- P.S. Miner and S.D. Johnson, Verification of an Optimized Fault-Tolerant Clock Synchronization Circuit, in Designing Correct Circuits, M. Sheeran and S. Singh editors, 1996, Springer-Verlag, Electronic Workshops in Computing