[isabelle] proof engineering for program verification



Hi,

I know that Isabelle is not a program verification environment per se but some people use it to build one. And they do read this list.

I am looking for literature on the challenges of building a practical program verification system.

There is the problem of defining the semantics of the language, there are tools for this: Ott and Lem are clear examples.

Beckert and Klebanov write about proof reuse:

Proof Reuse for Deductive Program Verification
http://i12www.ira.uka.de/~beckert/pub/sefm04.pdf

Alglave et al. write about the socio-economic aspects of verification tools:

Making Software Verification Tools Really Work
http://www0.cs.ucl.ac.uk/staff/J.Alglave/papers/atva11.pdf

Shao writes about certified software:

Certified Software
http://flint.cs.yale.edu/flint/publications/certsoft.pdf

"Developing large-scale mechanized proofs and human-readable
formal specifications will become an exciting research field on its
own, with many open issues."

I would like to read about these technical issues. What papers would you recommend?

- Gergely



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