(en) Daniel Kästner, Jörg Barrho, Ulrich Wünsche et Marc Schlickling, «CompCert: Practical Experience on Integrating and Qualifying a Formally Verified Optimizing Compiler», INRIA, , p.1 (lire en ligne, consulté le )
Par exemple sur l'EDSAC, comme le décrit Alan Turing dans sa conférence, lors de l'inauguration, (en) A. M. Turing, «Checking a Large Routine», dans Report of a Conference on High Speed Automatic Calculating Machines, Univ. Math. Lab., Cambridge, p.67-69 (1949) in Morris, F. L. et C. B. Jones, «An Early Program Proof by Alan Turing», Ann. Hist. Comp., vol.6, no2, , p.139-143 (lire en ligne).