Date: Tue, 31 Oct 2006 09:33:51 -0600
From: Sol Swords

Hi all,

Tomorrow's ACL2 meeting (4 PM in ACES 3.116) will feature Qiang 
speaking.  Here is his abstract:

;====================================================================
I will review the paper "Verifying a Signature Architecture -- A 
Comparative Case Study" by David Basin etc., and the paper reports on a 
case study in applying different formal methods, e.g. HOL-Z and 
PROMELA/Spin, to model and verify an architecture for administrating 
digital signatures.  The paper suggests that HOL-Z is well suited for 
temporal reasoning about process models with complex operations on data, 
and the comparison highlights that, in the hands of an experienced user, 
theorem proving may be neither substantially more time-consuming nor 
more complex than model checking.
;========================================================================

Hope to see you there,

 - Sol