Mechanical verification of mutually recursive procedures

DOI10.1007/3-540-61511-3_81MaRDI QIDQ4647514zbMATH OpenOpenAlexFDO

Authors Peter V. Homeier, David 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

Boolean expressionindividual programlogical variablerecursive procedureverification condition

Mathematics Subject Classification ID

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

Recommendations

• Secure mechanical verification of mutually recursive procedures
• Sound and complete verification condition generator for functional recursive programs
• Verification of procedural programs
• Proving mutual termination
• Frame rule for mutually recursive procedures manipulating pointers

Cites work

• Assignment and Procedure Call Proof Rules
• Automatic program verification. I: A logical basis and its implementation
• scientific article; zbMATH DE number 439891 (Why is no real title available?)
• scientific article; zbMATH DE number 3723840 (Why is no real title available?)
• scientific article; zbMATH DE number 3581593 (Why is no real title available?)
• scientific article; zbMATH DE number 234014 (Why is no real title available?)
• Partial correctness: The term-wise approach
• Soundness and Completeness of an Axiom System for Program Verification
• Substitution revisited

Cited in

(8)

• Secure mechanical verification of mutually recursive procedures
• Unbounded procedure summaries from bounded environments
• An algebraic treatment of procedure refinement to support mechanical verification
• Sound and complete verification condition generator for functional recursive programs
• Verification Condition Generation Via Theorem Proving
• Checking observational purity of procedures
• Frame rule for mutually recursive procedures manipulating pointers
• Proving mutual termination

Describes a project that uses

Uses Software

• ML
• HOL

This page was built for publication: Mechanical verification of mutually recursive procedures

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4647514)