A verification system for concurrent programs based on the Boyer-Moore prover
From MaRDI portal
Publication:1203115
DOI10.1007/BF03180564zbMath0758.68047OpenAlexW2034892041MaRDI QIDQ1203115
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
temporal logicconcurrent programmingprogram verificationBoyer-Moore theorem proverManna-Pnueli model
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
Cites Work