ACL2 Seminar, 9/30/2014

Some Ideas about Managing State in Code Proofs

J Moore

Abstract: Two characteristics of ACL2 code proofs --
especially for realistic machine code models -- are the
sizes of the symbolic state expressions produced by
runs through long sequences of instructions and the
predominance of arithmetic/logical expressions.  In
this talk I'll present some ideas for managing these
problems in a theorem-proving context.  This talk
describes work in progress; I'll welcome brainstorming
and be the first to admit that some of the ideas may be
inadequate to the task!