The axiomatic semantics of programs based on Hoare's logic
From MaRDI portal
Publication:800712
DOI10.1007/BF00264252zbMATH Open0551.68016MaRDI QIDQ800712FDOQ800712
Recommendations
Cites Work
- 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?)
- A PROPERTY OF 2‐SORTED PEANO MODELS AND PROGRAM VERIFICATION
- A complete logic for reasoning about programs via nonstandard model theory. I
- An axiomatic basis for computer programming
- An axiomatic definition of the programming language Pascal
- Axiomatic Definitions of Programming Languages
- CONSTRUCTIVE ALGEBRAS I
- Computable Algebra, General Theory and Theory of Computable Fields
- Consistent and complementary formal theories of the semantics of programming languages
- 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
- 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 (18)
- The B-Book
- Some general incompleteness results for partial correctness logics
- Dijkstra's interpretation of the approach to solving a problem of program correctness
- Title not available (Why is no real title available?)
- Matching logic: an alternative to Hoare/Floyd logic
- Algebraic specifications of computable and semicomputable data types
- AXIOMATIC FRAMEWORKS FOR DEVELOPING BSP-STYLE PROGRAMS∗
- A sound and complete Hoare logic for dynamically-typed, object-oriented programs
- Title not available (Why is no real title available?)
- Indexed and fibered structures for partial and total correctness assertions
- Fuzzy semantics of programming languages
- Forward with Hoare
- Axiomatization of if-then-else over possibly non-halting programs and tests
- Hoare's logic for nondeterministic regular programs: A nonstandard approach
- Title not available (Why is no real title available?)
- Title not available (Why is no real title available?)
- A complete axiomatic semantics of spawning
- The semantics of Hoare's iteration rule
Uses Software
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)
