Sol Swords, ACL2 Seminar, April 9, 2013

Abstract:

The And-Inverter Graph (AIG) is a data structure for expressing and 
manipulating Boolean functions and finite-state machines.  It is the basis 
for some of the best hardware equivalence- and model-checking algorithms.  We'll 
talk about a new ACL2 library for building and reasoning about AIGs and 
AIG-based algorithms, in particular its abstract-stobj-based representation, 
which helps to hide the implementation details and allow nicer ways of reasoning 
about the structures.