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

DOI10.1007/BF03180564MaRDI QIDQ1203115zbMATH OpenOpenAlexFDO

Authors 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

Boyer-Moore theorem proverconcurrent programmingManna-Pnueli modelprogram verificationtemporal logic

Mathematics Subject Classification ID

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

Recommendations

• Automatic verification of finite-state concurrent systems using temporal logic specifications
• Theories for mechanical proofs of imperative programs
• On the role of automated theorem proving in the compile-time derivation of concurrency
• Verifying Concurrent Systems with Symbolic Execution
• Modular verification for shared-variable concurrent programs

Cites work

• Adequate proof principles for invariance and liveness properties of concurrent programs
• scientific article; zbMATH DE number 88983 (Why is no real title available?)
• scientific article; zbMATH DE number 193479 (Why is no real title available?)
• scientific article; zbMATH DE number 194539 (Why is no real title available?)
• The addition of bounded quantification and partial functions to a computational logic and its theorem prover

Cited in

(11)

• Mechanical certification of systolic algorithms
• Theories for mechanical proofs of imperative programs
• A mechanically verified incremental garbage collector
• A mechanized proof environment for the convenient computations proof method
• Simplification of boolean verification conditions
• A mechanization of unity in PC-NQTHM-92
• scientific article; zbMATH DE number 65529 (Why is no real title available?)
• scientific article; zbMATH DE number 140005 (Why is no real title available?)
• scientific article; zbMATH DE number 177517 (Why is no real title available?)
• A Mechanically Checked Proof of IEEE Compliance of the Floating Point Multiplication, Division and Square Root Algorithms of the AMD-K7^™ Processor
• Wait-free linearization with a mechanical proof

Describes a project that uses

Uses Software

• NQTHM
• UNITY

This page was built for publication: A verification system for concurrent programs based on the Boyer-Moore prover

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