Automatic program verification. I: A logical basis and its implementation

DOI10.1007/BF00288746zbMath0279.68022OpenAlexW2032889498MaRDI QIDQ1843170

David C. Luckham, Ralph L. London, Shigeru Igarashi

Publication date: 1974

Published in: Acta Informatica (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/bf00288746

Mathematics Subject Classification ID

General topics in the theory of software (68N01)

Related Items

Secure mechanical verification of mutually recursive procedures, A decomposition rule for the Hoare logic, Automatic synthesis of logical models for order-sorted first-order theories, Proving the correctness of regular deterministic programs: A unifying survey using dynamic logic, Nondeterministic flowchart programs with recursive procedures: Semantics and correctness. II, Verification conditions for source-level imperative programs, Hoare's logic and Peano's arithmetic, Mechanical verification of mutually recursive procedures, Reasoning about programs, Structured implementation of symbolic execution: A first part in a program verifier, PASCAL in LCF: Semantics and examples of proof, The automated proof of a trace transformation for a bitonic sort, Current methods for proving program correctness, Formal verification of a programming logic for a distributed programming language, Axiomatic approach to total correctness of programs, The verification and synthesis of data structures

Uses Software

• Find

Cites Work

• Program proving: KJumps and functions
• An axiomatic definition of the programming language Pascal
• An axiomatic basis for computer programming
• Proof of a program
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item