Secure mechanical verification of mutually recursive procedures

DOI10.1016/S0890-5401(03)00133-0zbMath1075.68615MaRDI QIDQ1887136

David F. Martin, Peter V. Homeier

Publication date: 23 November 2004

Published in: Information and Computation (Search for Journal in Brave)

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60)

Related Items

Verification conditions for source-level imperative programs

Uses Software

• ML
• HOL

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Partial correctness: The term-wise approach
• Substitution revisited
• Automatic program verification. I: A logical basis and its implementation
• Assignment and Procedure Call Proof Rules
• Soundness and Completeness of an Axiom System for Program Verification