Providing a formal linkage between MDG and HOL

DOI10.1007/s10703-006-0017-yzbMath1112.68096OpenAlexW2011639059WikidataQ61929511 ScholiaQ61929511MaRDI QIDQ878110

Paul Curzon, Haiyan Xiong, Ann Blandford, Sofiène Tahar

Publication date: 26 April 2007

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

Full work available at URL: https://spectrum.library.concordia.ca/977375/1/FMSD-2007.pdf

zbMATH Keywords

Formal hardware verificationHybrid verification systemsUsability verificationVerification system correctness

Mathematics Subject Classification ID

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

Uses Software

• Maple
• ML
• Prosper
• PVS
• HOL
• BuDDy
• Gandalf
• PROSPER

Cites Work

• A Skeptic's approach to combining HOL and Maple
• A machine-checked implementation of Buchberger's algorithm
• Edinburgh LCF. A mechanized logic of computation
• Programming a Symbolic Model Checker in a Fully Expansive Theorem Prover
• Toward compiler implementation correctness proofs
• Graph-Based Algorithms for Boolean Function Manipulation
• Automated Technology for Verification and Analysis
• Demonstrating the cognitive plausability of interactive system specifications
• 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
• Unnamed Item