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

DOI10.1016/0020-0190(83)90056-XMaRDI QIDQ1050765zbMATH OpenFDO

Authors Ali Mili

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

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

Cites work

• scientific article; zbMATH DE number 3469999 (Why is no real title available?)
• scientific article; zbMATH DE number 3564287 (Why is no real title available?)
• scientific article; zbMATH DE number 3566126 (Why is no real title available?)
• scientific article; zbMATH DE number 3430635 (Why is no real title available?)
• scientific article; zbMATH DE number 3302923 (Why is no real title available?)
• scientific article; zbMATH DE number 3366464 (Why is no real title available?)
• scientific article; zbMATH DE number 3424017 (Why is no real title available?)
• An axiomatic basis for computer programming
• An axiomatic basis for proving total correctness of goto-programs
• Formalization of Properties of Functional Programs
• Is Sometimes Ever Better Than Always?
• Is “sometime” sometimes better than “always”?
• The Universal Field of Fractions of a Semifir I. Numerators and Denominators

Cited in

(1)

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

This page was built for publication: Verifying programs by induction on their data structure: general format and applications

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1050765)