Saturday, November 18, 2006

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: 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
  • 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: If we have missed essential intermediate representations, please point them out to us! -Joe Kiniry

Labels: , ,


Blogger Joe Kiniry said...

Peter Schmidt wrote me about this blog entry. Below is his email.


Thank you very much for initiating this discussion.

What I wanted to say at this point is:

The concept of intermediate representation needs further differentiation.

First, there are intermediate programming languages. Every program verification system needs at some point a precise semantics of the programming language it targets. Since real live programming languages abound with a lot of accidental details and unsystematic peculiarities most verification systems use a formal semantics of an idealized programming language. The program to be verified is first translated into this intermediate language. As far as I understand - others may correct me if this is wrong - this translation is a best effort job. From the languages you quoted BoogiePL and Why fall into this category.

Second, there are specification languages. I a sense they can be perceived as intermediate, intermediate i.e. between a high-level specification (using e.g. natural language or UML) and the input language of a theorem prover. Among the named languages JML and BML belong into this category.

Third, there are proof obligation languages. I do not like the name, but could not think of a better one from the top of my head. They are intermediate in that they are not tied to a specific prover. The SMT-LIB language seem to be a promising candidate for a format accepted by many groups. The TPTP, also mention in your account is primarily a collection of benchmark tests. But, relevant since it includes conversions algorithms into the input language for a dozen of automated theorem provers.


Fakultät für Informatik
Universität Karlsruhe

16 December, 2006 10:03  
Blogger Joe Kiniry said...

Thank you Peter for your input.

I completely agree with your characterization of intermediate representation(s). Indeed, each of these kinds of languages sits somewhere between the original language on which we are verifying (e.g., Java source or bytecode) and the theory in which we reason (e.g., a semantics for the Java VM).

Each facet you exhibit is essential the larger picture that is full program verification. Each is complex, fulfills a different role, and requires a non-trivial amount of theoretical and engineering effort. It is exactly because of these challenges that we should focus our attention on using, supporting, and evolving these high-quality de facto languages and tools.

I believe that, given the resources at our disposal as researchers in applied formal methods, the only time we should create or extend a new language is when we simply cannot express and reason about a (set of) concepts in one of the existing languages.

For example, I am very dissatisfied with UML because it is terrifically complicated and most of it has no semantics. Therefore, it is useless to me because I cannot say what I need to say and verify. This is why I use the (E)BON specification language instead.

Thanks again for your clarifications and input Peter!


16 December, 2006 10:11  

Post a Comment

<< Home