Monday, November 06, 2006

Welcome to the AFM Blog

Welcome to the Applied Formal Methods Blog, founded by the KindSoftware Research Group.

In this blog my friends and I will post about software engineering with applied formal methods.

As none of us are big bloggers, do not expect a ton of content.

But we hope that what we do write will, as a result, be interesting and useful to you, our readers.

Please contact us if there are particular topics in AFM you would like us to comment upon.

Or, if you are a user or researcher of AFM and are interested in contributing, drop us a line.

-Joe Kiniry

powered by performancing firefox


Anonymous Anonymous said...

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 formalsemantics of an idealized programming language. The program to be
verified is first translated into this intermediate language. As far as I under- stand - 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.

04 December, 2006 15:29  

Post a Comment

<< Home