Date: Mon, 10 Feb 2003 18:02:47 -0600 (CST) From: Sandip Ray To: cc: "Matthews, John" Subject: This week in ACL2 Content-Type: TEXT/PLAIN; charset=US-ASCII Reply-To: acl2-mtg@lists.cc.utexas.edu Sender: owner-acl2-mtg@lists.cc.utexas.edu X-Listprocessor-Version: 8.2.10/020311/17:52 -- ListProc(tm) by CREN Hi, This week, I will talk about verification of model-checking reductions in ACL2, a project that I was working on at CRL last summer. I would appreciate any questions, comments, and suggestions. Here is an abstract for the talk. Model-checking is used in the industry for automatically analysing temporal properties of reactive computer systems. Model-cheking is difficult to apply as is, on large designs of systems, because of the phenomenon of "state explosion". To allow for automatically analysing properties of large designs, people often use "Compositional Reduction Techniques". These techniques look at the system description and the property to be checked in order to decompose the original verification problem into one or more "simpler" problems. Each such problem can then be analysed by a model-checker or further decomposed. Given the high cost of defects in systems being released, it is important to insure that the compositional algorithms themselves are sound. In this work, we therefore, attempt to analyse and verify implementations of two "simple" compositional reductions in ACL2. Rigorous proofs of all the compositional reductions we verify are present in the literature. However, it turns out that because of restrictions imposed by the logic of ACL2, we cannot formalize such proofs as is in the ACL2 system. I will discuss this issue and point out our approach to modeling the semantics of LTL in a way that allows for verification in ACL2. This is joint work with John Matthews at OGI. Thanks a lot, Sandip. -- ****************************************************************************** Praise is well, compliment is well, but affection --- that is the last and final and most precious reward that any man can win, whether by character or achievement. ****************************************************************************** SANDIP RAY Graduate Student (Ph.D) The University of Texas at Austin Department of Computer Sciences Taylor Hall 2.124 Office: MAI 2004 Austin, TX 78712-1188 Austin, TX 78712 USA USA PH: +1-512-4717316 PH: +1-512-4719749 ****************************************************************************** Permanent Address: Contact Address: FD -- 82, 1911 Willow Creek Dr Sector -- III Apt #206 Salt Lake City Austin Calcutta -- 700091 Texas 78741 India USA PH: +91-33-3347672 PH: +1-512-8040833 ****************************************************************************** ("`-/")_.-'"``-._ . . `; -._ )-;-,_`) E-Mail: (v_,)' _ )`-.\ ``-' sandip@cs.utexas.edu _.- _..-_/ / ((' ((,.-' ((,/ Homepage at: http://www.cs.utexas.edu/users/sandip ******************************************************************************