Re: [isabelle] proof engineering for program verification
The publications from this project may be of interest:
On 17 June 2015 at 18:11, Buday Gergely <gbuday at karolyrobert.hu> wrote:
> 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
> 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
> - Gergely
This archive was generated by a fusion of
Pipermail (Mailman edition) and