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

[Simon Marlow]

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/  |