On Fixpoint/Iteration/Variant Induction Principles for Proving Total Correctness of Programs with Denotational Semantics
From MaRDI portal
Publication:5097622
DOI10.1007/978-3-030-45260-5_1zbMath1502.68078OpenAlexW3017851112MaRDI QIDQ5097622
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
Semantics in the theory of computing (68Q55) Specification and verification (program logics, model checking, etc.) (68Q60) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)
Related Items (2)
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- ``A la Burstall intermittent assertions induction principles for proving inevitability properties of programs
- A sound and relatively* complete Hoare-logic for a language with higher type procedures
- A closer look at termination
- Chain-complete posets and directed sets with applications
- Constructive versions of Tarski's fixed point theorems
- Axiomatic approach to total correctness of programs
- A lattice-theoretical fixpoint theorem and its applications
- A Hoare Logic for Call-by-Value Functional Programs
- Countable nondeterminism and random assignment
- Corrigendum: Soundness and Completeness of an Axiom System for Program Verification
- Soundness and Completeness of an Axiom System for Program Verification
- Programming Language Constructs for Which It Is Impossible To Obtain Good Hoare Axiom Systems
- Inductive methods for proving properties of programs
- Size-Change Termination and Transition Invariants
- The size-change principle for program termination
- An axiomatic basis for computer programming
- Fixpoint approach to the theory of computation
This page was built for publication: On Fixpoint/Iteration/Variant Induction Principles for Proving Total Correctness of Programs with Denotational Semantics
