A verification system for concurrent programs based on the Boyer-Moore prover

DOI10.1007/BF03180564zbMath0758.68047OpenAlexW2034892041MaRDI QIDQ1203115

David M. Russinoff

Publication date: 4 February 1993

Published in: Formal Aspects of Computing (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/bf03180564

zbMATH Keywords

temporal logicconcurrent programmingprogram verificationBoyer-Moore theorem proverManna-Pnueli model

Mathematics Subject Classification ID

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

Related Items

A mechanically verified incremental garbage collector, Wait-free linearization with a mechanical proof, Theories for mechanical proofs of imperative programs, Simplification of boolean verification conditions, A Mechanically Checked Proof of IEEE Compliance of the Floating Point Multiplication, Division and Square Root Algorithms of the AMD-K7^™ Processor

Uses Software

• NQTHM
• UNITY

Cites Work

• Adequate proof principles for invariance and liveness properties of concurrent programs
• The addition of bounded quantification and partial functions to a computational logic and its theorem prover
• Unnamed Item
• Unnamed Item
• Unnamed Item