Project Title:

An Intermediate Language for Formal Verification Tools

06.03-2020
900856
An Intermediate Language for Formal Verification Tools

Abstract:

This project will investigate an intermediate formal language for integrating formal
verification tools. Such a language would allow different tools such as theorem provers,
decision procedures, and formula generators to be used in the same environment either
through translating the various tools' formal languages into the intermediate language
and back or by using the intermediate language as an internal form which is shared
between tools. The ability to integrate different verification tools will significantly
enhance the usefulness of formal verification in developing reliable software. The
project objectives are to formulate a candidate intermediate formal language and
to define translation algorithms between the intermediate language and two existing
formal languages from different formal verification environments. The approach will
be to examine a collection of formal languages form existing formal verification
environments and formulate a candidate intermediate language which is expressive
enough to translate the existing languages into. It will then choose two existing
languages from different environments and define algorithms to translate them into
the intermediate language and back. This will demonstrate the feasibility of the
intermediate language for connecting different tools. The results will be a candidate
intermediate language and the translation algorithms.
Formal verification environments and tools integrated into existing software engineering
can be marketed as products in their own right or be used to produce high quality,
reliable software products.
formal verification tool integration intermediate language