[Haskell] Fwd: Formal verification of high-level language implementation of critical software?

[Amine Chaieb]

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 <David.von.Oheimb at siemens.com>.
> 
>  > ------------------------------------------------------------------------
>  >
>  > Subject: Formal verification of high-level language implementation of 
> critical software?
>  > From: David von Oheimb <David.von.Oheimb at siemens.com>
>  > Date: Mon, 09 Feb 2009 11:49:08 +0100
>  > To: members at fmeurope.org, formal-methods at cs.uidaho.edu, 
> fmacademic at cas.mcmaster.ca, haskell at haskell.org
>  > CC: Jorge Cuéllar <Jorge.Cuellar at siemens.com>, Greg Kimberly 
> <Greg.Kimberly at boeing.com>
>  >
>  >
>  > 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: David.von.Oheimb at siemens.com  |
>  > |  http://scd.siemens.de/db4/lookUp?tcgid=Z000ECRO   http://ddvo.net/  |
> _______________________________________________
> Haskell mailing list
> Haskell at haskell.org
> http://www.haskell.org/mailman/listinfo/haskell