A mechanical analysis of program verification strategies

DOI10.1007/s10817-008-9098-1zbMath1140.68060OpenAlexW2005344510MaRDI QIDQ928673

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

Theorem provingInvariantsInductive assertionsPartial correctnessTotal correctness

Mathematics Subject Classification ID

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

Uses Software

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

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
• Axioms for total correctness
• Partial functions in ACL2
• Program proving: KJumps and functions
• Proof of correctness of data representations
• Executable JVM model for analytical reasoning: A study
• Ten Years of Hoare's Logic: A Survey—Part I
• Verifying properties of parallel programs
• A New Incompleteness Result for Hoare's System
• Soundness and Completeness of an Axiom System for Program Verification
• Automated proofs of object code for a widely used microprocessor
• Computer Aided Verification
• Verification Condition Generation Via Theorem Proving
• Fundamental Approaches to Software Engineering
• Theorem Proving in Higher Order Logics
• Theorem Proving in Higher Order Logics
• Formal Methods in Computer-Aided Design
• An axiomatic basis for computer programming
• Logic for Programming, Artificial Intelligence, and Reasoning
• Correct Hardware Design and Verification Methods
• Automated Deduction – CADE-19
• Automated Deduction – CADE-19