On Fixpoint/Iteration/Variant Induction Principles for Proving Total Correctness of Programs with Denotational Semantics

DOI10.1007/978-3-030-45260-5_1MaRDI QIDQ5097622zbMATH OpenOpenAlexFDO

Authors Patrick Cousot

Publication date 25 August 2022

Published in Logic-Based Program Synthesis and Transformation (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-030-45260-5_1

zbMATH Keywords

verificationdenotational semanticspartial correctnessinduction principlestotal correctness

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Specification and verification (program logics, model checking, etc.) (68Q60) Semantics in the theory of computing (68Q55)

Cites work

• scientific article; zbMATH DE number 3714908 (Why is no real title available?)
• scientific article; zbMATH DE number 3792232 (Why is no real title available?)
• scientific article; zbMATH DE number 3469999 (Why is no real title available?)
• scientific article; zbMATH DE number 3302923 (Why is no real title available?)
• scientific article; zbMATH DE number 3362972 (Why is no real title available?)
• scientific article; zbMATH DE number 3073037 (Why is no real title available?)
• A Hoare Logic for Call-by-Value Functional Programs
• A closer look at termination
• A lattice-theoretical fixpoint theorem and its applications
• A sound and relatively* complete Hoare-logic for a language with higher type procedures
• An axiomatic basis for computer programming
• Axiomatic approach to total correctness of programs
• Chain-complete posets and directed sets with applications
• Constructive versions of Tarski's fixed point theorems
• Corrigendum: Soundness and Completeness of an Axiom System for Program Verification
• Countable nondeterminism and random assignment
• Fixpoint approach to the theory of computation
• Inductive methods for proving properties of programs
• Programming Language Constructs for Which It Is Impossible To Obtain Good Hoare Axiom Systems
• Size-change termination and transition invariants
• Soundness and Completeness of an Axiom System for Program Verification
• The size-change principle for program termination
• ``A la Burstall intermittent assertions induction principles for proving inevitability properties of programs

Cited in

(3)

• ``A la Burstall intermittent assertions induction principles for proving inevitability properties of programs
• scientific article; zbMATH DE number 7559486 (Why is no real title available?)
• Abstract interpretation of graphs

This page was built for publication: On Fixpoint/Iteration/Variant Induction Principles for Proving Total Correctness of Programs with Denotational Semantics

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