Automating most parts of hardware proofs in HOL
- 1 January 1992
- book chapter
- Published by Springer Nature
- p. 365-375
- https://doi.org/10.1007/3-540-55179-4_35
Abstract
No abstract availableKeywords
This publication has 11 references indexed in Scilit:
- A COMMON APPROACH TO TEST GENERATION AND HARDWARE VERIFICATION BASED ON TEMPORAL LOGICPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2005
- Verification of synchronous sequential machines based on symbolic executionPublished by Springer Nature ,1990
- Sequential circuit verification using symbolic model checkingPublished by Association for Computing Machinery (ACM) ,1990
- First-Order Logic and Automated Theorem ProvingPublished by Springer Nature ,1990
- Correctness Properties of the Viper Block Model: The Second LevelPublished by Springer Nature ,1989
- HARP: A tableau-based theorem proverJournal of Automated Reasoning, 1988
- Formal Verification and Implementation of a MicroprocessorPublished by Springer Nature ,1988
- Implementing Safety-Critical Systems: The VIPER MicroprocessorPublished by Springer Nature ,1988
- Seventy-five problems for testing automatic theorem proversJournal of Automated Reasoning, 1986
- A Machine-Oriented Logic Based on the Resolution PrincipleJournal of the ACM, 1965