Re: [isabelle] proof engineering for program verification



The publications from this project may be of interest:
http://ssrg.nicta.com.au/projects/TS/pme.pml

On 17 June 2015 at 18:11, Buday Gergely <gbuday at karolyrobert.hu> wrote:

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