The axiomatic semantics of programs based on Hoare's logic
From MaRDI portal
(Redirected from Publication:800712)
Recommendations
Cites work
- A complete logic for reasoning about programs via nonstandard model theory. I
- A PROPERTY OF 2‐SORTED PEANO MODELS AND PROGRAM VERIFICATION
- An axiomatic basis for computer programming
- An axiomatic definition of the programming language Pascal
- Axiomatic Definitions of Programming Languages
- Computable Algebra, General Theory and Theory of Computable Fields
- Consistent and complementary formal theories of the semantics of programming languages
- CONSTRUCTIVE ALGEBRAS I
- Expressiveness and the completeness of Hoare's logic
- Floyd's principle, correctness theories and program equivalence
- Guarded commands, nondeterminacy and formal derivation of programs
- Hoare's logic and Peano's arithmetic
- Hoare's logic for programming languages with two data types
- scientific article; zbMATH DE number 3686759 (Why is no real title available?)
- scientific article; zbMATH DE number 3707731 (Why is no real title available?)
- scientific article; zbMATH DE number 3722069 (Why is no real title available?)
- scientific article; zbMATH DE number 3729430 (Why is no real title available?)
- scientific article; zbMATH DE number 3742589 (Why is no real title available?)
- scientific article; zbMATH DE number 3755858 (Why is no real title available?)
- scientific article; zbMATH DE number 192929 (Why is no real title available?)
- scientific article; zbMATH DE number 3574936 (Why is no real title available?)
- scientific article; zbMATH DE number 3632451 (Why is no real title available?)
- scientific article; zbMATH DE number 3448070 (Why is no real title available?)
- Infinite proof rules for loops
- Proof rules for the programming language Euclid
- Some natural structures which fail to possess a sound and decidable Hoare-like logic for their while-programs
- Soundness and Completeness of an Axiom System for Program Verification
- Specifying the Semantics of while Programs: A Tutorial and Critique of a Paper by Hoare and Lauer
- Ten Years of Hoare's Logic: A Survey—Part I
- Two theorems about the completeness of Hoare's logic
Cited in
(20)- The semantics of Hoare's iteration rule
- Algebraic specifications of computable and semicomputable data types
- Some general incompleteness results for partial correctness logics
- Axiomatic semantics for escape statements
- Hoare's logic for nondeterministic regular programs: A nonstandard approach
- Towards reasoning about Hoare relations
- A sound and complete Hoare logic for dynamically-typed, object-oriented programs
- Fuzzy semantics of programming languages
- Matching logic: an alternative to Hoare/Floyd logic
- Forward with Hoare
- scientific article; zbMATH DE number 3848601 (Why is no real title available?)
- scientific article; zbMATH DE number 4058826 (Why is no real title available?)
- scientific article; zbMATH DE number 4068250 (Why is no real title available?)
- scientific article; zbMATH DE number 4106262 (Why is no real title available?)
- The B-Book
- AXIOMATIC FRAMEWORKS FOR DEVELOPING BSP-STYLE PROGRAMS∗
- Dijkstra's interpretation of the approach to solving a problem of program correctness
- Axiomatization of if-then-else over possibly non-halting programs and tests
- Indexed and fibered structures for partial and total correctness assertions
- A complete axiomatic semantics of spawning
This page was built for publication: The axiomatic semantics of programs based on Hoare's logic
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q800712)
