Verifying programs by induction on their data structure: general format and applications

DOI10.1016/0020-0190(83)90056-XzbMath0513.68014MaRDI QIDQ1050765

Ali Milli

Publication date: 1983

Published in: Information Processing Letters (Search for Journal in Brave)

zbMATH Keywords

program verificationNoetherian inductionintermittent assertion methodsubgoal induction method

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Data structures (68P05)

Related Items

Strongest invariant functions: Their use in the systematic analysis of while statements

Cites Work

• The Universal Field of Fractions of a Semifir I. Numerators and Denominators
• Is Sometimes Ever Better Than Always?
• An axiomatic basis for proving total correctness of goto-programs
• Is “sometime” sometimes better than “always”?
• An axiomatic basis for computer programming
• Formalization of Properties of Functional Programs
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item