Email Gateway (Aug 22 2022 at 10:13): Email Gateway (Aug 22 2022 at 10:13):From: Buday Gergely <gbuday@karolyrobert.hu>
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?
Email Gateway (Aug 22 2022 at 10:14):From: Ramana Kumar <rk436@cam.ac.uk>
The publications from this project may be of interest:
http://ssrg.nicta.com.au/projects/TS/pme.pml
Last updated: Apr 18 2024 at 20:16 UTC