ask@iesd.auc.dk (Arne Skou) (04/25/91)
THIRD WORKSHOP ON
C O M P U T E R A I D E D V E R I F I C A T I O N
JULY 1--4, 1991
AALBORG UNIVERSITY, DENMARK
OBJECTIVES
This workshop is the third in a series dedicated to bringing together
researchers and practitioners interested in the development and use of
methods, tools and theories for automatic verification of (finite) state
systems. The goal of the workshop is to compare the various
verification methods for (finite) state systems, and tools supporting
them as assistants of the application designer. Emphasis will be not
only on new research results but also on the applications of existing
results to real verification problems. Special sessions for
demonstration of verification tools will be planned.
A balanced participation of researchers and practitioners is expected.
The workshop will present papers on the following topics, though the
list is not exhaustive:
Verification and validation tools for hardware and software
(hardware controllers, communications protocols, real-time systems,
etc.); verification methods by theorem proving, model checking,
automata based methods; and verification theories and their
applicability.
SPONSORSHIP
The workshop is sponsored by the Danish National Research Council and
by Aalborg University through the basic research project Programming
Environments in Theory and Practice.
The workshop has official recognition from IFIP WG10.2 (Hardware
Description Languages).
INVITED SPEAKERS
The workshop will have two invited speakers: Joseph Sifakis (IMAG,
Grenoble, France) and Colin Stirling (Edinburgh University, Scotland).
P R E L I M I N A R Y P R O G R A M
SUNDAY, JUNE 30
19.00--21.00: Opening registration at Limfjordshotellet.
MONDAY, JULY 1
8.30-9.00: Registration at Aalborg University.
SESSION 1
9.00--9.50: Invited Speaker, Colin Stirling (Edinburgh U): Taming
Infinite State Spaces.
9.50--10.15: Silence is Golden: Branching Bisimilarity is Decidable
for Context--Free Processes, Hans H{\"u}ttel (Edinburgh U).
10.15--10.40:
Computing Distinguishing Formulas for Branching Bisimulation, Henri
Korver (CWI).
10.40--11.10: Coffee Break
SESSION 2
11.10--11.35: Compositional Checking of Satisfaction, Henrik Andersen,
Glynn Winskel (Aarhus U).
11.35--12.00: An action based framework for verifying logical and
behavioural properties of concurrent systems, R De Nicola, A Fantechi,
S Gniesi, G Ristori.
12.00--12.25: A Linear-Time Model-Checking Algorithm for the
Alternation-Free Modal Mu-Calculus, R Cleaveland, B Steffen.
12.25--14.00: Lunch
SESSION 3
14.00--14.25: Automatic Temporal Verification of Buffer Systems,
A. Prasad Sistla, Lenore D. Zuck.
14.25--14.50: Mechanically Checked Proofs of Kernel Specifications,
W Bevier, J S{\o}gaard-Andersen.
14.50--15.15: A Top Down Approach to the Formal Specification of SCI
Cache Coherence, Stein Gjessing, Stein Krogdahl, Ellen Munthe--Kaas
(Oslo U).
15.15--15.45: Coffee Break
SESSION 4
15.45--16.10: Integer Programming in the Analysis of Concurrent Systems,
G S Avrunin, U A Buy, J C Corbett.
16.10--16.35: The Lotos Model of a Fault Protected System and its
Verification Using a Petri Net Based Approach, M Barbeau, G v Bochmann
(Montreal U).
16.35--17.00: Error diagnosis in finite communicating systems,
A Rasse.
17.00--17.25: Temporal Precondition Verification of Design Transformations,
R Vemuri, A Sridhar.
TUESDAY, JULY 2
SESSION 5
9.00--9.25: Pam: A Process Algebra Manipulator, H Lin (Sussex U).
9.25--9.50: The Concurrency Workbench with Priorities, C T Jensen
(Aarhus U).
9.50--10.15: A Proof Assistant for PSF, S Mauw, G Veltink (Amsterdam
U).
10.15--10.40: Towards Imperative Program Testing Using Logic Program
Inversion, B J Ross (Edinburgh U).
10.40--11.10: Coffee Break
SESSION 6
11.10--11.35: Avoiding state explosion by composition of minimal covering
graphs, A. Finkel, L. Petrucci.
11.35--12.00: On the fly verification of behavioural equivalences and
preorders, J.C. Fernanadez, L. Mounier.
12.00--12.25: Bounded-memory algorithms for verification on the fly,
C. Jard, Th. Jeron.
12.25--14.00: Lunch
SESSION 7
14.00--14.25: Generating BDDs for Symbolic Model Checking in CCS,
R Enders, F Filkorn, D Taubner.
14.25--14.50: Vectorized Symbolic Model Checking of Computation Tree
Logic for Sequential Machine Verification,
Hiromi Hiraishi, Kiyoharu Hamaguchi, Hiroyuki Ochi, Shuzo Yajima.
14.50--15.15: Functional Extension of Symbolic Model Checking, T
Filkorn.
15.15--15.45: Coffee Break
SESSION 8
15.45--16.10: An Automated Proof Technique for Finite--state Machine
Equivalence, W Mao, G Milne (Strathclyde U).
16.10--16.35: From data structures to process structures, E Brinksma
(Twente U).
16.35--17.00: Checking for Language Inclusion Using Simulation
Relations, D L Dill, A J Hu, H Wong--Toi.
17.00--17.25: Semantics Driven Method to Check the Finiteness of CCS
Processes, N de Francesco, P Inverardi (Pisa U).
WEDNESDAY, JULY 3
SESSION 9
9.00--9.25: Using the HOL prove assistant for proving the correctness
of term rewriting rules reducing terms of sequential behaviour}, M
Mutz (Passau).
9.25--9.50: Mechanizing a Proof by Induction of Process Algebra
Specifications in Higher Order Logic}, M Nesi (Cambridge U).
9.50--10.15: A Two-Level Formal Verification Methodology using HOL and
COSMOS, C--J Seger, J J Joyce (University of British Columbia).
10.15--10.40: Efficient Algorithms for Verification of Equivalences
for Probabilistic Processes, L Christoff, I Christoff (Uppsala U).
10.40--11.10: Coffee Break
SESSION 10
11.10--11.35: Partial-Order Model Checking: A Guide for the Perplexed,
D K Probst, H F Li.
11.35--12.00: Using partial orders for the efficient verification of
deadlock freedom and safety properties, P Godefroid, P Wolper.
12.00--12.25: Complexity Results for POMSET Languages,
J Feigenbaum (AT&T), J A Kahn (Harward).
12.25--14.00: Lunch
SESSION 11
14.00--14.25: Mechanically Verifying Safety and Liveness Properties
of Delay Insensitive Circuits, D M Goldschlag.
14.25--14.50: Automating most parts of hardware tools in HOL, K
Schneider, R Kumar, T Kropf.
15.00--22.00: Excursion & Banquet
THURSDAY, JULY 4
SESSION 13
9.00--9.50: Invited Speaker, Joseph Sifakis (IMAG): Timed
Specification Formalisms: an overview.
9.50--10.15: Minimum and Maximum Delay Problems In Real-Time Systems,
C Courcoubetis, M Yannakakis (AT&T).
10.15--10.40: Formal Verification of Speed-Dependent Asynchronous
Circuits Using Symbolic Model Checking of Branching Time Regular
Temporal Logic, Kiyoharu Hamaguchi, Hiromi Hiraishi, Shuzo Yahima.
10.40--11.10: Coffee Break
SESSION 14
11.10--11.35: Verifying Properties of HMS Machine Specifications of
Real-Time Systems, A Gabrielian, R Iyer.
11.35--12.00: A Linear Time Process Algebra,
A Jeffrey (Chalmers)
12.20--12.25: Deciding Properties for Regular Real Timed Processes,
U Holmer, K Larsen, W Yi.
12.25--14.00: Lunch
SESSION 15
14.00--14.25: From S/R models to Boolean processes, C. Corcoubetis,
S. Graf, J. Sifakis.
14.25--14.50: Comparing Generic State Machines, M. Langevin, E.
Cerny.
14.50--15.15: An Automata Theoretic approach to Temporal Logic, G G
de Jong.
DEMONSTRATIONS
Please find enclosed a call for demonstration of (verification) tools.
Demonstration of tools is planned to take place during coffee breaks
and in parallel with presentations neighbouring coffee breaks. The
demonstations will take place near the Auditorium for presentations.
LOCATION AND ACCOMMODATION
Aalborg is the fourth largest city of Denmark with approximately
200.000 inhabitants, and is situated approximately 100 km north of
Aarhus. Moreover, Aalborg is very close to the Danish west coast
(approximately 40 km to Blokhus and L{\o}kken) which is certainly well
worth a visit in the summer.
The organizers have arranged for accommodation at Limfjordshotellet
(single DKK 550,- and double DKK 800,-), andc in addition at an
unspecified hotel of tourist standard (in the range DKK 300,- --
500,-). All hotels are conveniently situated in the very center of
Aalborg and not far from the railway station.
Please find enclosed with this program a hotel
reservation form. Deadline for hotel reservation is May 24th.
The workshop itself will take place in the buildings of Aalborg
University, which is some 7 km from the
city center. Transportation between the hotels and the University
will be provided, and in addition one may use the existing bus
services number 11 and 20.
TRANSPORTATION
If you want to travel by plane, there are several daily connections
from Copenhagen. When arriving at Aalborg Airport, you can
conveniently use the special Airport bus (approximately DKK 25,-) towards
Aalborg city as it stops just opposite Limfjordshotellet (the very
first stop after the Limfjords--bridge). Alternatively, you can take
a taxi, costing approximately DKK 70,-.
If you arrive at the Railway Station in Aalborg you be just opposite
Park Hotel; to go to Limfjordshotellet you may choose to take a 10
minutes walk (there is a city map inside the arrival hall of the
Railway Station) or you may take a taxi (approximately DKK 30,-).
REGISTRATION
Please find enclosed with this program a registration form.
The prize for registration (DKK 1600,-) includes proceedings and a copy
of the final LNCS publication, transportation between hotel and
University, lunches, reception, excursion, and workshop banquet. Deadline for
registration is May 24th.
A registration desk will operate in Limfjordshotellet on Sunday, June
30, 7--9 pm. From Monday through Thursday, there will be a
registration and information desk outside the Auditorium at the University.
ADDRESSES AND TELEPHONES
You may find the following addresses useful:
Limfjordshotellet, Ved Stranden 14--16, 9100 Aalborg. Phone
+45 98164333. Telex: 69516 lim; Telefax: +45 98161747.
Kim Guldstrand Larsen, Aalborg University Center, Fredrik
Bajersvej 7, 9220 Aalborg. Telephone: +45 98158522 (through
switch board) or +45 98 154211 (wait--for--tone) 5017
(direct). E--mail: kgl@iesd.auc.dk.
Telefax: +45 98158129.
SOCAIL EVENTS
Sunday, 30 June, 19.00--21.00: Opening registration and gatering
at Limfjordshotellet, Ved Stranden 14--16.
Monday, 1 July, 19.00: Reception at the Art Museum of North
Jutland.
Wednesday, 3 July, 15.00: Excursion to the Danish west coast (Slette
Strand --- remember to bring swimming suits!) followed by Workshop
banquet. Transportation by bus leaving at 15.00 from the
Auditorium at the University.
C O N F E R E N C E O R G A N I Z A T I O N
STEERING COMMITTEE
E.M. Clarke (Carnegie--Mellon University),
R.P. Kurshan (At\& T Bell Laboratories),
K.G. Larsen (Aalborg University),
A. Pnueli (Weizmann Institue),
J. Sifakis (LGI--IMAG).
ORGANIZING COMMITTEE
K.G. Larsen, A. Skou (Aalborg University).
PROGRAM COMMITTEE
Gregor Bochmann (U. Montreal),
Robert Brayton (U. California, Berkeley),
Ed Brinksma (Twente U.),
Randy Bryant (Carnegie Mellon),
Rance Cleaveland (N.C. State),
Olivier Coudert (Bull),
Costas Courcoubetis (U. Crete),
David Cohen (Bell Core),
Werner Damm (U. Oldenburg),
David Dill (Stanford U.),
Allen Emerson (U. Texax, Austin),
Masahiro Fujita (Fujutsu),
Orna Grumberg (Technion),
Hiromi Hiraishi (Kyoto U.),
Gerard Holtzmann (AT&T Bell Labs),
Bengt Jonsson (SICS),
Kurt Keutzer (AT&T Bell Labs),
Harry Lewis (Harvard),
Michael Lightner (U.Colorado),
George Milne (U. Strathclyde),
Willem deRoever (Kiel U.),
Prasad Sistla (GTE Labs),
Colin Stirling (Edinburgh U.),
P.A. Subrahmanyam (AT&T Bell Labs),
Pierre Wolper (U. Liege),
Michael Yoeli (Technion).
-cut---------------------------------------------------------------------
C A V 9 1 R E G I S T R A T I O N F O R M
Name: ________________________________________
Organization: ________________________________
Address: ________________________________
________________________________
________________________________
________________________________
________________________________
Phone: ________________________________________
FAX: ________________________________________
E-mail: ________________________________________
Date: _____________ Signature: ______________
The registration fee is DKK 1600,-. It covers workshop lunches and
refreshments, the participant proceedings, reception, and an
excursion (including the banquet dinner) on July 3rd to the west coast
of Northern Jutland.
PAYMENT:
Payment of registration fee should be made by banker's cheque drawn on
a Danish bank and in Danish Kroner (private cheques will not be
accepted). The cheque should be made payable to:
CAV '91, c/o Aalborg Tourist Bureau, {\O}steraa 8, DK-9000 Aalborg,
Denmark.
Please return this form and PAYMENT NOT LATER THAN MAY 24th to
the registration secretary:
CAV '91
Aalborg Tourist Bureau
{\O}steraa 8
DK-9000 Aalborg
Denmark
phone: $+$45 98 12 63 55
fax: $+$45 98 16 69 22
The form may be sent via telefax followed by the cheque via snailmail.
-cut------------------------------------------------------------------------
C A V ' 9 1 H O T E L R E S E R V A T I O N F O R M
Name: ________________________________________
Organization: ________________________________
Address: ________________________________
________________________________
________________________________
________________________________
________________________________
Phone: ________________________________________
FAX: ________________________________________
E-mail: ________________________________________
Please reserve hotel room for me according to the following:
Single Double
Limfjordshotellet _ _
(single room DKK 550,-, (_) (_)
double room DKK 800,-)
Unspecified hotel of tourist _ _
standard in the range of DKK (_) (_)
300,- to 500,-
Date of arrival: ____ Date of departure: ______
Date: _______________ Signature: ______________
Please return this form NO LATER THAN MAY 24th to
the registration secretary:
CAV '91
Aalborg Tourist Bureau
{\O}steraa 8
DK-9000 Aalborg
Denmark
phone: $+$45 98 12 63 55
fax: $+$45 98 16 69 22
The form may be sent via telefax.
--cut----------------------------------------------------------------
C A V ' 9 1 D E M O N S T R A T I O N F O R M
During the conference there will be arranged sessions for
demonstration of verification tools. For those of you who want to use
this opportunity, please indicate your requirements below concerning
hardware and software for such a demonstration. As a standard
facility we will make a number of SUN4 machines available (SUN UNIX-OS
version 4.1.1), and we will offer to initiate the execution of
standard installation jobs before the conference. Also, we will on
request make accounts available for running FTP's and remote
installation jobs. Requirements going beyond the above will be
fulfilled as far as possible, but our resources are limited. For
example, we have a number of MAC's and we can also contact the
computing center of our campus in order to allow for remote usage of
VAX's. (The campus is covered by an Ethernet).
The filled out form should be returned to one of the local organisers
(Kim Larsen, Arne Skou) at Aalborg University, Department of
Mathematics and Computer Science, Fredrik Bajersvej 7, Bygn. E,
DK-9220 Aalborg, DENMARK
NAME OF TOOL: ________________________________________
NAME OF AUTHOR(S); ___________________________________
ADDRESS OF AUTHOR (including e-mail, fax, phone):
______________________________________________
______________________________________________
______________________________________________
______________________________________________
______________________________________________
REQUIREMENTS: machine, OS, disk, RAM, Windows, remote
connection,..
______________________________________________
______________________________________________
______________________________________________
______________________________________________
-cut---------------------------------------------------------------------
--
Arne Skou Internet: ask@iesd.auc.dk
Institute for electronic systems Aalborg University
Fredrik Bajers vej 7, 9220 Aalborg
DENMARK. (W) +45 98 15 85 22 (H) +45 98 39 17 81
--
=========================== MODERATOR ==============================
Steve Stevenson {steve,fpst}@hubcap.clemson.edu
Department of Computer Science, comp.parallel
Clemson University, Clemson, SC 29634-1906 (803)656-5880.mabellask@iesd.auc.dk (Arne Skou) (04/25/91)
THIRD WORKSHOP ON
C O M P U T E R A I D E D V E R I F I C A T I O N
JULY 1--4, 1991
AALBORG UNIVERSITY, DENMARK
OBJECTIVES
This workshop is the third in a series dedicated to bringing together
researchers and practitioners interested in the development and use of
methods, tools and theories for automatic verification of (finite) state
systems. The goal of the workshop is to compare the various
verification methods for (finite) state systems, and tools supporting
them as assistants of the application designer. Emphasis will be not
only on new research results but also on the applications of existing
results to real verification problems. Special sessions for
demonstration of verification tools will be planned.
A balanced participation of researchers and practitioners is expected.
The workshop will present papers on the following topics, though the
list is not exhaustive:
Verification and validation tools for hardware and software
(hardware controllers, communications protocols, real-time systems,
etc.); verification methods by theorem proving, model checking,
automata based methods; and verification theories and their
applicability.
SPONSORSHIP
The workshop is sponsored by the Danish National Research Council and
by Aalborg University through the basic research project Programming
Environments in Theory and Practice.
The workshop has official recognition from IFIP WG10.2 (Hardware
Description Languages).
INVITED SPEAKERS
The workshop will have two invited speakers: Joseph Sifakis (IMAG,
Grenoble, France) and Colin Stirling (Edinburgh University, Scotland).
P R E L I M I N A R Y P R O G R A M
SUNDAY, JUNE 30
19.00--21.00: Opening registration at Limfjordshotellet.
MONDAY, JULY 1
8.30-9.00: Registration at Aalborg University.
SESSION 1
9.00--9.50: Invited Speaker, Colin Stirling (Edinburgh U): Taming
Infinite State Spaces.
9.50--10.15: Silence is Golden: Branching Bisimilarity is Decidable
for Context--Free Processes, Hans H{\"u}ttel (Edinburgh U).
10.15--10.40:
Computing Distinguishing Formulas for Branching Bisimulation, Henri
Korver (CWI).
10.40--11.10: Coffee Break
SESSION 2
11.10--11.35: Compositional Checking of Satisfaction, Henrik Andersen,
Glynn Winskel (Aarhus U).
11.35--12.00: An action based framework for verifying logical and
behavioural properties of concurrent systems, R De Nicola, A Fantechi,
S Gniesi, G Ristori.
12.00--12.25: A Linear-Time Model-Checking Algorithm for the
Alternation-Free Modal Mu-Calculus, R Cleaveland, B Steffen.
12.25--14.00: Lunch
SESSION 3
14.00--14.25: Automatic Temporal Verification of Buffer Systems,
A. Prasad Sistla, Lenore D. Zuck.
14.25--14.50: Mechanically Checked Proofs of Kernel Specifications,
W Bevier, J S{\o}gaard-Andersen.
14.50--15.15: A Top Down Approach to the Formal Specification of SCI
Cache Coherence, Stein Gjessing, Stein Krogdahl, Ellen Munthe--Kaas
(Oslo U).
15.15--15.45: Coffee Break
SESSION 4
15.45--16.10: Integer Programming in the Analysis of Concurrent Systems,
G S Avrunin, U A Buy, J C Corbett.
16.10--16.35: The Lotos Model of a Fault Protected System and its
Verification Using a Petri Net Based Approach, M Barbeau, G v Bochmann
(Montreal U).
16.35--17.00: Error diagnosis in finite communicating systems,
A Rasse.
17.00--17.25: Temporal Precondition Verification of Design Transformations,
R Vemuri, A Sridhar.
TUESDAY, JULY 2
SESSION 5
9.00--9.25: Pam: A Process Algebra Manipulator, H Lin (Sussex U).
9.25--9.50: The Concurrency Workbench with Priorities, C T Jensen
(Aarhus U).
9.50--10.15: A Proof Assistant for PSF, S Mauw, G Veltink (Amsterdam
U).
10.15--10.40: Towards Imperative Program Testing Using Logic Program
Inversion, B J Ross (Edinburgh U).
10.40--11.10: Coffee Break
SESSION 6
11.10--11.35: Avoiding state explosion by composition of minimal covering
graphs, A. Finkel, L. Petrucci.
11.35--12.00: On the fly verification of behavioural equivalences and
preorders, J.C. Fernanadez, L. Mounier.
12.00--12.25: Bounded-memory algorithms for verification on the fly,
C. Jard, Th. Jeron.
12.25--14.00: Lunch
SESSION 7
14.00--14.25: Generating BDDs for Symbolic Model Checking in CCS,
R Enders, F Filkorn, D Taubner.
14.25--14.50: Vectorized Symbolic Model Checking of Computation Tree
Logic for Sequential Machine Verification,
Hiromi Hiraishi, Kiyoharu Hamaguchi, Hiroyuki Ochi, Shuzo Yajima.
14.50--15.15: Functional Extension of Symbolic Model Checking, T
Filkorn.
15.15--15.45: Coffee Break
SESSION 8
15.45--16.10: An Automated Proof Technique for Finite--state Machine
Equivalence, W Mao, G Milne (Strathclyde U).
16.10--16.35: From data structures to process structures, E Brinksma
(Twente U).
16.35--17.00: Checking for Language Inclusion Using Simulation
Relations, D L Dill, A J Hu, H Wong--Toi.
17.00--17.25: Semantics Driven Method to Check the Finiteness of CCS
Processes, N de Francesco, P Inverardi (Pisa U).
WEDNESDAY, JULY 3
SESSION 9
9.00--9.25: Using the HOL prove assistant for proving the correctness
of term rewriting rules reducing terms of sequential behaviour}, M
Mutz (Passau).
9.25--9.50: Mechanizing a Proof by Induction of Process Algebra
Specifications in Higher Order Logic}, M Nesi (Cambridge U).
9.50--10.15: A Two-Level Formal Verification Methodology using HOL and
COSMOS, C--J Seger, J J Joyce (University of British Columbia).
10.15--10.40: Efficient Algorithms for Verification of Equivalences
for Probabilistic Processes, L Christoff, I Christoff (Uppsala U).
10.40--11.10: Coffee Break
SESSION 10
11.10--11.35: Partial-Order Model Checking: A Guide for the Perplexed,
D K Probst, H F Li.
11.35--12.00: Using partial orders for the efficient verification of
deadlock freedom and safety properties, P Godefroid, P Wolper.
12.00--12.25: Complexity Results for POMSET Languages,
J Feigenbaum (AT&T), J A Kahn (Harward).
12.25--14.00: Lunch
SESSION 11
14.00--14.25: Mechanically Verifying Safety and Liveness Properties
of Delay Insensitive Circuits, D M Goldschlag.
14.25--14.50: Automating most parts of hardware tools in HOL, K
Schneider, R Kumar, T Kropf.
15.00--22.00: Excursion & Banquet
THURSDAY, JULY 4
SESSION 13
9.00--9.50: Invited Speaker, Joseph Sifakis (IMAG): Timed
Specification Formalisms: an overview.
9.50--10.15: Minimum and Maximum Delay Problems In Real-Time Systems,
C Courcoubetis, M Yannakakis (AT&T).
10.15--10.40: Formal Verification of Speed-Dependent Asynchronous
Circuits Using Symbolic Model Checking of Branching Time Regular
Temporal Logic, Kiyoharu Hamaguchi, Hiromi Hiraishi, Shuzo Yahima.
10.40--11.10: Coffee Break
SESSION 14
11.10--11.35: Verifying Properties of HMS Machine Specifications of
Real-Time Systems, A Gabrielian, R Iyer.
11.35--12.00: A Linear Time Process Algebra,
A Jeffrey (Chalmers)
12.20--12.25: Deciding Properties for Regular Real Timed Processes,
U Holmer, K Larsen, W Yi.
12.25--14.00: Lunch
SESSION 15
14.00--14.25: From S/R models to Boolean processes, C. Corcoubetis,
S. Graf, J. Sifakis.
14.25--14.50: Comparing Generic State Machines, M. Langevin, E.
Cerny.
14.50--15.15: An Automata Theoretic approach to Temporal Logic, G G
de Jong.
DEMONSTRATIONS
Please find enclosed a call for demonstration of (verification) tools.
Demonstration of tools is planned to take place during coffee breaks
and in parallel with presentations neighbouring coffee breaks. The
demonstations will take place near the Auditorium for presentations.
LOCATION AND ACCOMMODATION
Aalborg is the fourth largest city of Denmark with approximately
200.000 inhabitants, and is situated approximately 100 km north of
Aarhus. Moreover, Aalborg is very close to the Danish west coast
(approximately 40 km to Blokhus and L{\o}kken) which is certainly well
worth a visit in the summer.
The organizers have arranged for accommodation at Limfjordshotellet
(single DKK 550,- and double DKK 800,-), andc in addition at an
unspecified hotel of tourist standard (in the range DKK 300,- --
500,-). All hotels are conveniently situated in the very center of
Aalborg and not far from the railway station.
Please find enclosed with this program a hotel
reservation form. Deadline for hotel reservation is May 24th.
The workshop itself will take place in the buildings of Aalborg
University, which is some 7 km from the
city center. Transportation between the hotels and the University
will be provided, and in addition one may use the existing bus
services number 11 and 20.
TRANSPORTATION
If you want to travel by plane, there are several daily connections
from Copenhagen. When arriving at Aalborg Airport, you can
conveniently use the special Airport bus (approximately DKK 25,-) towards
Aalborg city as it stops just opposite Limfjordshotellet (the very
first stop after the Limfjords--bridge). Alternatively, you can take
a taxi, costing approximately DKK 70,-.
If you arrive at the Railway Station in Aalborg you be just opposite
Park Hotel; to go to Limfjordshotellet you may choose to take a 10
minutes walk (there is a city map inside the arrival hall of the
Railway Station) or you may take a taxi (approximately DKK 30,-).
REGISTRATION
Please find enclosed with this program a registration form.
The prize for registration (DKK 1600,-) includes proceedings and a copy
of the final LNCS publication, transportation between hotel and
University, lunches, reception, excursion, and workshop banquet. Deadline for
registration is May 24th.
A registration desk will operate in Limfjordshotellet on Sunday, June
30, 7--9 pm. From Monday through Thursday, there will be a
registration and information desk outside the Auditorium at the University.
ADDRESSES AND TELEPHONES
You may find the following addresses useful:
Limfjordshotellet, Ved Stranden 14--16, 9100 Aalborg. Phone
+45 98164333. Telex: 69516 lim; Telefax: +45 98161747.
Kim Guldstrand Larsen, Aalborg University Center, Fredrik
Bajersvej 7, 9220 Aalborg. Telephone: +45 98158522 (through
switch board) or +45 98 154211 (wait--for--tone) 5017
(direct). E--mail: kgl@iesd.auc.dk.
Telefax: +45 98158129.
SOCAIL EVENTS
Sunday, 30 June, 19.00--21.00: Opening registration and gatering
at Limfjordshotellet, Ved Stranden 14--16.
Monday, 1 July, 19.00: Reception at the Art Museum of North
Jutland.
Wednesday, 3 July, 15.00: Excursion to the Danish west coast (Slette
Strand --- remember to bring swimming suits!) followed by Workshop
banquet. Transportation by bus leaving at 15.00 from the
Auditorium at the University.
C O N F E R E N C E O R G A N I Z A T I O N
STEERING COMMITTEE
E.M. Clarke (Carnegie--Mellon University),
R.P. Kurshan (At\& T Bell Laboratories),
K.G. Larsen (Aalborg University),
A. Pnueli (Weizmann Institue),
J. Sifakis (LGI--IMAG).
ORGANIZING COMMITTEE
K.G. Larsen, A. Skou (Aalborg University).
PROGRAM COMMITTEE
Gregor Bochmann (U. Montreal),
Robert Brayton (U. California, Berkeley),
Ed Brinksma (Twente U.),
Randy Bryant (Carnegie Mellon),
Rance Cleaveland (N.C. State),
Olivier Coudert (Bull),
Costas Courcoubetis (U. Crete),
David Cohen (Bell Core),
Werner Damm (U. Oldenburg),
David Dill (Stanford U.),
Allen Emerson (U. Texax, Austin),
Masahiro Fujita (Fujutsu),
Orna Grumberg (Technion),
Hiromi Hiraishi (Kyoto U.),
Gerard Holtzmann (AT&T Bell Labs),
Bengt Jonsson (SICS),
Kurt Keutzer (AT&T Bell Labs),
Harry Lewis (Harvard),
Michael Lightner (U.Colorado),
George Milne (U. Strathclyde),
Willem deRoever (Kiel U.),
Prasad Sistla (GTE Labs),
Colin Stirling (Edinburgh U.),
P.A. Subrahmanyam (AT&T Bell Labs),
Pierre Wolper (U. Liege),
Michael Yoeli (Technion).
-cut---------------------------------------------------------------------
C A V 9 1 R E G I S T R A T I O N F O R M
Name: ________________________________________
Organization: ________________________________
Address: ________________________________
________________________________
________________________________
________________________________
________________________________
Phone: ________________________________________
FAX: ________________________________________
E-mail: ________________________________________
Date: _____________ Signature: ______________
The registration fee is DKK 1600,-. It covers workshop lunches and
refreshments, the participant proceedings, reception, and an
excursion (including the banquet dinner) on July 3rd to the west coast
of Northern Jutland.
PAYMENT:
Payment of registration fee should be made by banker's cheque drawn on
a Danish bank and in Danish Kroner (private cheques will not be
accepted). The cheque should be made payable to:
CAV '91, c/o Aalborg Tourist Bureau, {\O}steraa 8, DK-9000 Aalborg,
Denmark.
Please return this form and PAYMENT NOT LATER THAN MAY 24th to
the registration secretary:
CAV '91
Aalborg Tourist Bureau
{\O}steraa 8
DK-9000 Aalborg
Denmark
phone: $+$45 98 12 63 55
fax: $+$45 98 16 69 22
The form may be sent via telefax followed by the cheque via snailmail.
-cut------------------------------------------------------------------------
C A V ' 9 1 H O T E L R E S E R V A T I O N F O R M
Name: ________________________________________
Organization: ________________________________
Address: ________________________________
________________________________
________________________________
________________________________
________________________________
Phone: ________________________________________
FAX: ________________________________________
E-mail: ________________________________________
Please reserve hotel room for me according to the following:
Single Double
Limfjordshotellet _ _
(single room DKK 550,-, (_) (_)
double room DKK 800,-)
Unspecified hotel of tourist _ _
standard in the range of DKK (_) (_)
300,- to 500,-
Date of arrival: ____ Date of departure: ______
Date: _______________ Signature: ______________
Please return this form NO LATER THAN MAY 24th to
the registration secretary:
CAV '91
Aalborg Tourist Bureau
{\O}steraa 8
DK-9000 Aalborg
Denmark
phone: $+$45 98 12 63 55
fax: $+$45 98 16 69 22
The form may be sent via telefax.
--cut----------------------------------------------------------------
C A V ' 9 1 D E M O N S T R A T I O N F O R M
During the conference there will be arranged sessions for
demonstration of verification tools. For those of you who want to use
this opportunity, please indicate your requirements below concerning
hardware and software for such a demonstration. As a standard
facility we will make a number of SUN4 machines available (SUN UNIX-OS
version 4.1.1), and we will offer to initiate the execution of
standard installation jobs before the conference. Also, we will on
request make accounts available for running FTP's and remote
installation jobs. Requirements going beyond the above will be
fulfilled as far as possible, but our resources are limited. For
example, we have a number of MAC's and we can also contact the
computing center of our campus in order to allow for remote usage of
VAX's. (The campus is covered by an Ethernet).
The filled out form should be returned to one of the local organisers
(Kim Larsen, Arne Skou) at Aalborg University, Department of
Mathematics and Computer Science, Fredrik Bajersvej 7, Bygn. E,
DK-9220 Aalborg, DENMARK
NAME OF TOOL: ________________________________________
NAME OF AUTHOR(S); ___________________________________
ADDRESS OF AUTHOR (including e-mail, fax, phone):
______________________________________________
______________________________________________
______________________________________________
______________________________________________
______________________________________________
REQUIREMENTS: machine, OS, disk, RAM, Windows, remote
connection,..
______________________________________________
______________________________________________
______________________________________________
______________________________________________
-cut---------------------------------------------------------------------
--
Arne Skou Internet: ask@iesd.auc.dk
Institute for electronic systems Aalborg University
Fredrik Bajers vej 7, 9220 Aalborg
DENMARK. (W) +45 98 15 85 22 (H) +45 98 39 17 81
--
=========================== MODERATOR ==============================
Steve Stevenson {steve,fpst}@hubcap.clemson.edu
Department of Computer Science, comp.parallel
Clemson University, Clemson, SC 29634-1906 (803)656-5880.mabell