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.