Indexed and fibered structures for partial and total correctness assertions

DOI10.1017/S0960129522000275MaRDI QIDQ5889306FDOQ5889306

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)

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

zbMATH Keywords

fibrationsHoare logicindexed categoriespartial correctness assertionstotal correctness assertions

Mathematics Subject Classification ID

Computer science (68-XX)

Cites Work

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

Cited In (3)

• Indexed and fibred structures for Hoare logic
• Hoare Logic in the Abstract
• Title not available (Why is that?)

Uses Software

• Dafny
• Isabelle/HOL

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)