VDM to HOL model and proof obligation translation

One recent addition to the Overture project is an Automatic Proof Support system, developed by Sander Vermolen.

In our work we make much use of this system's translator, as well as the proof tactics.

We have contributed in widening the translator VDM++ syntax knowledge, implementing some basic (but essential to have recursive functions translated) operators like hd (head), tl (tail), len (length) and ^(concatenation).

Another contribution is the pre-processing script and parsers, that allow us to automaticaly pre process a VDM++ model to be translated (including its proof obligations), the complete package with source can be found here.

Links

News Flash

  • Refresh at public area projet information MiguelFerreira - 8 Mar 2008

  • Added the first files for the Intel Flash File System Core specification

  • Added new references on the flash memory subject MiguelFerreira - 6 Dez 2007

  • Added POSIX extracts of some system interfaces (open, mkdir, opendir, close, closedir, rmdir, unlink) MiguelFerreira - 30 Nov 2007

  • Added alloy library and updated bib file SamuelSilva - 19 Nov 2007

r1 - 19 May 2008 - 07:04:23 - MiguelFerreira
This site is powered by the TWiki collaboration platformCopyright © by the contributing authors. All material on this collaboration platform is the property of the contributing authors.
Ideas, requests, problems regarding TWiki? Send feedback
Syndicate this site RSSATOM