Adam Chlipala

7 references under this name, matched as it is written. Somebody else may write under it too, and the same person may appear here spelled another way.

This description was written by a machine and published without a person checking it. It is what the agent made of this grouping, and not a statement anybody has stood behind.

Adam Chlipala

Adam Chlipala, MIT: proof-assistant-based hardware and systems -- Kami in 2017, the 2025 Making work and Granite in 2026, with the 2011 mostly-automated verification paper behind them. Four records.

Granite: A Modular Methodology for Foundational Verification of Hardware-Software Leakage Contracts
Stella Lau and others (2026)
Making Concurrent Hardware Verification Sequential
Thomas Bourgeat and others (2025) · Proceedings of the ACM on Programming Languages
Integration verification across software and hardware for a simple embedded system
Andres Erbsen and others (2021) · Proceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation · ACM
Kami: A Platform for High-Level Parametric Hardware Specification and Its Modular Verification
Joonwon Choi and others (2017) · Proceedings of the ACM on Programming Languages
Mostly-automated verification of low-level programs in computational separation logic
Adam Chlipala (2011) · 32nd ACM Conference on Programming Language Design and Implementation (PLDI)
An introduction to programming and proving with dependent types in coq
Adam Chlipala (2010) · J. Formalized Reasoning
A multipurpose formal RISC-V specification, 2021.
Thomas Bourgeat and others