Providing a formal linkage between MDG and HOL
From MaRDI portal
Publication:878110
DOI10.1007/s10703-006-0017-yzbMath1112.68096WikidataQ61929511 ScholiaQ61929511MaRDI QIDQ878110
Sofiène Tahar, Haiyan Xiong, Paul Curzon, Ann Blandford
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
Formal hardware verification; Hybrid verification systems; Usability verification; Verification system correctness
68Q60: Specification and verification (program logics, model checking, etc.)
Uses Software
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