Date: Mon, 06 Nov 2006 17:16:25 -0600
From: Sol Swords
Subject: ACL2 Meeting Nov. 8

Hi everyone,

Julien Schmaltz will be talking at the meeting this Wednesday, Nov. 8, 4 
PM, in ACES 3.116.  Hope to see you all there.  Here is the abstract of 
his talk:

"Asynchronous Communications at the Gate Level: An Isabelle Theory by an 
ACL2 User"

We present an Isabelle formalization of the bit transfer between two 
indepently clocked registers. Our model considers precise timing 
parameters and metastability.  We prove the correct bit transfer in an 
analog context and show how to integrate this result into proofs about 
digital entities only. The outcome is a formal definition of digital 
conditions which guarantee correctness in the analog context. These 
separation between analog and digital concerns allows the use of 
automatic tools, like model checkers or SAT solvers. To illustrate our 
approach, we develop the correctness proof of clock synchronization 
hardware. In the context of the Verisoft project, our results constitute 
the ground theory for the pervasive verification, from abstract software 
down to gates, of real-time distributed systems. The proof has been 
carried out within Isabelle and using nuSMV. Finally, we discuss this 
Isabelle proof as compared as the ACL2 approach.