|
|
|---|
|
|
|
|---|
S. Goel, W. A. Hunt, Jr., and M. Kaufmann, “Engineering
a Formal, Executable x86 ISA Simulator for Software Verification”,
in M. Hinchey, J. P. Bowen, and E.-R. Olderog, editors, Provably Correct
Systems Springer, pp. 173-209, 2017.
Relevance: operational model of the x86 at both the
user- and system-level and code proofs
Abstract
Construction of a formal model of a computing system is a necessary practice in formal verification. The results of formal analysis can only be valued to the same degree as the model itself. Model development is error-prone, not only due to the complexity of the system being modeled, but also because it involves addressing disparate requirements. For example, a formal model should be defined using simple constructs to enable efficient reasoning but it should also be optimized to offer fast concrete simulations. Models of large computing systems are themselves large software systems and must be subject to rigorous validation. We describe our formal, executable model of the x86 instruction-set architecture; we use our model to reason about x86 machine-code programs. Validation of our x86 ISA model is done by co-simulating it regularly against a physical x86 machine. We present design decisions made during model development to optimize both validation and verification, i.e., efficiency of both simulation and reasoning. Our engineering process provides insight into the development of a software verification and model animation framework from the points of view of accuracy, efficiency, scalability, maintainability, and usability.
See the collection of ACL2 books and files at
Also relevant are bib::goel16 and the following earlier papers bib::hk12, bib::ghk13,and bib::ghkg14.