scientific article; zbMATH DE number 1500648

MaRDI QIDQ4501670zbMATH OpenFDO

Authors David von Oheimb

Publication date 7 November 2000

zbMATH Keywords

Hoare logic

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Logic in computer science (03B70)

Recommendations

• scientific article; zbMATH DE number 2110621
• scientific article; zbMATH DE number 1948157
• Automata, Languages and Programming
• scientific article; zbMATH DE number 3900131
• scientific article; zbMATH DE number 3888900

Cited in

(10)

• scientific article; zbMATH DE number 1948157 (Why is no real title available?)
• Structural operational semantics through context-dependent behaviour
• Completeness for recursive procedures in separation logic
• Frame rule for mutually recursive procedures manipulating pointers
• Fifty years of Hoare's logic
• Local variable scoping and Kleene algebra with tests
• Verification conditions for source-level imperative programs
• Deriving a Floyd-Hoare logic for non-local jumps from a formulæ-as-types notion of control
• Process expressions and Hoare's logic: Showing and irreconcilability of context-free recursion with Scott's induction rule
• Scope Logic: An Extension to Hoare Logic for Pointers and Recursive Data Structures

Describes a project that uses

Uses Software

• Isabelle/HOL
• Isabelle

This page was built for publication:

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