Sunday 7-9 pm, 21 March
Novotel Amsterdam
All ETAPS'99 participants are encouraged to register on Sunday evening at the Novotel, Europaboulevard 10, Amsterdam. The hotel is close to the RAI railway/metro-station. Once you're at that station you cannot miss the Novotel. Free drinks will be served from 7 to 9 pm. Other possibilities to register for ETAPS'99 are on Monday morning from 8 am onwards at the Royal Tropical Institute (KIT)
Reception by the Mayor and Aldermen of the City of Amsterdam
Monday 6.45-7.45 pm, 22 March,
City Hall Amsterdam
All ETAPS'99 participants are invited to the Amsterdam City Hall for a reception, offered by the Mayor and Aldermen of the City. Busses will leave from the conference site between 6.15 and 6.30. The reception will take place in the "Boekmanzaal" of the City Hall. City Hall is part of the Opera/Cityhall complex, Located alongside the Amstel at Amstel 1.
Tuesday, 7-11 pm, 23 March,
Kapitein Kok Amsterdam.
The ETAPS'99 banquet will be held on a traditional Dutch wheelboat touring the IJsselmeer (a former branch of the Northsea). Busses will leave from the conference center between 6.15 and 6.30 pm to head for the pier where the Kapitein Kok is moored. The pier can be found at the Oostelijke Handelskade near the Amsterdam Passenger Terminal (just in case you miss the bus). After the tour the boat will moor at Amsterdam Central Station.
 |
Soiree |
24 March 1999
Speakers
Abstract
Object-oriented programming is among our most effective techniques
for managing complexity. In places, this has led to the belief that everything
is best tought of as an object and best represented in a program as an
object. However, not everything is an object and not every object is best
represented using a single language mechanism. I will give a few examples
of what can usefully be considered objects and what are best thought of
as non-objects. I will discuss a few aspects that can make an object useful
in a system.
I illustrate these ideas using C++ examples.
Abstract
Symbolic Model Checking has proven to be a powerful technique for the verification
of reactive systems. BDDs have traditionally been used as a symbolic representation
of the system. We show how boolean decision procedures, like Staalmarck's
Method or the Davis & Putnam Procedure, can replace BDDs. This new
technique avoids the space blow up of BDDs, generates counterexamples much
faster, and sometimes speeds up the verification. In addition, it produces
counterexamples of minimal length. We introduce a bounded model checking
procedure for LTL which reduces model checking to propositional satisfiability.
We show that bounded LTL model checking can be done without a tableau construction.
We have implemented a model checker BMC, based on bounded model checking,
and preliminary results will be presented.
Reception
After the two speakers at the CWI soiree, CWI requests the pleasure of your company at a reception from 10 - 11.30 pm at the ETAPS conference site. The program of the CWI soiree is as follows: