ESF Workshop on Challenges in Java Program Verification

From Monday to Wednesday, the 16-18 of October 2006, I participated in the European Science Foundation's workshop on "Challenges in Java Program Verification." This workshop was graciously organized by Reiner Hähnle from Chalmers University of Technology and Wojciech Mostowski from Radboud University Nijmegen. This workshop invited around twenty researchers working in Java program verification to come to Nijmegen, NL and give talk about recent work and, more importantly, talk with each other about our successes and failures as individuals and as a field, discuss where we should head next (again, collectively and individually), how we should organize ourselves, etc. I gave the opening talk on Tuesday at this workshop. My talk was called "Usable Formal Tools" and focused on the non-technical aspects of building a successful verification tool. On Wednesday afternoon I chaired a panel section called "Past Experiences and Lessons for the Future." The abstract for this panel was as follows:

Many of us actively took part in the development of a verification tool for OO languages. As in all research tools one has to make design and technology decisions that in the end may turn out to be suboptimal. Are there things that we can learn from each other? Which mistakes did we make in designing our verification tool? Which technologies worked and which didn't? Which lessons did we learn for the future?

Panel participants, and the tools with which they are associated, were:

• Erik Poll on the Loop tool
• Claude Marché on Krakatoa
• Peter Müller on Jive
• Joe Kiniry on ESC/Java2 (and a bit on Simplify and OBJ3)
• Steffen Schlager on KeY
• Mariela Pavlova on Jack
• Kurt Stenzel on KIV
• Rustan Leino on Boogie (and a bit on ESC/Java)
• Robby on Bandera, Bogor, and Kiasan

I asked each panel member to discuss at most two positive and two negative (not necessarily unique) things that they learned from their tool experiences. I took notes of the responses of the panel members. But what I present here is my interpretation of a much longer statement, so any errors are my own and I apologize for any mis-interpretations. (Panel participants please feel free to write responses or clarifications to this blog post.) Peter Müller:

• pros
• use someone elses prover on the backend
• use a small sound core logic (about 24 rules)
• cons
• working on a small language subset - use a real language instead
• underestimated the amount of work that is necessary to build a tool

Erik Poll:

• pros
• it is feasible to define a semantics of a real language (e.g., Java)
• reimplementation of a tool from scratch is sometimes necessary
• cons
• deep embeddings do not work well in practice
• underestimate workload and keeping tool alive and usable

Rustan Leino:

• pros
• use an intermediate language
• develop a rich test suite
• cons
• some aspects of the test suite are weak (completeness, coverage, evolution)
• documentation, particularly no document describing logic

Claude Marché:

• pros
• using an intermediate language works well
• support multiple provers (via the why tool)
• cons
• cooperating provers is very difficult or not possible
• underestimate work involved in building a tool and have few developer

Mariela Pavlova:

• pros
• splitting tactics and having a rich UI
• good intermediate representation
• cons
• underspecification of architecture, lack of documentation
• problems in semantics that prevent certain VC possibilities

Robby:

• pros
• design early and modularly
• bells & whistles for effective sales and use
• cons
• "quick and dirty" leads to dirty - aka don't overdesign
• complex architecture and code

Kurt Stenzel:

• pros
• use an existing foundation
• formal proof of properties of calculus and semantics
• cons
• good for complex interactive proofs, but bad for simple things
• limited manpower (i.e., no JML support)

Steffan Schlager:

• pros
• symbolic execution is an excellent reasoning technique
• JML support is crucial (i.e., use a "real world" language)
• cons
• using provers that use decision procedures does not provide any evidence
• core data structures overly focused on Java

Joe Kiniry:

• pros
• community support via growing a community and giving good support
• used real software engineering practices
• cons
• complexity of architecture and evolution, given history
• using real software engineering practices

Several audience members also had some things to contribute as well. In particular, Arnd Poetzsch-Heffter argued that, given the number of groups working on tools, and the fact that none of them have sufficient resources to accomplish all of their goas, some common tool foundation seemed to be necessary. This is not a unique perspective. A handful of us in the verification community have argued for such over the past several years. Unfortunately, like many other communities in Computer Science, the verification community is full of researchers who have Not Invented Here syndrome when it comes to developing new tools. I find this amusing and frustrating, given how many researchers have no problem at all standing on the shoulders of theoretical giants, but refuse to even sidle up to the big toe of the practical. It is our intention that the Mobius Program Verification Environment, on which we will write more later, be exactly such a common foundation. The other point made by several tool builders is a positive emphasis on intermediate representations. There now have emerged several high-quality intermediate representations which we in the Mobius community are convinced are the proper foundations for inter-operable, maintainable, long-lasting tool suites. In particular, we would like to draw your attention to the following (non-exhaustive) list of excellent intermediate representations with tool and community support:

• BoogiePL
• TPTP
• SMT-LIB
• Why
• JML and BML

If we have missed essential intermediate representations, please point them out to us! -Joe Kiniry