SAVCBS 2007

In the beginning of September I attended SAVCBS in Cavtat, Croatia. The place is beautiful, with landscapes in the style of the Pirates of the Caribbean. The focus of the workshop is on components, but a good proportion of people who run it are from the formal methods world. The presentation I liked most was that of Ádám Darvas. One reason why I liked it is that I am familiar with the subject so I was able to understand. He talked about what model classes are good for and how to encode them in first-order logic so that theorem provers can reason about them. The first previous solution is to give an encoding using uninterpreted functions. The second previous solution is to use the built-in theories of the theorem prover. ESC/Java does neither. Model classes are specified using normal JML and that will roughly get translated by ESC/Java into uninterpreted functions for the theorem prover. That translation is probably slightly worse than a handcrafted translation. And Ádám claims that the problem with the handcrafted translation into uninterpreted functions is performance, which sounds quite probable. The reason theorem provers have built-in theories is performance, while in principle uninterpreted functions are good enough for everything.

Ádám presented a systematic way of encoding model classes using higher-order provers built-in theories. A simple and powerful idea. I forgot to ask him while I was there what he things about using his method for an automated prover.

By the way, Ádám is Hungarian and on my way back to Bucharest I stopped for a little while in Budapest, which appears to be a beautiful city. I certainly have to go there again. Now I am in Liverpool, a rather sad city, attending FroCoS and FTP.