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

DOI10.1016/0020-0190(83)90056-XzbMATH Open0513.68014MaRDI QIDQ1050765FDOQ1050765

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

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

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)