A mechanical analysis of program verification strategies

DOI10.1007/S10817-008-9098-1MaRDI QIDQ928673zbMATH OpenOpenAlexFDO

Authors Elsie Sterbin Gottlieb

Publication date 11 June 2008

Published in Journal of Automated Reasoning (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/s10817-008-9098-1

zbMATH Keywords

InvariantsTheorem provingInductive assertionsPartial correctnessTotal correctness

Mathematics Subject Classification ID

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

Recommendations

• Programmed strategies for program verification
• Mechanical Verification of Automatic Synthesis of Fault-Tolerant Programs
• A new approach to program verification
• A vindication of program verification
• A unified approach of program verification

Cites work

• scientific article; zbMATH DE number 3702108 (Why is no real title available?)
• scientific article; zbMATH DE number 3707731 (Why is no real title available?)
• scientific article; zbMATH DE number 88983 (Why is no real title available?)
• scientific article; zbMATH DE number 3560698 (Why is no real title available?)
• scientific article; zbMATH DE number 3617510 (Why is no real title available?)
• scientific article; zbMATH DE number 1088222 (Why is no real title available?)
• scientific article; zbMATH DE number 3448070 (Why is no real title available?)
• scientific article; zbMATH DE number 2090288 (Why is no real title available?)
• scientific article; zbMATH DE number 868107 (Why is no real title available?)
• scientific article; zbMATH DE number 234014 (Why is no real title available?)
• scientific article; zbMATH DE number 3302923 (Why is no real title available?)
• scientific article; zbMATH DE number 3403724 (Why is no real title available?)
• scientific article; zbMATH DE number 3024905 (Why is no real title available?)
• A New Incompleteness Result for Hoare's System
• Algorithms for ordinal arithmetic.
• An axiomatic basis for computer programming
• Automated proofs of object code for a widely used microprocessor
• Axioms for total correctness
• Computer Aided Verification
• Executable JVM model for analytical reasoning: A study
• Formal Methods in Computer-Aided Design
• Fundamental Approaches to Software Engineering
• Inductive assertions and operational semantics
• Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
• Logic for Programming, Artificial Intelligence, and Reasoning
• Partial functions in ACL2
• Program proving: KJumps and functions
• Proof of correctness of data representations
• Proving pointer programs in higher-order logic.
• Soundness and Completeness of an Axiom System for Program Verification
• Ten Years of Hoare's Logic: A Survey—Part I
• Theorem Proving in Higher Order Logics
• Theorem Proving in Higher Order Logics
• Verification Condition Generation Via Theorem Proving
• Verifying properties of parallel programs

Cited in

(5)

• Programmed strategies for program verification
• Mechanical verification on strategies
• scientific article; zbMATH DE number 1693427 (Why is no real title available?)
• Formal Methods in Computer-Aided Design
• Program analysis is harder than verification: a computability perspective

Describes a project that uses

Uses Software

• Piton
• NQTHM
• ESC/Java
• HOL
• StateFlow
• PVS
• SPARK
• Isabelle/HOL
• ML
• ACL2

This page was built for publication: A mechanical analysis of program verification strategies

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