Letters to Participants

Letters  1  2  3  4 

Letter 1

We are happy to invite you to a 3 day workshop on proving liveness of infinite-state systems (aka "Beyond Safety", or "Progressing to Progress") to be held in the beautiful Schloss Ringberg (see http://www.rzg.mpg.de/ringberg-castle/), on April 25--28, 2004. An informal description of the workshop follows. We have restricted the number of participants to 25, to fit the length and the intended depth of the meeting. Consequently, we would appreciate if you can let us know whether you can attend in the next few days.

Hope to hear from you soon & Happy New Year!

Andreas, Bernhard, and Lenore

Letter 2

We are delighted that you will join us in the "Beyond Safety" workshop. We will shortly send some practical information as well as tentative schedule for the first day. We set up a web page, http://www.cs.nyu.edu/acsys/beyond-safety that will contain updated information. There you can find:

  1. list of confirmed participants
  2. the "Accellera report" (courtesy of Intel) that has a list of 70+ sample properties supplied by industry and their treatment in various methods. Some (although few) of these properties are "pure iveness." We will post a document that only contains those
  3. whatever else we think may be of interest

So you may want to occasionally check this site.

Meanwhile, we'd like to assemble a list of your opinions about "What is liveness and what types of liveness properties (if any!) are important for software verification." If you can send us a (<= 5 lines) Liveness Manifesto we will post it.

Looking forward to seeing you in April (if not before),

Andreas, Bernhard, and Lenore

Letter 3

We'd like to give you some update about the upcoming workshop. In this note you'll find

  1. travel related information
  2. tentative program


On the web-page (http://www.cs.nyu.edu/acsys/beyond-safety) there are directions how to get to Schloss Ringberg. If you send Lenore your (plane) arrival time it will be posted so you can coordinate travel. Andreas can assist with rental cars (MPI has special rates with EuroCar). If you arrive in Munich on Saturday (like the three organizers do), you can book a room in the Hotel Stephanie, in the nice, central Munich neighborhood "Schwabing," Trkenstr. 35, Tel +49 89 2881400, Fax +49 89 2814049; we pre-reserved a number of rooms until April 17 (please give the code name "liveness" when you do the reservation). We have reserved a table in a nice restaurant for Saturday evening (nice, not Bavarian). Please tell us if you are interested. To find out about trains from Munich airport to Tegernsee train station, you may use http://reiseauskunft.bahn.de/bin/query.exe/e.


We'll start on Sunday evening, with each of you getting a list of the "Liveness Statement" made, and the names of the people who made them. ** YOU SHOULD THEREFORE SEND YOURS IF YOU HAVE NOT ALREADY DONE SO ** You'll be asked to guess who made which statement. This could be quite hard since some people gave two (moreover, contradictory) statements! We will also go through the liveness properties in the Accelra Document (posted on the web) and an termination example from a window device driver (given to us by Byron Cook).

On Monday and Tuesday we'll have 2 sessions each day -- morning and afternoon, and one on Wednesday. Sessions chairs will be appointed and they will invite participants for "their" sessions. We will post information on the web page as it stabalizes. We are also planning a "5-minute madness session" one evening, discussion groups followed by summarizing presentations by the group leader (again, we'll post details as they are finalized) and panel discussions.

And, while preparing all this, we'd appreciate you suggestions and comments.

See you in 2.5 weeks!

Andreas, Bernhard, and Lenore

Letter 4

After our mail of two days ago we got various responses which made us re-think the structure of the workshop -- instead of having 5 sessions composed by sessions chairs, we'd like each of you to let us know whether you'd like to
   - present your work (emphasis on perspective on established work, rather than yesterday's new results, these will be presented in the evenings),
   - participate in / organize a panel discussions (on liveness-related issues), or
   - just be part of an active audience. Once we get your responses, we'll divide the presentors/panelists into sessions and make announcements accordingly.

Andreas, Bernhard, & Lenore

« back  |  home  |  top ^