Automated proofs of object code for a widely used microprocessor
Journal of the ACM1996Vol. 43(1), pp. 166–192
Citations Over TimeTop 10% of 1996 papers
Abstract
We have formally described a substantial subset of the MC68020, a widely used microprocessor built by Motorola, within the mathematical logic of the automated reasoning system Nqthm, a.k.a. the Boyer-Moore
Related Papers
- → Do Generic Proofs Improve Proof Comprehension?(2020)10 cited
- → Combining Pencil/Paper Proofs and Formal Proofs, A Challenge for Artificial Intelligence and Mathematics Education(2022)4 cited
- → Postsecondary Student Perceptions of Received Mathematical Proofs(2014)3 cited
- → Mathematical Proofs 101: How Proofs Should Be Read, Written, and Taught(2018)
- Passages of Proof(2003)