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
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
posted by Joe Kiniry at 11:49 PM
1 Comments:
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.
Post a Comment
<< Home