In this vein of discussion, is there (and if not, should we try and make
one) a basic [guide] to the current capabilities and limitations of
formal verification/proofs of correctness?
Perhaps a good place to start would a bibliography. The nature of what
constitutes a proof of a computer code and the methods for constructing such
a proof have not changed since the dawn of software so "current capabilities
and limitations" must mean all capabilities and limitations discovered to
date. (Formal methods for software seem to be a tabula-rasa-causing fever
that comes around about every 17 years like cicadas.)
The bibliography from Huang's 2008 book
(http://onlinelibrary.wiley.com/doi/10.1002/9780470464076.biblio/pdf) is a
possible starting point as is the bibliography from Jean-Christophe
Filliatre's 2011 habilitation thesis
(https://www.lri.fr/~filliatr/biblio-these.html).
Ralph London's article "Computer Programs can be Proved Correct" in LNORMS,
v. 28 (1970) (http://link.springer.com/chapter/10.1007/978-3-642-99976-5_11)
is a timeless and valuable introduction to the topic that includes an
extensive bibliography up to that point in time. One might also consult
London's paper "The Current State of Proving Programs Correct" in ACM '72
(http://dl.acm.org/citation.cfm?doid=800193.805820) for this purpose.
London's bibliography can be found in the following places:
http://aitopics.org/sites/default/files/classic/Machine%20Intelligence%205/MI5-Appendix-London.pdf,
ftp://ftp.cs.wisc.edu/pub/techreports/1969/TR64.pdf, and
ftp://ftp.cs.wisc.edu/pub/techreports/1970/TR104.pdf.
Cheers, Scott
P.S. London's note in the January, 2013, CACM, Who Earned First Computer
Science PhD.?
(http://cacm.acm.org/blogs/blog-cacm/159591-who-earned-first-computer-science-phd/fulltext
with additional information here
http://www.clarke.edu/media/files/Academics/Departments/Computer_Science/First%20PhD%20Additional%20Info.pdf)
is an irrelevant yet informative read.
_______________________________________________
langsec-discuss mailing list
langsec-discuss@mail.langsec.org
https://mail.langsec.org/cgi-bin/mailman/listinfo/langsec-discuss
