AMAST Mail 1998
[Prev][Next][Index]

CAV'98 Tutorials

(Apologies in advance for the multiple copies you may receive.  This
was sent to multiple mailing lists with overlapping subscribers, so there
is no way to prevent that.  If you receive duplicate copies or an incorrectly
addressed copy emailed directly to you (not through another mail list),
please let me know, and I'll try to fix the problem.  --Alan Hu, ajh@cs.ubc.ca)


		CAV'98 Tutorials on Formal Verification

    1998 International Conference on Computer-Aided Verification (CAV'98)
			June 28 - July 2, 1998
	    University of British Columbia, Vancouver, Canada


We are pleased to present a full-day of invited tutorials on formal
verification on Sunday, June 28, 1998, preceding the CAV'98 conference.
(Abstracts below.)  These tutorials are included in the conference
registration fee.  The rest of the conference program features additional
invited tutorials and talks, as well as a superb program of refereed
research papers.

For the conference program, additional information, registration,
and accommodations, please see:
	http://www.cs.ubc.ca/conferences/CAV98/index.html
Early registration deadline is May 29!


CAV'98 Tutorial Abstracts, Sunday, June 28, 1998:

9:00-10:30, 11:00-12:30
Invited Tutorial Sessions 1,2:
Model Checking for Beginners:  A Tutorial Introduction to
	Finite-State Verification
	Bob Kurshan (Bell Labs), Ken McMillan (Cadence Berkeley Labs)

Model checking is a technique of verifying automatically that a finite
state system satisfies a formal specification about its behavior over
time.  It has been successfully applied in numerous instances
to find errors in commercial hardware designs that escaped simulation,
from low-level control logic, to the cache coherence protocols of
multiprocessors.  Nonetheless, there is still a great deal of 
uncertainty as to how and whether model checking can be made into a 
workable tool for the engineer.

This tutorial will introduce the basics of model checking and related 
methods of verifying finite-state (and sometimes non-finite-state)
systems -- how to formally specify and verify a design, and techiques
such as abstraction, decomposition,  and "symbolic methods" that are
used to avoid the exponential explosion of state space size as system 
size increases.  We will also discuss the practicalities of using 
model checking as a verification aid in a commercial environment, 
using examples from commercial design practice, how to make the best
use of the particular advantages of model checking to find difficult
bugs, and why "formal" verification in practice is not always as 
formal as you might think.
	
2:00-3:30
Invited Tutorial Session 3:
Synchronous Programming of Reactive Systems
	Nicolas Halbwachs (VERIMAG)

We present the principles of synchronous languages, a family of
programming languages devoted to the design of reactive systems.
These principles are illustrated by two examples, the data-flow
language Lustre, and the imperative language Esterel. Specific
features related to the compilation and the verification of
synchronous programs are described, together with a survey of
current trends in this domain.

4:00-5:30
Invited Tutorial Session 4:
Ten Years of Partial Order Reduction
	Doron Peled (Bell Labs)

Checking the properties of concurrent systems is an ever growing 
challenge. Along with the development of improved verification methods, 
some critical systems that require careful attention have become 
highly concurrent and intricate. Partial order reduction methods were 
proposed for reducing the time and memory required to automatically
verify concurrent asynchronous systems. We describe partial order 
reduction for various logical formalisms, such as LTL, CTL and process 
algebras.  We show how one can combine partial order reduction with
other efficient model checking techniques.
[ AMAST Mail 1998 | Latest Update | AMAST Mail Meta-Index | AMAST ]