Structuring and automating hardware proofs in a higher-order theorem- proving environment

DOI10.1007/BF01383880zbMath0778.68074OpenAlexW1982619477MaRDI QIDQ1801500

Thomas Kropf, Ramayya Kumar, Klaus Schneider

Publication date: 9 January 1994

Published in: Formal Methods in System Design (Search for Journal in Brave)

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

zbMATH Keywords

verificationlogic designHOLFAUSTMEPHISTO

Mathematics Subject Classification ID

Fault detection; testing in circuits and networks (94C12)

Related Items

Accelerating tableaux proofs using compact representations

Uses Software

• HOL
• SATCHMO
• NQTHM

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Seventy-five problems for testing automatic theorem provers
• The notion of proof in hardware verification
• The undecidability of the second-order unification problem
• Symbolic model checking: \(10^{20}\) states and beyond
• Edinburgh LCF. A mechanized logic of computation
• A Machine-Oriented Logic Based on the Resolution Principle
• The undecidability of unification in third order logic
• A note on the Entscheidungsproblem