Re: [isabelle] Program verification and Isabelle?



Hello Klaus Ostermann,

as part of the Verisoft project (www.verisoft.de) I have developed a 
verification environment for sequential imperative programs over the last few 
years. It's a combination of a deep and shallow embedding and provides a 
quite general core language that is suitable to express most common language 
constructs of imperative programming languages. Allthough the focus in 
Verisoft is on a subset of C, I believe it can also be customized to express 
the object-oriented  features of languages like Java or C#. I look forward to 
someone heading in this direction. So if you are interested have a look at: 

http://www4.in.tum.de/~schirmer/verification_environment.html

   Norbert
 





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.