Boogie Workshop

I recently attended the Boogie workshop on intermediate verification languages in Wroclaw, Poland.

First let me recall that one goal of the Hi-Lite project is to bring formal verification to the Ada language. An intermediate verification language (IVL) can help here because it deals with the most common features that exist in most programming languages: integers, arrays, sequential programming, loops, function calls. There was no need for us in Hi-Lite to reinvent the wheel, we simply picked a suitable IVL.

There are two main IVLs in the research community, namely Boogie[1] (hence the name of the workshop) and Why[2]. In the Hi-Lite project, the natural choice was Why, as the Why developers are also part of the project.

Besides talks discussing various improvements in these two main tools, there was also a talk about a new IVL called jStar, mainly targeted at complex programs with shared mutable state, and the very interesting invited talk by Viktor Kuncak[5] showed some ways of using IVLs to develop new programming techniques.

The workshop website[3] contains a list of all the talks. It is also worth mentioning that it is part of the CADE 23 conference[4] which takes part in Wroclaw all week.

[1] http://boogie.codeplex.com/
[2] http://why.lri.fr
[3] http://research.microsoft.com/en-us/um/people/moskal/boogie2011/
[4] http://cade23.ii.uni.wroc.pl/
[5] http://lara.epfl.ch/~kuncak/

This entry was posted in Open-DO News. Bookmark the permalink. Post a comment or leave a trackback: Trackback URL.

Post a Comment

Your email is never published nor shared. Required fields are marked *

*
*
 
  • Categories

  • Open-DO Projects

  • Contact

    info @ open-do.org