Automatic program verification. I: A logical basis and its implementation
From MaRDI portal
Cites work
- 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?)
- An axiomatic basis for computer programming
- An axiomatic definition of the programming language Pascal
- Program proving: KJumps and functions
- Proof of a program
Cited in
(16)- PASCAL in LCF: Semantics and examples of proof
- A decomposition rule for the Hoare logic
- Proving the correctness of regular deterministic programs: A unifying survey using dynamic logic
- Formal verification of a programming logic for a distributed programming language
- The verification and synthesis of data structures
- Automatic synthesis of logical models for order-sorted first-order theories
- Axiomatic approach to total correctness of programs
- Verification conditions for source-level imperative programs
- Current methods for proving program correctness
- Nondeterministic flowchart programs with recursive procedures: Semantics and correctness. II
- Reasoning about programs
- Mechanical verification of mutually recursive procedures
- Secure mechanical verification of mutually recursive procedures
- Hoare's logic and Peano's arithmetic
- Structured implementation of symbolic execution: A first part in a program verifier
- The automated proof of a trace transformation for a bitonic sort
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)
