call for papers, previous message
From: dill@hohum.stanford.edu (David Dill)
Subject: Conference Announcment -- CAV 94
Date: Mon, 2 May 94 11:36:56 PDT
CONFERENCE ANNOUNCEMENT
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
"cav@hohum.stanford.edu" if you have further questions about the
conference.
----------------------------------------------------------------
REGISTRATION
If you are paying by credit card, you may return this registration
form by electronic mail to "cav-registration@hohum.stanford.edu"
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
USA
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: ___________________
TECHNICAL PROGRAM
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
Control"
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
Automata"
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
Checking"
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
EXCURSION AND BANQUET 6:00 -- ?
----------------------------------------------------------------
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
Expressions",
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
Model-Checking"
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
* END OF CONFERENCE *
--------------------------------------------
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
headed.
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)