Formal Verification of a C-like Memory Model and Its Uses for Verifying Program Transformations

1. Appel, A.W., Blazy, S.: Separation logic for small-step Cminor. In: Theorem Proving in Higher Order Logics, 20th Int. Conf. TPHOLs 2007, Lecture Notes in Computer Science, vol. 4732, pp. 5–21. Springer, New York (2007)

   Chapter  Google Scholar 

2. Bertot, Y., Castéran, P.: Interactive Theorem Proving and Program Development – Coq’Art: The Calculus of Inductive Constructions. EATCS Texts in Theoretical Computer Science. Springer, New York (2004)

   Google Scholar 

3. Blazy, S., Dargaye, Z., Leroy, X.: Formal verification of a C compiler front-end. In: FM 2006: Int. Symp. on Formal Methods, Lecture Notes in Computer Science, vol. 4085, pp. 460–475. Springer, New York (2006)

   Google Scholar 

4. Bornat, R.: Proving pointer programs in Hoare logic. In: MPC ’00: Proc. Int. Conf. on Mathematics of Program Construction, Lecture Notes in Computer Science, vol. 1837, pp. 102–126. Springer, New York (2000)

   Google Scholar 

5. Burstall, R.: Some techniques for proving correctness of programs which alter data structures. Mach. Intell. 7, 23–50 (1972)

   Google Scholar 

6. Chrząszcz, J.: Modules in type theory with generative definitions. Ph.D. thesis, Warsaw University and University of Paris-Sud (2004)

7. Conchon, S., Contejean, E., Kanig, J.: The Ergo automatic theorem prover. Software and documentation available at http://ergo.lri.fr/ (2005–2008)

8. Coq development team: The Coq proof assistant. Software and documentation available at http://coq.inria.fr/ (1989–2008)

9. De Moura, L., Bjørner, N., et al.: Z3: an efficient SMT solver. Software and documentation available at http://research.microsoft.com/projects/z3 (2006–2008)

10. Detlefs, D., Nelson, G., Saxe, J.B.: Simplify: a theorem prover for program checking. J. ACM 52(3), 365–473 (2005)

    Article  MathSciNet  Google Scholar 

11. Filliâtre, J.C., Marché, C.: Multi-prover verification of C programs. In: 6th Int. Conf. on Formal Engineering Methods, ICFEM 2004, Lecture Notes in Computer Science, vol. 3308, pp. 15–29. Springer, New York (2004)

    Google Scholar 

12. Filliâtre, J.C., Marché, C., Moy, Y., Hubert, T.: The Why software verification platform. Software and documentation available at Software and documentation available at http://why.lri.fr/ (2004–2008)

13. ISO: International Standard ISO/IEC 9899:1999, Programming languages – C. ISO, Geneva (1999)

14. Jia, L., Walker, D.: ILC: a foundation for automated reasoning about pointer programs. In: Programming Languages and Systems, 15th European Symposium on Programming, ESOP 2006, Lecture Notes in Computer Science, vol. 3924, pp. 131–145. Springer, New York (2006)

    Google Scholar 

15. Leroy, X.: Formal certification of a compiler back-end, or: programming a compiler with a proof assistant. In: 33rd Symposium Principles of Programming Languages, pp. 42–54. ACM, New York (2006)

    Google Scholar 

16. Manson, J., Pugh, W., Adve, S.V.: The Java memory model. In: 32nd Symposium Principles of Programming Languages, pp. 378–391. ACM, New York (2005)

    Google Scholar 

17. Marti, N., Affeldt, R., Yonezawa, A.: Formal verification of the heap manager of an operating system using separation logic. In: Formal Methods and Software Engineering, 8th Int. Conf. ICFEM 2006, Lecture Notes in Computer Science, vol. 4260, pp. 400–419. Springer, New York (2006)

    Google Scholar 

18. McCreight, A., Shao, Z., Lin, C., Li, L.: A general framework for certifying garbage collectors and their mutators. In: Programming Language Design and Implementation 2007, pp. 468–479. ACM, New York (2007)

    Chapter  Google Scholar 

19. Mehta, F., Nipkow, T.: Proving pointer programs in higher-order logic. Inf. Comput. 199(1–2), 200–227 (2005)

    Article  MATH  MathSciNet  Google Scholar 

20. Nita, M., Grossman, D., Chambers, C.: A theory of platform-dependent low-level software. In: 35th Symposium Principles of Programming Languages. ACM, New York (2008)

    Google Scholar 

21. Norrish, M.: C formalized in HOL. Technical report UCAM-CL-TR-453. Ph.D. thesis, University of Cambridge (1998)

22. O’Hearn, P.W., Reynolds, J.C., Yang, H.: Local reasoning about programs that alter data structures. In: Computer Science Logic, 15th Int. Workshop, CSL 2001, Lecture Notes in Computer Science, vol. 2142, pp. 1–19. Springer, New York (2001)

    Google Scholar 

23. Reynolds, J.C.: Intuitionistic reasoning about shared data structures. In: Davies, J., Roscoe, B., Woodcock, J. (eds.) Millenial Perspectives in Computer Science, pp. 303–321. Palgrave, Hampshire (2000)

    Google Scholar 

24. Reynolds, J.C.: Separation logic: a logic for shared mutable data structures. In: 17th Symposium on Logic in Computer Science (LICS 2002), pp. 55–74. IEEE Computer Society, Los Alamitos (2002)

    Chapter  Google Scholar 

25. Shen, X., Arvind, R.L.: Commit-reconcile & fences (CRF): a new memory model for architects and compiler writers. In: ISCA ’99: Proc. Int. Symp. on Computer Architecture, pp. 150–161. IEEE Computer Society, Los Alamitos (1999)

    Google Scholar 

26. Tennent, R.D., Ghica, D.R.: Abstract models of storage. Higher-Order and Symbolic Computation 13(1–2), 119–129 (2000)

    Article  MATH  Google Scholar 

27. Tuch, H., Klein, G., Norrish, M.: Types, bytes, and separation logic. In: 34th Symposium Principles of Programming Languages, pp. 97–108. ACM, New York (2007)

    Chapter  Google Scholar 

28. Yang, Y., Gopalakrishnan, G., Lindstrom, G.: UMM: an operational memory model specification framework with integrated model checking capability. Concurr. Comput.: Practice and Experience 17(5–6), 465–487 (2005)

    Article  Google Scholar 

Download references