Automatic program verification. I: A logical basis and its implementation
From MaRDI portal
Cites work
- An axiomatic basis for computer programming
- An axiomatic definition of the programming language Pascal
- scientific article; zbMATH DE number 3291623 (Why is no real title available?)
- scientific article; zbMATH DE number 3349334 (Why is no real title available?)
- scientific article; zbMATH DE number 3393716 (Why is no real title available?)
- scientific article; zbMATH DE number 3403724 (Why is no real title available?)
- Program proving: KJumps and functions
- Proof of a program
Cited in
(16)- A decomposition rule for the Hoare logic
- Proving the correctness of regular deterministic programs: A unifying survey using dynamic logic
- Nondeterministic flowchart programs with recursive procedures: Semantics and correctness. II
- Hoare's logic and Peano's arithmetic
- Reasoning about programs
- Structured implementation of symbolic execution: A first part in a program verifier
- PASCAL in LCF: Semantics and examples of proof
- Formal verification of a programming logic for a distributed programming language
- Automatic synthesis of logical models for order-sorted first-order theories
- The automated proof of a trace transformation for a bitonic sort
- The verification and synthesis of data structures
- Secure mechanical verification of mutually recursive procedures
- Axiomatic approach to total correctness of programs
- Current methods for proving program correctness
- Mechanical verification of mutually recursive procedures
- Verification conditions for source-level imperative programs
This page was built for publication: Automatic program verification. I: A logical basis and its implementation
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1843170)
