The Formal Methods World Congress (FM´99)

By Paul Pettersson.

The Formal Methods World Congress (FM'99) was organized in Toulouse the 20th to 24th of September this year. With its 520 visitors, 31 technical symposia sessions, 12 user group meetings, 12 industrial tutorials, and formal methods tool exhibitions it must certainly be considered one of the main event in the formal methods community in the year of 1999.

The invited speakers at FM99 were Gilles Kahn, C.A.R Hoare, Cliff B. Jones, Amir Pnueli (two invited talks), John Rushby, Joseph Sifakis, Michael A. Jackson, and Gerhard Holzmann. I found many of their talks very interesting as the speakers often gave their personal view of the current status of formal methods (and formal method tools), both in academia and their use in industry. Some invited speakers also identified future directions and goals of the use of formal methods. A general recurring statement in several talks (including Amir Punueli's and John Rushby's) was that the industry seems to be more attracted to automated formal techniques, such as model-checking, than to the currently available deductive methods, such as theorem proving. It was argued that engineers in general prefer model-checking tools because they support a way of working that the engineers already are used to, whereas theorem provers often requires domain specific expert knowledge that the engineers are lacking.

One of the main events at FM'99 was the well organized exhibition, were as many as 32 exhibitors showed their products (mostly formal method tools, methods and computer science books). I (together with Alexandre David, Uppsala University) took part in the exhibition to launch a new version of the verification tool UPPAAL. It turned out that the exhibition was exactly the right place for doing that. Our exhibition, and the new UPPAAL version, received a lot of attention and we were often busy giving demos. The tool developers at the exhibition were also invited to model and analyze a given problem in a competition. We also did so, but the jury did not rank our contribution among the three winners.

Of course, a number of interesting papers/talks were presented at FM'99. Here I very briefly review some of them:

• Error Detection with Directed Symbolic Model Checking, by F. Reffel and S. Edelkamp, in LNCS number 1708, pages 195 to 211: It is described in the paper how a heuristic directed search of the state-space (instead of standard depth-first or breadth-first) is used to reduce the space and time consumption of a verification algorithm. An experiment is presented where the technique is shown to work very well when applied to models with seeded errors.
  
  
• Deduction is Forever, by Amir Pnueli: In this talk Amir Pnueli discussed how the deductive methods will eventually take their rightful place as a verification technique for circuits. He also gave a list of (necessary) conditions on the ultimate verification tool. It must be: specific to an application area; all verification conditions should be automatically resolvable (i.e. no need for interactive proving); invalid verifications must yield usable and focused counter-examples; the need for cleverness should be factored into familiarity with the verified design.
  
  
• Applying Model Checking in Java Verification, by K. Havelund and J. Ulrik Skakkebæk, LNCS number 1680, pages 140 to 155: In this case study paper the authors describe how their recently developed Java to Promella translator, called Java Pathfinder (JPF), has been applied to verify a Chinese Chess game server application written in Java. The translation implemented in JFP is described as well as the sub set of JAVA translated by the tool.

To conclude this travel report, I wish to state that FM'99 was a very enriching experience for me. It gave me many ideas for future research.

Submitted: Wed, 03 Nov 1999 14:19
By: Paul Pettersson
At: BRICS, Aalborg University