|
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:
- list of confirmed participants
- 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
- 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
- travel related information
- tentative program
Travel:
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.
Program:
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
|
