1/24/07 Dave Greve, Rockwell Collins, Inc. ACL2 Information Flow Proofs at Rockwell Collins ------------------------------------------------------------------------ Rockwell Collins has used ACL2 to support the security certifications of a number of computing systems. This talk will overview the certification of the Rockwell Collins' AAMP7 and the Green Hills Integrity 178b Operating System. We will also discuss the key theorems employed in these efforts and the primary challenges faced in proving and using those theorems effectively.