On the mechanical derivation of loop invariants

DOI10.1016/S0747-7171(06)80010-6zbMath0804.68129OpenAlexW2093349003MaRDI QIDQ1322851

Ritu Chadha, David Alan Plaisted

Publication date: 12 January 1995

Published in: Journal of Symbolic Computation (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/s0747-7171(06)80010-6

zbMATH Keywords

iterative algorithmresolutionloop invariantsflowchart programpartial correctness of programsunskolemization

Mathematics Subject Classification ID

Related Items (3)

Automatic generation of invariants and intermediate assertions ⋮ On Interpolation in Decision Procedures ⋮ On interpolation in automated theorem proving

Cites Work

• Un-Skolemizing clause sets
• A complete, nonredundant algorithm for reversed Skolemization
• Invariance and non-determinacy
• Mechanical proofs about computer programs
• A New Incompleteness Result for Hoare's System
• Soundness and Completeness of an Axiom System for Program Verification
• A Machine-Oriented Logic Based on the Resolution Principle
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: On the mechanical derivation of loop invariants