|
|
|---|
|
|
|
|---|
J S. Moore, “ Computing
Verified Machine Address Bounds during Symbolic Exploration of
Code,” in J. Bowen, H. Langmaack and E.-R. Olderog, editors,
Provably Correct Systems, Springer, pp. 151-172, 2017.
Relevance: an ACL2 tool for determining whether two
symbolic machine addresses may be equal
Abstract
When operational semantics is used as the basis for mechanized
verification of machine code programs it is often necessary for the theorem
prover to determine whether one expression denoting a machine address is
unequal to another. For example, this problem arises when trying to determine
whether a read at the address given by expression a is affected by an
earlier write at the address given by b. If it can be determined that
a and b are definitely unequal, the write does not affect the
read. Such address expressions are typically composed of “machine
arithmetic function symbols” such as
The utility described here is available in the ACL2 book