[isabelle] proof engineering for program verification


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

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

Making Software Verification Tools Really Work

Shao writes about certified software:

Certified Software

"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.