Date: Mon, 27 Oct 2003 20:37:48 -0600 (CST) From: Sandip Ray To: acl2-mtg@lists.cc.utexas.edu 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 Greetings, This week, I plan to give a practice talk for my Ph.D. Oral proposal, scheduled on Nov 17. The talk is targetted for people not necessarily familiar with ACL2, so will possibly be on a "high level". However, I will be happy to go into details on any aspect which is found interesting. I expect to get active feedbacks which will help me to prepare for the proposal defense. Sandip. ========================================================================= Here are the title and abstract. I will provide a draft of the write-up and the slides soon. Title: Using Theorem Proving and Algorithmic Techniques for Large-Scale System Verification Abstract: We propose to write a thesis on using theorem proving with algorithmic techniques for verification of large scale computer systems. Large-scale computer systems tend to have a non-terminating computation, and reasoning about such systems involves exhibiting some temporal property of the system. For large system models, automatic verification of non-trivial temporal properties is often infeasible, because of the state explosion problem. Theorem proving has a better potential to scale up to large designs, but it often requires considerable user assistance to guide the proof. We consider an intermediate approach, using theorem proving to verify correspondence between executions of a concrete system design and its abstraction, and then using automated analysis to verify the temporal properties of abstractions. We explore the logical issues and problems involved in the use of automated analysis on abstractions verified by a theorem prover. We implement tools and techniques that provide a reasonable amount of automation in the verification process. We plan to demonstrate our techniques on verification of multiprocessor system models, and specifically focus on synchronization protocols, cache coherence, and pipelined architecture of realistic systems. We use ACL2 (a programming language, logic, and theorem prover) to illustrate our techniques.