Abstract:
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.

Bibliography

• 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

Slides (.pdf)