Mechanical verification of mutually recursive procedures

DOI10.1007/3-540-61511-3_81zbMath1412.68138OpenAlexW191371315MaRDI QIDQ4647514

Peter V. Homeier, David F. Martin

Publication date: 15 January 2019

Published in: Automated Deduction — Cade-13 (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/3-540-61511-3_81

zbMATH Keywords

recursive procedureBoolean expressionverification conditionlogical variableindividual program

Mathematics Subject Classification ID

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

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