[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:
"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?
This archive was generated by a fusion of
Pipermail (Mailman edition) and