Automated proofs of object code for a widely used microprocessor

1996116 citationsJournal Articlebronze Open Access

Authors

Robert S. Boyer · The University of Texas at Austin

Yuan Yu · The University of Texas at Austin

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

Topics & Keywords

Logic, programming, and type systems Formal Methods in Verification Parallel Computing and Optimization Techniques

Publication Details

Published in: Journal of the ACM

Volume 43, Issue 1, pp. 166-192

DOI: 10.1145/227595.227603

Field-Weighted Citation Impact: 9.74

Command Palette

Automated proofs of object code for a widely used microprocessor

Authors

Abstract

Topics & Keywords

Publication Details