Secure mechanical verification of mutually recursive procedures

DOI10.1016/S0890-5401(03)00133-0zbMATH Open1075.68615MaRDI QIDQ1887136FDOQ1887136

Authors: Peter V. Homeier, David Martin 

Publication date: 23 November 2004

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

Recommendations

• Mechanical verification of mutually recursive procedures
• scientific article; zbMATH DE number 1962854
• Mechanical verification of concurrency control and recovery protocols
• Modular Verification of Recursive Programs
• A framework for compositional verification of security protocols
• scientific article; zbMATH DE number 1903362
• Programming Languages and Systems

Mathematics Subject Classification ID

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

Cites Work

• Title not available (Why is that?)
• Soundness and Completeness of an Axiom System for Program Verification
• Title not available (Why is that?)
• Automatic program verification. I: A logical basis and its implementation
• Substitution revisited
• Partial correctness: The term-wise approach
• Assignment and Procedure Call Proof Rules
• Title not available (Why is that?)
• Title not available (Why is that?)

Cited In (3)

• Verification Condition Generation Via Theorem Proving
• Verification conditions for source-level imperative programs
• Sound and complete verification condition generator for functional recursive programs

Uses Software

• ML
• HOL

This page was built for publication: Secure 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 Q1887136)