Re: [isabelle] Program verification and Isabelle?

Hello Klaus Ostermann,

as part of the Verisoft project ( 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:


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