[langsec-discuss] Bibliography for Proving Code

Scott Guthery sbg at acw.com
Wed Jul 9 15:16:46 UTC 2014

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

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: 
ftp://ftp.cs.wisc.edu/pub/techreports/1969/TR64.pdf, and 

Cheers, Scott

P.S. London's note in the January, 2013, CACM, Who Earned First Computer 
Science PhD.? 
with additional information here 
is an irrelevant yet informative read. 

More information about the langsec-discuss mailing list