call for papers, previous message

From: (David Dill)
Subject:  Conference Announcment -- CAV 94
Date:     Mon, 2 May 94 11:36:56 PDT


		Conference on Computer-Aided Verification
				CAV 1994

Stanford University
June 21-23, 1994


The Sixth Conference on Computer-Aided Verification will be held June
21-23 at Stanford University.  The conference will be followed on June
24th by a one-day workshop on practical aspects of computer-aided
formal verification.

CAV 94 is sponsored by a group of companies with a strong interest in
the topic area: AT&T, IBM, Intel, Motorola, Redwood Design Automation
and Sun Microsystems.

IMPORTANT NOTE: World Cup matches will be held at Stanford on June
20th and 24th, which will contribute to congestion both locally and in
air travel.  Please make your flight reservations as soon as possible!

WORKSHOP: On Friday, June 24th, there will be a one-day workshop
consisting of presentations by both developers and users of formal
verification tools, with special emphasis on experiences on
applications.  This is still being arranged -- more details will
follow shortly.

LOCATION: The conference will be held on the Stanford campus.
Stanford will provide housing and food for participants in student
residences.  Participants may opt to stay in local hotels, but rooms
will be scarce due to the World Cup Finals being held in the area at
that time.

The Stanford Campus is about 30-40 minutes drive from two major
international airports, San Francisco and San Jose.  Commercial
shuttle service is available.

REGISTRATION: Please complete the attached reservation form and either
email or physically mail it with payment to the appropriate address.

HOUSING: We strongly encourage participants to stay on campus to
promote interaction with other conference participants.  The cost of
rooms and all meals (except for dinner on Wednesday night) will be
$217 for three days and nights.  A room may be reserved for the night
of Thursday, June 23, for an additional $39.  There is also a $50 key
deposit that will be refunded upon checkout.  A few rooms may be
reserved for subsequent nights (for participants who wish to tour the
Bay area), depending on availability.  Dinner on Wednesday will be a
banquet at another site (transportation will be provided).  Student
registration does NOT include the banquet Wednesday.

PARKING: Parking permits will be available on request at registration.
Parking is available near the dorms.

CLIMATE:  The weather will almost certainly be 72-80 degrees (F)
with cloudless skies.  It generally cools down significantly in the
evenings (in the 50s), so a sweater is helpful if you are out in the
evening.  At other places in the Bay area (e.g. parts San Francisco),
it can by foggy and very cool.

FURTHER INFORMATION: You can send electronic mail to
"" if you have further questions about the



If you are paying by credit card, you may return this registration
form by electronic mail to ""

Otherwise, physically mail the form along with payment in the form of
a VISA or MasterCard number, a check drawn on a U.S. bank, or an
international money order (in U.S. dollars) to Events Plus and mail
it to

	Events Plus
	attn: Cecilia Sanchez
	540 Valley Way
	Milpitas, CA 95035

Events Plus can be contacted at the above address.  Their
telephone is (408) 262 8109 and fax is (408) 262 8344.

Please contact Events Plus for special arrangements (e.g. hotel
rooms after the conference).

The registration form is due May 20.  Timely registration is important to make
sure we have reserved adequate rooms.  There is also a limit on the number
who can attend the banquet.

     Name: _____________________________________________________

     Affiliation: ______________________________________________

     Address: __________________________________________________


     Country: __________________________________________________

     Phone: _______________________ Fax: _______________________
     (please include country and city code)

     Email: ____________________________________________________

For room assignment:

     Are you:   Male   Female

Confirmation will be sent to you by email.

     Regular advanced registration:	$200		$___
     Late registration:			$250		$___
     Student registration:		$150		$___
     Housing&Meals June 20-22		$267		$___
        (excl. banquet, incl. $50 refundable key deposit)
     Housing June 23			 $39		$___
     TOTAL 						$___

Would you like to pay by VISA [ ] or MasterCard [ ]?  

If so, what is the number? _______________________________ 

expiration date ______,  daytime telephone _________________

Do you have any special dietary requirements?

Vegetarian [ ]		Kosher [ ]	Other: ___________________


This is the final program.  However, there may be last-minute changes
in the schedule.

Monday  June 20, 1994

8 - 10 PM	Reception and registration

Tuesday  June 21, 1994

8:30  Late registration

9 AM	Welcome

Session 1:	9:15 -- 10:45

9:15 - 9:45:    "A Determinizable Class of Timed Automata"
    R. Alur and L. Fix and T. A. Henzinger

9:45 - 10:15:    "Real-Time System Verification Using P/T Nets"
    R. Gorrieri and G. Siliprandi

10:15 - 10:45:    "Criteria for the Simple Path Property in Timed Automata"
    W. K.C. Lam and R. K. Brayton

BREAK:  10:45 - 11:15

Session 2:	11:00 - 12:30

11:00 - 11:30:    "Hierarchical Representations of Discrete Functions,
		  with Application to Model Checking"
    K. L. McMillan

11:30 - 12:00: "Symbolic Verification with Periodic Sets"
    B. Boigelot and P. Wolper

12:00 - 12:30: "Automatic Verification of Pipelined Microprocessor
    J. R. Burch and D. L. Dill

LUNCH: 12:30 -- 2:00

Session 3:	2:00 - 4:00

2:00 - 2:30: "Using Abstractions for the Verification of Linear
		Hybrid Systems"
    A. Olivero, J. Sifakis and S. Yovine

2:30 - 3:00: "Decidability of Hybrid Systems with Rectangular
		 Differential Inclusions"
    A. Puri and P. Varaiya

