10 Years of Verification in Cachan: Part I

On November 26 and 27, Anna and I were in Paris for 10 Years of Verification in Cachan, a two-day workshop organized by the Laboratoire Spécification & Vérification (LSV) of the ENS Cachan to celebrate its 10th anniversary. The workshop was centered around two special award ceremonies honouring two very good colleagues and friends of ours: Patricia Bouyer received CNRS's 2007 Bronze Medal for Computer Science (Monday 26th November), and Kim G. Larsen became Doctor Honoris Causa at ENS Cachan (Tuesday 27th November).

Despite being very busy and getting nowhere fast, we felt that we really ought to make the trip to Paris for this event, to which the organizers had kindly invited us to contribute talks. We were visiting professors at LSV in May 1998, when that laboratory was in its infancy, and we have very fond memories, both scientifically and socially, from that stay. In fact, our connection with LSV started informally long before that time when François Laroussinie and I shared an office in Aalborg for about a year starting from the autumn 1994 (when BRICS started its activities).

Today, there is little doubt that LSV is one of the hotbeds of TCS research in the Paris area, where there is really no shortage of talent and of extremely strong CS departments covering the whole gamut of TCS research. According to Philippe Schnoebelen, the present director of LSV, the centre now has about 40 members, and since its inception it had graduated 33 PhD students, seven of whom have been hired by CNRS. This is just one of the many indications of the success achieved by LSV over the first ten years of its existence. To my mind, another definite sign of impact is the number of former members of the laboratory who have taken up high-profile academic positions elsewhere. Here is what I could find on the LSV web site.

• François Laroussinie has become a full professor at University Paris-Diderot (Paris 7).
• Ralf Treinen is a full professor at University Paris-Diderot (Paris 7).
• Hubert Comon-Lundh is on sabbatical leave at RCIS (AIST, Tokyo).
• Michel Bidoit is the Director of INRIA Futurs.
• Antoine Petit is the director of INRIA Paris-Rocquencourt.
• Béatrice Bérard is a full professor at University Paris-Dauphine.

The workshop was a really enjoyable event. We had a great time, listened to some excellent talks, met a lot of colleagues and friends, and tasted some very good food. The organization was simply superb, thanks to the sterling efforts of Philippe Schnoebelen, Thomas Chatain, and Stéphanie Delaune.

Apart from my presentation, which ended the event, the two-day workshop featured talks by André Arnold, Pierre Wolper, Kim G. Larsen, Claude Kirchner, Marta Kwiatkowska, Michel Bidoit, Patricia Bouyer, Anna Ingólfsdóttir, Wolfgang Thomas, and Colin Stirling. This was really an embarrassment of riches, and I learned a lot from all of the talks---even from the two delivered in French :-) The quality of the presentations by these colleagues was invariably high, and the talks offered very accessible introductions to several areas of research covered by the members of LSV.

It would take way too long to report on all of the presentations. In this post and in subsequent ones, I'll therefore limit myself to recalling a few opinions and trivia that I heard at the workshop.

In his talk 25 years of automata and verification, Pierre Wolper went on record as saying that "Complexity, as traditionally measured, is not very relevant in verification." To wit, in his talk he pointed out that verification algorithms with high worst-case complexity turn out to perform well in practice and are widely used. Prime examples are automata-theoretic algorithms for LTL model checking as well as those implemented in the tool MONA, which implements decision procedures for the Weak Second-order Theory of One or Two successors (aka WS1S/WS2S)---a theory that is not elementary-recursive, as shown by Albert Meyer in this seminal paper. On the other hand, he presented an example from his own work yielding efficient automata-theoretic algorithms for CTL model checking, which are not used in practice. His conclusion was that one cannot trust complexity results. (I myself have mixed feelings about this opinion of Wolper's. Maybe I'll devote a post to this topic when life is less hectic. In the meantime, I'd love to hear your opinion.)

Pierre Wolper also said that his LICS 1986 paper An Automata-Theoretic Approach to Automatic Program Verification (Preliminary Report) with Moshe Vardi, which eventually won the LICS Test-of-Time Award and formed the basis for their paper that won the Gödel prize in 2000, had been rejected by two or three conferences before being accepted at LICS 1986! He also recalled the following sequence of reactions by Gerald Holzmann to their automata-theoretic algorithms for LTL model checking:

1. "It must be wrong!"
2. "It is impractical!"
3. "It does not fit into SPIN!"

Eventually, the algorithm was implemented in SPIN, showing the power of elegant ideas in practice.

At the end of his talk, Pierre called for renewed efforts in implementing automata. I keep telling my students that automata are the most basic computational model in computer science, and I cannot help but share Pierre's call to arms.

I hope to report on a few other talks from the workshop when I have managed to catch up with a few of the items on my to-do list.