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

DOI10.1007/978-3-030-45260-5_1zbMATH Open1502.68078OpenAlexW3017851112MaRDI QIDQ5097622FDOQ5097622

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

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

Cited In (3)

• ``A la Burstall intermittent assertions induction principles for proving inevitability properties of programs
• Title not available (Why is that?)
• 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)