BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:A Mechanically Verified AIG-to-BDD Conversion Algorithm - Sol Swor
 ds (University of Texas)
DTSTART:20100706T120000Z
DTEND:20100706T130000Z
UID:TALK25412@talks.cam.ac.uk
CONTACT:Thomas Tuerk
DESCRIPTION:We present the mechanical verification of an algorithm for bui
 lding a BDD from an AND/INVERTER graph (AIG).  The algorithm uses two meth
 ods to simplify an input AIG using BDDs of limited size\; it repeatedly ap
 plies these methods while varying the BDD size limit.\n\nOne method is sim
 ilar to dynamic weakening in that it replaces oversized BDDs by a conserva
 tive approximation\; the other method introduces fresh variables to repres
 ent oversized BDDs. This algorithm is written in the executable logic of t
 he ACL2 theorem prover. The primary contribution is the verification of ou
 r conversion algorithm. We state its correctness theorem and outline\nthe 
 major steps needed to prove it.
LOCATION:Computer Laboratory\, William Gates Building\, Room SS03
END:VEVENT
END:VCALENDAR