[Termtools] minutes of WST business meeting

Thu Aug 24 15:23:14 CEST 2006

Please find below the minutes of the WST business meeting as written
down by Harald Sondergaard.

For the competition the main facts are:

* The organising committee of the competition now consists of Claude
Marche, Johannes Waldmann and me.

* We will take care of archiving this termtools list.

* The next competition will be short before WST 2007, so in June 2007.

            Best regards, Hans Zantema.

_________________________________________________________
Dr Hans Zantema            
Technische Universiteit Eindhoven, Department of Computer Science 
P.O. Box 513, 5600 MB Eindhoven, The Netherlands 
e-mail: H.Zantema at tue.nl, homepage: www.win.tue.nl/~hzantema
office: Hoofdgebouw room 6.73, tel: (040)2472749

WST 2006 Business Meeting, Seattle, 15 August 2006, 17:10

Alfons Geser welcomed all to the meeting and gave a short report from
the WST 2006 chairs.  

Selection of papers
-------------------
Concerns were raised that the reviewing process in 2006 may have been
too rigorous, undermining the informal character of the event.  Some
referees' comments suggested an unawareness of this informality.
It was explained that the number and detail of referee reports had not
been stipulated beforehand - these were simply a result of PC members'
willingness to contribute comments, and that the workshop's aim of being
open to all papers that were both sound and within scope had been stated
clearly in the PC discussions.  Practically all reviews were produced by
the PC and all submitted papers had been accepted.

Next WST
--------
Ralf Treinen was invited to present the plans for RTA/TLCA in Paris
25-29 June 2007.  The aim is to have 6 or 7 pre- and post-workshops,
each of one day's duration.  A spot had been reserved for WST.  The six
workshops that had signed up were: HOR, RULE, UNIF, SecRET, WFLP and
WRS.  The location will be CNAM, centrally located  on the right bank.
Regular registration fees were expected to be below Euro 250 for the
conferences (with lunch, coffee, banquet, proceedings) and below Euro 70
for workshops (with lunch and coffee, as well as access to concurrent
workshops).

In the subsequent discussion, it was pointed out that the 2004 Business
Meeting had decided to run WST every two years only, to ensure that
enough papers would be submitted, and that RTA 2007 was only 10 months
away.  On the other hand it was argued that Paris is an attractive venue
and easy to reach for the bulk of the termination community.  There was
a good deal of concern about the changing nature of WST: in the old days
the workshop was held in at a secluded venue, stretched over several
days, with longer talks and more time for informal discussion.  A
one-day workshop in 2007 would continue an unfortunate trend.  There was
also concern about the increasing competition with related workshops.

Hans Zantema made it clear that a decision about a WST 2007 was
independent of the Termination Competition 2007, which would run in any
case.

A vote was taken on the proposal to have a WST 2007 in Paris, affiliated
with RTA 2007.  In favour 9; against 5; abstained 5.  
Hence the motion was passed.  Following the last years'
tradition, the 2006 chairs will identify two chairs for WST 2007.

The Termination Competition
---------------------------
Hans Zantema had earlier reported on the 2006 competition and reiterated
its aim of stimulating research, driving innovation and shifting
emphasis towards automation.  It also serves as a vehicle for growing
the TPDB.  The point is not to win but to have a reliable benchmarking
tool, allowing, for example, to prove that some termination tool solves
some problem no other tool can handle.

Hans found a May-June competition in 2007 feasible, with results
reported at WST/RTA.  Only few changes were needed.  It might be time to
extend the competition to other programming paradigms.
Also, the second round should be dropped, as it had made little
difference, only more work.

Aart Middeldorp raised a number of issues.  First, the competition
format makes does not encourage newcomers to enter, as it is very
difficult to be competitive in any category without years of accumulated
know-how.  Second, the format hides the impact of new ideas and
technologies - there is little honour to win for, say, a specialised
matrix method tool or a new poSAT based tool up against the armoury of
established tools, in spite of the innovation they represent.
Innovations then do not get proper recognition.  To encourage progress,
should there be categories for specialised tools?  Finally, to make the
competition more exciting, it should run over shorter time: a smaller
time-out, using just a random subset of the TPDB.

But this year's competition had in fact shown that it was not impossible
for new entries to make their mark.  Besides, it was argued, more
categories would be unmanageable, and who would be entitled to decide
the categories?

This led to a suggestion that the competition should have a steering
committee.  

It was mentioned that for a given problem instance, the SAT competition
allocates more points the fewer the other tools that solved it, thus
rewarding progress on difficult cases.

There was broad agreement that the current format does not make it
transparent what an individual technique contributes, nor how its
different implementations compare.  From the reporting, one should be
able to read not just overall results, but also be able to zoom in on
techniques.  Could reporting include statistics on the techniques used?

It was argued that a focus on techniques could be unmanageable.
Also, new techniques arrive - last year nobody could predict that all
winning tools in 2006 would use SAT solving.

Several felt that more openness would serve the aims of the competition
better.  Time is wasted when everybody need to reimplement everything
all over.  The proper solution is to standardise, to modularise tools
better and encourage researchers to make their software more open,
possibly even making all tools open source.

A discussion followed on whether modularisation could be achieved.
It was suggested that a strategy definition language a la Aprove's could
be made a standard.  There is also an urgent need to complete current
work on a proof verifier and to provide a general scheme for formatting
proofs taking yet-to-be-formalised new techniques into account.

There was concern that discussion on the termtools mailing list no
longer is archived.  

Discussion returned to the suggestion that a competition steering
committee be formed, and its ideal size.  After some debate, Hans
Zantema proposed the simpler scheme of extending the organising
committee to three members.  In addition to Claude Marche and Hans
Zantema, Johannes Waldmann was nominated and agreed to join.
Members of the extended committee expressed a willingness to take new
initiatives, drive continued discussion, and implement changes based on
the discussion.

The meeting closed at 18:50.

Harald Sondergaard
16 August 2006

-- 
Harald Sondergaard              Dept. of Computer Science and Software
Eng.
mailto:harald at cs.mu.OZ.AU            The University of Melbourne, Vic.
3010
http://www.cs.mu.oz.au/~harald/
Australia
_______________________________________________
Termtools mailing list
Termtools at lists.lri.fr
http://lists.lri.fr/mailman/listinfo/termtools