Symbolic Simulation of x86-64 Instructions Using Congruence-Based
Rewriting: A Failed but Interesting Experiment on the x86isa Model

Shilpi Goel
1st March, 2016

In this talk, I will describe why my plan of using congruence-based
rewriting to symbolically simulate x86-64 programs on the x86isa model
(books/projects/x86isa) failed --- not because of some limitation of
congruence-based reasoning, but because of subtleties in the x86
paging mechanism which I inconveniently neglected to consider while
formulating my plan.

This setback hasn't left me embittered about congruence-based
reasoning at all --- after all, that's not where the problem was.
This experiment afforded me the pleasure of working with ACL2's
congruence rules for a while, and I will try to convince you how
amazing congruence-based reasoning is, as long as it is applied
wisely.