3:00 - 3:30 "Suspension Automata: A Decidable Class of Hybrid
    J. McManis and P. Varaiya

3:30 - 4:00 "Verification of Context-Free Timed Systems Using
		Linear Hybrid Observers"
    A. Bouajjani, R. Echahed, and R. Robbana

BREAK:  4:00 - 6:00

Session 4:	4:30 - 6:00		Chair: A. Emerson

4:30 - 5:00    "On the Random Walk Method for Protocol Testing"
    M. Mihail and C. H. Papadimitriou

5:00 - 5:30    "An Automata-Theoretic Approach to Branching-Time Model 
    O. Bernholtz, M. Y. Vardi, and P. Wolper

5:30 - 6:00   "Realizability and Synthesis of Reactive Modules"
    A. Anuchitanukul and Z. Manna

7:00 PM  Dinner

After dinner:  Software demos

Wednesday,  June 22, 1994

Session 5:	8:30 - 10:00

8:30 - 9:00    "Methodology and System for Practical Formal Verification
		   of Reactive Hardware"
    I. Beer, S. Ben-David, D. Geist, R. Gewirtzman, and M. Yoeli

9:00 - 9:30    "Modeling and Verification of a Real Life Protocol 
		   Using Symbolic Model Checking",
    V. G. Naik and A. P. Sistla

9:30 - 10:00    "Verification of a Distributed Cache Memory by 
		using Abstractions",
    S. Graf

BREAK  10:00 - 10:30

Invited talk:	10:30 - 11:30
     "Beyond Model Checking"
     Z. Manna,  Stanford University

Session 6:	11:30 -- 12:30

11:30 - 12:00    "Models Whose Checks Don't Explode"
    R. P. Kurshan

12:00 - 12:30    "On the Automatic Computation of Network Invariants"
    F. Balarin and A. L. Sangiovanni-Vincentelli

LUNCH		12:30 -- 1:30

Session 7: 	1:30 -- 3:00

1:30 - 2:00    "Ground Temporal Logic: A Logic for Hardware Verification"
    D. Cyrluk and P. Narendran

2:00 - 2:30    "A Hybrid Model for Reasoning about Composed Hardware Systems"
    E. T. Schubert

2:30 - 3:00   "Composing Symbolic Trajectory Evaluation Results"
    S. Hazelhurst and C-J. H. Seger

Session 8:	3:00 - 5:30		Chair:  R. Bryant

3:00 - 3:30   "The Completeness of a Hardware Inference System"
    Z. Zhu and C-J. H. Seger

3:30 - 4:00   "Efficient Model Checking by Automated Ordering of 
	       Transition Relation Partitions"
    D. Geist and I. Beer

4:00 - 4:30   "The Verification Problem for Replaceability"
    V. Singhal and C. Pixley


Thursday,  June 23. 1994

Session 9:	9:00 - 10:00

8:30 - 9:00  "Formula-Dependent Equivalence for Compositional CTL 
	       Model Checking",
    A. Aziz, T. R. Shiple, V. Singhal, and A. L. Sangiovanni-Vincentelli

9:00 - 9:30  "An Improved Algorithm for the Evaluation of Fixpoint
    D. E. Long, A. Browne, E. M. Clarke, S. Jha, and W. R. Marrero

9:30 - 10:00  "Incremental Model Checking in Modal Mu-Calculus",
    O. V. Sokolsky and S. A. Smolka

BREAK:  10:00 - 10:30

Session 10:	10:30 - 12:30

10:30 - 11:00   "Performance Improvement of State Space Exploration by 
		 Regular and Differential Hashing Functions"
    B. Cousin and J. H\'{e}lary

11:00 - 11:30   "Combining Partial Order Reductions with On-the-fly 
    D. Peled

11:30 - 12:00   "Improving Language Containment Using Fairness Graphs"
    R. Hojati, R. Mueller-Thuns, and R. K. Brayton

12:00 - 12:30   "A Parallel Algorithm for Relational Coarsest Partition
		 Problems and Its Implementation"
    I. Lee and S. Rajasekaran

LUNCH  12:30 - 2:00

Session 11:	2:00 - 3:30

2:00 - 2:30    "Another Look at LTL Model Checking"
    E. Clarke, O. Grumberg, and K. Hamaguchi

2:30 - 3:00   "The Mobility Workbench:  A Tool for the Pi-Calculus"
    B. Victor and F. Moller

3:00 - 3:30    "Model Checking of Macro Processes"
    H. Hungar

Session: 12:	3:30 - 4:30

3:00 - 3:30   "Compositional Semantics of Esterel and Verification by
	       Compositional Reductions"
    R. de Simone and A. Resouche

3:30 - 4:00  "Design of a VHDL/S Model Checker Based on Adaptive State 
	      and Data Abstraction"
    D. Dams, R. Gerth, G. D\"{o}hmen, R. Herrmann, P. Kelb and H. Pargmann

4:00 - 4:30   "Automatic Verification of Timed Circuits"
    T. G. Rokicki and C. J. Myers


Friday,  June 24, 1994

Workshop on Practical Aspects of Formal Verification

Stanford University

9:00 -- 5:00 PM

The workshop will be a series of series of presentations and
discussions on formal verification tools and practical applications of
them in industry.  We hope to emerge with a clearer view of the state
of the art of practical formal verification, and where things are

The following people have already agreed to speak.  There will be more
on the schedule later.

Ken McMillan		(Cadence Laboratories)

Carl Pixley		(Motorola)

Andreas Nowatzyk	(Sun Microsystems)

Robert Kurshan 		(AT&T)

Ze'ev Shtadtler		(Intel)

David Dill		(Stanford)