Hi,
Maybe not that "big" components, but we verified formally (in
Isabelle/HOL) some decision procedure implementations (mainly quantifier
elimination for linear real, integer arithmetic and their combination).
Using Isabelle's push button Technology you transform the formally
Isabelle/HOL implementation in to SML, Ocaml or Haskell.
Here are some pointers:
http://www.cl.cam.ac.uk/~ac638/pubs/pdf/mir.pdf
http://www.cl.cam.ac.uk/~ac638/pubs/pdf/frpar.pdf
http://www.cl.cam.ac.uk/~ac638/pubs/pdf/linear.pdf
Best wishes,
Amine.
Simon Marlow wrote:
Forwarding on behalf of David von Oheimb <[email protected]>.
> ------------------------------------------------------------------------
>
> Subject: Formal verification of high-level language implementation of
critical software?
> From: David von Oheimb <[email protected]>
> Date: Mon, 09 Feb 2009 11:49:08 +0100
> To: [email protected], [email protected],
[email protected], [email protected]
> CC: Jorge Cuéllar <[email protected]>, Greg Kimberly
<[email protected]>
>
>
> Dear all,
>
> at Siemens Corporate Technology we are currently doing a study with
> Boeing on how to enhance assurance of open-source security-critical
> software components like OpenSSL. Methods considered range from standard
> static analysis tools to formal verification.
>
> One observation is that the higher the programming language used is,
> the less likely programming mistakes are, and the easier a formal model
> can be obtained and the more likely it is to be faithful and verifiable.
> In this sense, implementations e.g. in a functional/logic programming
> language would be ideal.
>
> Are you aware of any (security critical or other) software component
> that has been implemented in such a high-level language and has been
> formally verified? Any quick pointers etc. are appreciated.
>
> Thanks,
> David v.Oheimb
>
> +------------------------------------------------------------------<><-+
> | Dr. David von Oheimb Senior Research Scientist |
> | Siemens AG, CT IC 3 Phone : +49 89 636 41173 |
> | Otto-Hahn-Ring 6 Fax : +49 89 636 48000 |
> | 81730 München Mobile: +49 171 8677 885 |
> | Germany E-Mail: [email protected] |
> | http://scd.siemens.de/db4/lookUp?tcgid=Z000ECRO http://ddvo.net/ |
_______________________________________________
Haskell mailing list
[email protected]
http://www.haskell.org/mailman/listinfo/haskell
_______________________________________________
Haskell mailing list
[email protected]
http://www.haskell.org/mailman/listinfo/haskell
