Indexed and fibered structures for partial and total correctness assertions

DOI10.1017/S0960129522000275MaRDI QIDQ5889306zbMATH OpenFDO

Authors A. R. Martini, Edward Hermann Haeusler, Uwe Wolter

Publication date 19 April 2023

Published in Mathematical Structures in Computer Science (Search for Journal in Brave)

Copyright license Creative Commons Attribution 4.0 International

zbMATH Keywords

fibrationsHoare logicindexed categoriespartial correctness assertionstotal correctness assertions

Mathematics Subject Classification ID

Computer science (68-XX)

Recommendations

• Indexed and fibred structures for Hoare logic
• scientific article; zbMATH DE number 1678378
• A general framework for sound and complete Floyd-Hoare logics
• Partial hyperdoctrines: categorical models for partial function logic and Hoare logic
• The axiomatic semantics of programs based on Hoare's logic

Cites work

• scientific article; zbMATH DE number 44976 (Why is no real title available?)
• scientific article; zbMATH DE number 46995 (Why is no real title available?)
• A Relatively Complete Generic Hoare Logic for Order-Enriched Effects
• Categories for Types
• Dafny: an automatic program verifier for functional correctness
• Fibred and Indexed Categories for Abstract Model Theory
• Graded Hoare logic and its categorical semantics
• Guarded commands, nondeterminacy and formal derivation of programs
• Hoare Logic in the Abstract
• Institution-independent model theory
• Institutions: abstract model theory for specification and programming
• Logic in Computer Science
• Partial hyperdoctrines: categorical models for partial function logic and Hoare logic
• Soundness and Completeness of an Axiom System for Program Verification
• Towards a uniform presentation of logical systems by indexed categories and adjoint situations
• Verification of sequential and concurrent programs
• Weakest preconditions in fibrations

Cited in

(3)

• Indexed and fibred structures for Hoare logic
• Hoare Logic in the Abstract
• scientific article; zbMATH DE number 1678378 (Why is no real title available?)

Describes a project that uses

Uses Software

• Isabelle/HOL
• Dafny

This page was built for publication: Indexed and fibered structures for partial and total correctness assertions

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