Kami: a platform for high-level parametric hardware specification and its modular verification
<jats:p>It has become fairly standard in the programming-languages research world to verify functional programs in proof assistants using induction, algebraic simplification, and rewriting. In this paper, we introduce Kami, a Coq library that enables similar expressive and modular reasoning fo...
Main Authors: | Choi, Joonwon, Vijayaraghavan, Muralidaran, Sherman, Benjamin, Chlipala, Adam, Arvind |
---|---|
Other Authors: | Massachusetts Institute of Technology. Computer Science and Artificial Intelligence Laboratory |
Format: | Article |
Language: | English |
Published: |
Association for Computing Machinery (ACM)
2021
|
Online Access: | https://hdl.handle.net/1721.1/134865 |
Similar Items
-
Modular Deductive Verification of Multiprocessor Hardware Designs
by: Vijayaraghavan, Muralidaran, et al.
Published: (2019) -
Modular verification of hardware systems
by: Vijayaraghavan, Muralidaran
Published: (2016) -
Integration verification across software and hardware for a simple embedded system
by: Erbsen, Andres, et al.
Published: (2022) -
Formal Verification of Hardware Synthesis
by: Braibant, Thomas, et al.
Published: (2014) -
Specification and Verification of Strong Timing Isolation of Hardware Enclaves
by: Lau, Stella, et al.
Published: (2025)