On the mechanical derivation of loop invariants
- 1 May 1993
- journal article
- Published by Elsevier in Journal of Symbolic Computation
- Vol. 15 (5-6) , 705-744
- https://doi.org/10.1016/s0747-7171(06)80010-6
Abstract
No abstract availableKeywords
This publication has 8 references indexed in Scilit:
- Program verification system with synthesizer of invariant assertionsSystems and Computers in Japan, 1989
- A complete, nonredundant algorithm for reversed SkolemizationTheoretical Computer Science, 1983
- Soundness and Completeness of an Axiom System for Program VerificationSIAM Journal on Computing, 1978
- A New Incompleteness Result for Hoare's SystemJournal of the ACM, 1978
- Property extraction in well-founded property setsIEEE Transactions on Software Engineering, 1975
- A synthesizer of inductive assertionsIEEE Transactions on Software Engineering, 1975
- Assigning meanings to programsPublished by American Mathematical Society (AMS) ,1967
- A Machine-Oriented Logic Based on the Resolution PrincipleJournal of the ACM, 1965