24
12. Duff, T.: On Duff’s device (1988). URL http://www.lysator.liu.se/c/duffs-device.html.
Message to the comp.lang.c Usenet group
13. Filli
ˆ
atre, J.C., March
´
e, C.: Multi-prover verification of C programs. In: 6th Int. Conference on Formal
Engineering Methods, ICFEM 2004, Lecture Notes in Computer Science, vol. 3308, pp. 15–29 (2004)
14. Gimenez, E., Ledinot, E.: Semantics of a subset of the C language (2004). URL http://coq.inria.
fr/contribs/minic.html. Coq contributed library
15. Gr
´
egoire, B., Leroy, X.: A compiled implementation of strong reduction. In: International Conference
on Functional Programming (ICFP 2002), pp. 235–246. ACM Press (2002)
16. Gurevich, Y., Huggins, J.: The semantics of the C programming language. In: Computer Science Logic,
6th Workshop, CSL ’92, Lecture Notes in Computer Science, vol. 702, pp. 274–308. Springer (1993)
17. Hardekopf, B., Lin, C.: The ant and the grasshopper: fast and accurate pointer analysis for millions of
lines of code. SIGPLAN Notices 42(6), 290–299 (2007)
18. Hartel, P.H., Moreau, L.: Formalizing the safety of Java, the Java virtual machine, and Java card. ACM
Computing Surveys 33(4), 517–558 (2001)
19. Hatton, L.: Safer language subsets: an overview and a case history, MISRA C. Information & Software
Technology 46(7), 465–472 (2004)
20. Hoare, T., O’Hearn, P.W.: Separation logic semantics for communicating processes. In: Proceedings of
the First International Conference on Foundations of Informatics, Computing and Software (FICS 2008),
Electronic Notes in Computer Science, vol. 212, pp. 3–25 (2008)
21. Huisman, M., Jacobs, B.: Java program verification via a Hoare logic with abrupt termination. In: Fun-
damental Approaches to Software Engineering, 3rd Int. Conf. FASE 2000, Lecture Notes in Computer
Science, vol. 1783, pp. 284–303. Springer (2000)
22. Hymans, C., Levillain, O.: Newspeak, doubleplussimple minilang for goodthinkful static analysis of C.
Technical note 2008-IW-SE-00010-1, EADS (2008)
23. van Inwegen, M., Gunter, E.L.: HOL-ML. In: Higher Order Logic Theorem Proving and its Applications,
6th International Workshop, HUG ’93, Lecture Notes in Computer Science, vol. 780, pp. 61–74. Springer
(1993)
24. Klein, G., Nipkow, T.: A machine-checked model for a Java-like language, virtual machine, and compiler.
ACM Trans. Program. Lang. Syst. 28(4), 619–695 (2006)
25. Lee, D.K., Crary, K., Harper, R.: Towards a mechanized metatheory of Standard ML. In: 34th Sympo-
sium on Principles of Programming Languages, pp. 173–184. ACM Press (2007)
26. Leinenbach, D., Paul, W., Petrova, E.: Towards the formal verification of a C0 compiler: Code generation
and implementation correctness. In: IEEE Conference on Software Engineering and Formal Methods
(SEFM’05), pp. 2–11. IEEE Computer Society Press (2005)
27. Leroy, X.: Formal certification of a compiler back-end, or: programming a compiler with a proof as-
sistant. In: 33rd ACM symposium on Principles of Programming Languages, pp. 42–54. ACM Press
(2006)
28. Leroy, X.: A formally verified compiler backend (2008). arXiv:0902.2137 [cs]. Submitted
29. Leroy, X., Blazy, S.: Formal verification of a C-like memory model and its uses for verifying program
transformations. Journal on Automated Reasoning 41(1), 1–31 (2008)
30. Leroy, X., Grall, H.: Coinductive big-step operational semantics. Information and Computation 207(2),
284–304 (2009)
31. Milner, R., Tofte, M., Harper, R., MacQueen, D.: The definition of Standard ML (revised). The MIT
Press (1997)
32. Motor Industry Software Reliability Association: MISRA-C. http://www.misra-c.com/ (2004)
33. Necula, G.C., McPeak, S., Rahul, S.P., Weimer, W.: CIL: Intermediate language and tools for analysis
and transformation of C programs. In: Compiler Construction, 11th International Conference, CC 2002,
Lecture Notes in Computer Science, vol. 2304, pp. 213–228. Springer (2002)
34. Nepomniaschy, V.A., Anureev, I.S., Promsky, A.V.: Towards verification of C programs: Axiomatic se-
mantics of the C-kernel language. Programming and Computer Software 29(6), 338–350 (2003)
35. Nipkow, T., Paulson, L.C.: Isabelle/Hol: A Proof Assistant for Higher-Order Logic. Springer (2004)
36. Norrish, M.: C formalised in HOL. Ph.D. thesis, University of Cambridge (1998). Technical report
UCAM-CL-TR-453
37. Norrish, M.: Deterministic expressions in C. In: Programming Languages and Systems, 8th European
Symposium on Programming, ESOP’99, Lecture Notes in Computer Science, vol. 1576, pp. 147–161.
Springer (1999)
38. Owens, S.: A sound semantics for OCamllight. In: Programming Languages and Systems, 17th European
Symposium on Programming, ESOP 2008, Lecture Notes in Computer Science, vol. 4960, pp. 1–15.
Springer (2008)
39. Papaspyrou, N.: A formal semantics for the C programming language. Ph.D. thesis, National Technical
University of Athens (1998)