Carl Kwan
Current Organizations / Institutes
The organizations/institutes from the scholar's latest article
Research Subjects
Research Interests
Carl Kwan has a total of 2 co-authors. Here are the top co-authors by number of shared publications:
Justin Thaler
Georgetown University
1 shared publication- Quang Dao
Carnegie Mellon University
1 shared publication
Latest Publications
- Open Access
- 25 July 2025
- Published by Open Publishing Association in Electronic Proceedings in Theoretical Computer Science
- Vol. 423, 46-50
RV32I in ACL2
We present a simple ACL2 simulator for the RISC-V 32-bit base instruction set architecture, written in the operational semantics style. Like many other ISA models, our RISC-V state object is a singlethreaded object and we prove read-over-write, write-over-write, writing-the-read, and state wellformedness theorems. Unlike some other models, we separate the instruction decoding functions from their semantic counterparts. Accordingly, we verify encoding / decoding functions for each RV32I instruction, the proofs for which are entirely automatic.
- 25 July 2025
- Published by Open Publishing Association in Electronic Proceedings in Theoretical Computer Science
- Vol. 423, 46-50
Open AccessRV32I in ACL2
We present a simple ACL2 simulator for the RISC-V 32-bit base instruction set architecture, written in the operational semantics style. Like many other ISA models, our RISC-V state object is a singlethreaded object and we prove read-over-write, write-over-write, writing-the-read, and state wellformedness theorems. Unlike some other models, we separate the instruction decoding functions from their semantic counterparts. Accordingly, we verify encoding / decoding functions for each RV32I instruction, the proofs for which are entirely automatic.