Skip header Section
Skip Bibliometrics Section
Higher order logic and hardware verificationDecember 1993
- Author:
- T. Melham
Abstract
No abstract available.
Cited By
- Lööw A Lutsig: a verified Verilog compiler for verified circuit development Proceedings of the 10th ACM SIGPLAN International Conference on Certified Programs and Proofs, (46-60)
- Wang M, Tian C, Zhang N, Duan Z and Du H (2019). Verifying a scheduling protocol of safety-critical systems, Journal of Combinatorial Optimization, 37:4, (1191-1215), Online publication date: 1-May-2019.
- Reynolds T, Procter A, Harrison W and Allwein G (2019). The Mechanized Marriage of Effects and Monads with Applications to High-assurance Hardware, ACM Transactions on Embedded Computing Systems, 18:1, (1-26), Online publication date: 28-Feb-2019.
- Reynolds T, Procter A, Harrison W and Allwein G A core calculus for secure hardware Proceedings of the 15th ACM-IEEE International Conference on Formal Methods and Models for System Design, (122-131)
- Harrison W, Procter A and Allwein G Model-driven design & synthesis of the SHA-256 cryptographic hash function in ReWire Proceedings of the 27th International Symposium on Rapid System Prototyping: Shortening the Path from Specification to Prototype, (114-120)
- Austin E and Alexander P Stateless higher-order logic with quantified types Proceedings of the 4th international conference on Interactive Theorem Proving, (469-476)
- Braibant T Coquet Proceedings of the First international conference on Certified Programs and Proofs, (330-345)
- Perna J and Woodcock J A denotational semantics for Handel-C hardware compilation Proceedings of the formal engineering methods 9th international conference on Formal methods and software engineering, (266-285)
- Perna J and Woodcock J A Denotational Semantics for Handel-C Hardware Compilation Formal Methods and Software Engineering, (266-285)
- Gordon M, Iyoda J, Owens S and Slind K (2006). Automatic Formal Synthesis of Hardware from Higher Order Logic, Electronic Notes in Theoretical Computer Science (ENTCS), 145, (27-43), Online publication date: 1-Jan-2006.
- Cornelissen F, Jonker C and Treur J (2003). Compositional verification of knowledge-based task models and problem-solving methods, Knowledge and Information Systems, 5:3, (337-367), Online publication date: 1-Sep-2003.
- O'Donnell J Overview of Hydra Proceedings of the 16th International Parallel and Distributed Processing Symposium
- Susanto K and Melham T (2001). Formally Analyzed Dynamic Synthesis of Hardware, The Journal of Supercomputing, 19:1, (7-22), Online publication date: 1-May-2001.
- Hanna K (2000). Reasoning About Analog-Level Implementationsof Digital Systems, Formal Methods in System Design, 16:2, (127-158), Online publication date: 1-Mar-2000.
- Krämer B and Völker N (1997). A Highly Dependable Computing Architecture for Safety-CriticalControl Applications, Real-Time Systems, 13:3, (237-251), Online publication date: 1-Nov-1997.
Index Terms
- Higher order logic and hardware verification
Please enable JavaScript to view thecomments powered by Disqus.
Recommendations
The Use of Higher Order Logic in Program Verification
This paper focuses on the interface between program verification and mechanical theorem proving. It is often much easier to express what a program does in higher order logic than in first-order logic. However, in general, higher order theorem proving is ...