Sunday 7-9 pm, 21 March
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.
24 March 1999
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.
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.
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: