ACM Software System Calendar 2024開催
https://qiita.com/advent-calendar/2024/acm
Day 6 投稿記事です。

投稿予定の方は、購読ボタンを押してください。よろしくお願いします。
記事をお読みになられたら、Calendarにあってもいいかなって記事には、いいね💚　をお願いします。

CompCert

COMPCERT
https://compcert.org/compcert-C.html

Formal verification of a realistic compiler,

Xavier Leroy
https://xavierleroy.org/publi/compcert-CACM.pdf

AbsInt / CompCert
https://github.com/AbsInt/CompCert

7. References

[1] A. W. Appel. Foundational proof-carrying code. In Logic in Computer Science 2001, pages 247–258. IEEE, 2001.
[2] A. W. Appel and S. Blazy. Separation logic for small-step Cminor. In Theorem Proving in Higher Order Logics, TPHOLs 2007, volume 4732 of LNCS, pages 5–21. Springer, 2007.
[3] Y. Bertot and P. Cast ́eran. Interactive Theorem Proving and Program Development – Coq’Art: The Calculus of Inductive Constructions. Springer, 2004.
[4] S. Blazy, Z. Dargaye, and X. Leroy. Formal verification of a C compiler front-end. In FM 2006: Int. Symp. on Formal Methods, volume 4085 of LNCS, pages 460–475. Springer, 2006.
[5] S. Blazy and X. Leroy. Mechanized semantics for the Clight subset of the C language. J. Autom. Reasoning, 2009. Accepted for publication, to appear.
[6] G. J. Chaitin. Register allocation and spilling via graph coloring. In 1982 SIGPLAN Symposium on Compiler Construction, pages 98–105. ACM Press, 1982.
[7] Coq development team. The Coq proof assistant. Available at http://coq.inria.fr/, 1989–2009.
[8] M. A. Dave. Compiler verification: a bibliography. SIGSOFT Softw. Eng. Notes, 28(6):2–2, 2003.
[9] L. George and A. W. Appel. Iterated register coalescing. ACM Trans. Prog. Lang. Syst., 18(3):300–324, 1996.
[10] T. C. Hales. Formal proof. Notices of the AMS, 55(11):1370–1380, 2008.
[11] X. Leroy. Formal certification of a compiler back-end, or: programming a compiler with a proof assistant. In 33rd symp. Principles of Progr. Lang., pages 42–54. ACM Press, 2006.
[12] X. Leroy. The CompCert verified compiler, software and commented proof. Available at http://compcert.inria.fr/, Aug. 2008.
[13] X. Leroy. A formally verified compiler back-end. arXiv:0902.2137 [cs]. Submitted, July 2008.
[14] X. Leroy and S. Blazy. Formal verification of a C-like memory model and its uses for verifying program transformations. J. Autom. Reasoning, 41(1):1–31, 2008.
[15] P. Letouzey. Extraction in Coq: An overview. In Logic and Theory of Algorithms, Computability in Europe, CiE 2008, volume 5028 of LNCS, pages 359–369. Springer, 2008.
[16] J. McCarthy and J. Painter. Correctness of a compiler for arithmetical expressions. In Mathematical Aspects of Computer Science, volume 19 of Proc. of Symposia in Applied Mathematics, pages 33–41. AMS, 1967.
[17] R. Milner and R. Weyhrauch. Proving compiler correctness in a mechanized logic. In Proc. 7th Annual Machine Intelligence Workshop, volume 7 of Machine Intelligence, pages 51–72. Edinburgh University Press, 1972.
[18] G. Morrisett, D. Walker, K. Crary, and N. Glew. From System F to typed assembly language. ACM Trans. Prog. Lang. Syst., 21(3):528–569, 1999.
[19] G. C. Necula. Proof-carrying code. In 24th symp. Principles of Progr. Lang., pages 106–119. ACM Press, 1997.
[20] G. C. Necula. Translation validation for an optimizing compiler. In Prog. Lang. Design and Impl. 2000, pages 83–95. ACM Press, 2000.
[21] G. C. Necula, S. McPeak, S. P. Rahul, and W. Weimer. CIL: Intermediate language and tools for analysis and transformation of C programs. In Compiler Construction, volume 2304 of LNCS, pages 213–228. Springer, 2002.
[22] A. Pnueli, M. Siegel, and E. Singerman. Translation validation. In Tools and Algorithms for Construction and Analysis of Systems, TACAS ’98, volume 1384 of LNCS, pages 151–166. Springer, 1998.
[23] J.-B. Tristan and X. Leroy. Formal verification of translation validators: A case study on instruction scheduling optimizations. In 35th symp. Principles of Progr. Lang., pages 17–27. ACM Press, 2008.
[24] J.-B. Tristan and X. Leroy. Verified validation of lazy code motion. In Prog. Lang. Design and Impl. 2009. ACM Press, 2009. To appear.

arXiv

Formally Verified Native Code Generation in an Effectful JIT -- or: Turning the CompCert Backend into a Formally Verified JIT Compiler

Aurèle Barrière, Sandrine Blazy, David Pichardie
https://arxiv.org/pdf/2212.03129

This work presents a model JIT with dynamic generation of native code, implemented and formally verified in Coq. Although some parts of a JIT cannot be written in Coq, we propose a proof methodology to delimit, specify and reason on the impure effects of a JIT.

2013年受賞のCOQがRてくるとは。

REFERENCES

Andrew W. Appel. 2015. Verification of a Cryptographic Primitive: SHA-256. ACM Trans. Program. Lang. Syst. 37, 2 (2015), 7:1–7:31. https://doi.org/10.1145/2701415
Aurèle Barrière, Sandrine Blazy, Olivier Flückiger, David Pichardie, and Jan Vitek. 2021. Formally verified speculation and deoptimizationinaJITcompiler.Proc.ACMProgram.Lang.POPL(2021). https://doi.org/10.1145/3434327
Gilles Barthe, Delphine Demange, and David Pichardie. 2014. Formal Verification of an SSA-Based Middle-End for CompCert. ACMTrans.Program.Lang.Syst.36,1(2014),4:1–4:35. https://doi.org/10.1145/2579080
Fraser Brown, John Renner, Andres Nötzli, Sorin Lerner, Hovav Shacham, and Deian Stefan. 2020. Towards a verified range analysis for JavaScript JITs. In Proceedings of the 41st ACM SIGPLAN International Conference on Programming Language DesignandImplementation,PLDI2020.ACM,135–150. https://doi.org/10.1145/3385412.3385968
David Cock, Gerwin Klein, and Thomas Sewell. 2008. Secure Microkernels, State Monads and Scalable Refinement. In Proc. ofTPHOLs2008,Vol.5170.Springer,167–182. https://doi.org/10.1007/978-3-540-71067-7_16
Olivier Flückiger, Gabriel Scherer, Ming-Ho Yee, Aviral Goel, Amal Ahmed, and Jan Vitek. 2018. Correctness of speculative optimizationswithdynamicdeoptimization.POPL(2018). https://doi.org/10.1145/3158137
HotSpot 2022. Java HotSpot Performance Engine. HotSpot. https://openjdk.org/groups/hotspot/
Inria 2022. The Coq proof assistant reference manual. Inria. http://coq.inria.fr Version 8.12.1.
Jeehoon Kang, Yoonseung Kim, Youngju Song, Juneyoung Lee, Sanghoon Park, Mark Dongyeon Shin, Yonghyun Kim,
Sungkeun Cho, Joonwon Choi, Chung-Kil Hur, and Kwangkeun Yi. 2018. Crellvm: verified credible compilation for LLVM. In Proceedings of the 39th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2018.ACM,631–645. https://doi.org/10.1145/3192366.3192377
Daniel Kästner, Jörg Barrho, Ulrich Wünsche, Marc Schlickling, Bernhard Schommer, Michael Schmidt, Christian Ferdinand, Xavier Leroy, and Sandrine Blazy. 2018. CompCert: Practical Experience on Integrating and Qualifying a Formally Verified Optimizing Compiler. In ERTS2 2018 - 9th European Congress Embedded Real-Time Software and Systems. 3AF, SEE, SIE, 1–9. https://hal.inria.fr/hal-01643290
Ramana Kumar, Magnus O. Myreen, Michael Norrish, and Scott Owens. 2014. CakeML: a verified implementation of ML. In ProceedingsofPOPL. https://doi.org/10.1145/2535838.2535841
Peter Lammich and S. Reza Sefidgar. 2019. Formalizing Network Flow Algorithms: A Refinement Approach in Isabelle/HOL.
J. Autom. Reason. 62, 2 (2019), 261–280. https://doi.org/10.1007/s10817-017-9442-4
Xavier Leroy. 2006. Formal certification of a compiler back-end or: programming a compiler with a proof assistant. In ProceedingsofPOPL. https://doi.org/10.1145/1111037.1111042
Xavier Leroy. 2009a. Formal verification of a realistic compiler. Commun. ACM (2009). https://doi.org/10.1145/1538788.1538814
Xavier Leroy. 2009b. A formally verified compiler back-end. Journal of Automated Reasoning 43, 4 (2009), 363–446. https://doi.org/10.1007/s10817- 009- 9155- 4
Xavier Leroy, Sandrine Blazy, Daniel Kästner, Bernhard Schommer, Markus Pister, and Christian Ferdinand. 2016. CompCert - A Formally Verified Optimizing Compiler. In ERTS 2016: Embedded Real Time Software and Systems, 8th European Congress. SEE. https://hal.inria.fr/hal-01238879
Thomas Letan and Yann Régis-Gianas. 2020. FreeSpec: specifying, verifying, and executing impure computations in
Coq. In Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP. https://doi.org/10.1145/3372885.3373812
Andreas Lööw, Ramana Kumar, Yong Kiam Tan, Magnus O. Myreen, Michael Norrish, Oskar Abrahamsson, and Anthony C. J. Fox. 2019. Verified compilation on a verified processor. In Proceedings of the 40th ACM SIGPLAN Conference on ProgrammingLanguageDesignandImplementation,PLDI2019.ACM,1041–1053. https://doi.org/10.1145/3314221.3314622
Magnus O. Myreen. 2010. Verified just-in-time compiler on x86. In Proceedings of the 37th ACM SIGPLAN-SIGACT Symposium onPrinciplesofProgrammingLanguages,POPL2010.ACM,107–118. https://doi.org/10.1145/1706299.1706313
Scott Owens, Michael Norrish, Ramana Kumar, Magnus O. Myreen, and Yong Kiam Tan. 2017. Verifying efficient function callsinCakeML.PACMPL1,ICFP(2017),18:1–18:27. https://doi.org/10.1145/3110262
Clément Pit-Claudel, Peng Wang, Benjamin Delaware, Jason Gross, and Adam Chlipala. 2020. Extensible Extraction of Efficient Imperative Programs with Foreign Functions, Manually Managed Memory, and Proofs. In Proc. of IJCAR 2020, Vol.12167.Springer,119–137. https://doi.org/10.1007/978-3-030-51054-1_7
PyPy 2022. PyPy Python Implementation. PyPy. https://www.pypy.org/
Kazuhiko Sakaguchi. 2018. Program Extraction for Mutable Arrays. In Functional and Logic Programming - 14th International
Symposium,FLOPS2018,Vol.10818.Springer,51–67. https://doi.org/10.1007/978-3-319-90686-7_4
Youngju Song, Minki Cho, Dongjoo Kim, Yonghyun Kim, Jeehoon Kang, and Chung-Kil Hur. 2020. CompCertM: CompCert with C-assembly linking and lightweight modular verification. Proc. ACM Program. Lang. 4, POPL (2020), 23:1–23:31. https://doi.org/10.1145/3371091
Gordon Stewart, Lennart Beringer, Santiago Cuellar, and Andrew W. Appel. 2015. Compositional CompCert. In Proc. ACM Program.Lang.POPL2015.ACM,275–287. https://doi.org/10.1145/2676726.2676985
WouterSwierstra.2008.Datatypesàlacarte.J.Funct.Program.(2008). https://doi.org/10.1017/S0956796808006758
Yong Kiam Tan, Magnus O. Myreen, Ramana Kumar, Anthony C. J. Fox, Scott Owens, and Michael Norrish. 2016. A new verified compiler backend for CakeML. In Proceedings of the 21st ACM SIGPLAN International Conference on Functional Programming,ICFP2016.ACM,60–73. https://doi.org/10.1145/2951913.2951924
V8 2022. V8 Javascript Engine. V8. https://v8.dev/
Yuting Wang, Pierre Wilke, and Zhong Shao. 2019. An abstract stack based approach to verified compositional compilation
tomachinecode.Proc.ACMProgram.Lang.3,POPL(2019),62:1–62:30. https://doi.org/10.1145/3290375
Conrad Watt, Xiaojia Rao, Jean Pichon-Pharabod, Martin Bodin, and Philippa Gardner. 2021. Two Mechanisations of WebAssembly 1.0. In Formal Methods - 24th International Symposium, FM 2021, Vol. 13047. Springer, 61–79. https://doi.org/10.1007/978-3-030-90870-6_4
Li-yao Xia, Yannick Zakowski, Paul He, Chung-Kil Hur, Gregory Malecha, Benjamin C. Pierce, and Steve Zdancewic. 2020. Interaction trees: representing recursive and impure programs in Coq. Proc. ACM Program. Lang. POPL (2020). https://doi.org/10.1145/3371119
Yannick Zakowski, Calvin Beck, Irene Yoon, Ilia Zaichuk, Vadim Zaliva, and Steve Zdancewic. 2021. Modular, compositional, andexecutableformalsemanticsforLLVMIR.ICFP(2021). https://doi.org/10.1145/3473572
Jianzhou Zhao, Santosh Nagarakatte, Milo M. K. Martin, and Steve Zdancewic. 2012. Formalizing the LLVM intermediate representation for verified program transformations. In Proceedings of the Symposium on Principles of Programming Languages,POPL. https://doi.org/10.1145/2103656.2103709
Jianzhou Zhao, Santosh Nagarakatte, Milo M. K. Martin, and Steve Zdancewic. 2013. Formal verification of SSA-based optimizations for LLVM. In ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2013. ACM. https://doi.org/10.1145/2491956.2462164

The Trusted Computing Base of the CompCert Verified Compiler

Authors: David Monniaux, Sylvain Boulmé
https://arxiv.org/pdf/2201.10280

References

[1] Alasdair Armstrong et al. “ISA Semantics for ARMv8-a, RISC-V, and CHERI-MIPS”. In: Proc. ACM Program. Lang. 3.POPL (2019). doi: 10.1145/3290384. url: https://doi.org/10.1145/3290384.
[2] Gilles Barthe, Delphine Demange, and David Pichardie. “A Formally Veri- fied SSA-Based Middle-End - Static Single Assignment Meets CompCert”. In: Programming Languages and Systems (ESOP). Ed. by Helmut Seidl. Vol. 7211. Lecture Notes in Computer Science. Springer, 2012, pp. 47–66. doi: 10.1007/978-3-642-28869-2_3.
[3] Fr ́ed ́eric Besson, Sandrine Blazy, and Pierre Wilke. “CompCertS: a Memory- Aware Verified C Compiler Using a Pointer as Integer Semantics”. In: J. Autom. Reason. 63.2 (2019), pp. 369–392. doi: 10.1007/s10817-018-9496-y.
[4] Bruno Blanchet et al. “A Static Analyzer for Large Safety-Critical Software”. In: ACM SIGPLAN Conference on Programming language design and implementation (PLDI). ACM. 2003, pp. 196–207. doi: 10.1145/781131.781153. arXiv: cs/0701193.
[5] Sandrine Blazy. “Experiments in validating formal semantics for C”. In: C/C++ Verification Workshop. Oxford, United Kingdom, 2007, pp. 95– 102. url: https://hal.inria.fr/inria-00292043.
[6] Mathieu Boespflug, Maxime D ́enes, and Benjamin Gr ́egoire. “Full Reduc- tion at Full Throttle”. In: Certified Programs and Proofs - First Inter- national Conference, CPP 2011, Kenting, Taiwan, December 7-9, 2011. Proceedings. Ed. by Jean-Pierre Jouannaud and Zhong Shao. Vol. 7086. Lecture Notes in Computer Science. Springer, 2011, pp. 362–377. doi: 10.1007/978-3-642-25379-9\_26. [7] Sylvain Boulm ́e. “Formally Verified Defensive Programming (efficient Coq- verified computations from untrusted ML oracles)”. See also http://www- verimag.imag.fr/~boulme/hdr.html. Habilitation a diriger des recherches. Universit ́e Grenoble-Alpes, Sept. 2021. url: https://hal.archives-ouvertes. fr/tel-03356701.
24
[8] Sylvain Boulm ́e et al. “The Verified Polyhedron Library: an Overview”. In: 20th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing, SYNASC 2018, Timisoara, Romania, September 20-23, 2018. IEEE Computer Society, 2018, pp. 9–17. doi: 10.1109/SYNASC.2018.00014. url: https://hal.archives-ouvertes.fr/hal-02100006.
[9] Timothy Bourke et al. “A formally verified compiler for Lustre”. In: PLDI 2017: Programming Language Design and Implementation. ACM Press, 2017, pp. 586–601. url: http://xavierleroy.org/publi/velus-pldi17. pdf.
[10] Thomas Braibant, Jacques-Henri Jourdan, and David Monniaux. “Imple- menting and Reasoning About Hash-consed Data Structures in Coq”. In: Journal of Automated Reasoning (June 2014), pp. 1–34. issn: 0168-7433. doi: 10.1007/s10817-014-9306-0. HAL: hal-00816672. url: https:// hal.archives-ouvertes.fr/hal-00816672.
[11] Laurent Chicli, Loic Pottier, and Carlos Simpson. “Mathematical Quo- tients and Quotient Types in Coq”. In: Types for Proofs and Programs, Second International Workshop, TYPES 2002, Berg en Dal, The Nether- lands, April 24-28, 2002, Selected Papers. Ed. by Herman Geuvers and Freek Wiedijk. Vol. 2646. Lecture Notes in Computer Science. Springer, 2002, pp. 95–107. doi: 10.1007/3-540-39185-1_6.
[12] Laurent Igal Chicli. “Sur la formalisation des math ́ematiques dans le Calcul des Constructions Inductives”. PhD thesis. Universit ́e de Nice, 2003. url: http://www-sop.inria.fr/lemme/Laurent.Chicli/these_ chicli.ps.
[13] Sylvain Conchon and Jean-Christophe Filliaˆtre. “A persistent union-find data structure”. In: Proceedings of the ACM Workshop on ML, 2007, Freiburg, Germany, October 5, 2007. Ed. by Claudio V. Russo and Derek Dreyer. ACM, 2007, pp. 37–46. doi: 10.1145/1292535.1292541.
[14] Delphine Demange. “Semantic foundations of intermediate program rep- resentations. (Fondements s ́emantiques des repr ́esentations interm ́ediaires de programmes)”. PhD thesis. E ́ cole normale sup ́erieure de Cachan, France, 2012. url: https://tel.archives-ouvertes.fr/tel-00905442.
[15] Jean-Christophe Filliaˆtre and Sylvain Conchon. “Type-safe modular hash- consing”. In: Proceedings of the ACM Workshop on ML, 2006, Portland, Oregon, USA, September 16, 2006. Ed. by Andrew Kennedy and Franc ̧ois Pottier. ACM, 2006, pp. 12–19. doi: 10.1145/1159876.1159880.
[16] Anthony C. J. Fox et al. “Verified compilation of CakeML to multiple machine-code targets”. In: Proceedings of the 6th ACM SIGPLAN Con- ference on Certified Programs and Proofs, CPP 2017, Paris, France, Jan- uary 16-17, 2017. Ed. by Yves Bertot and Viktor Vafeiadis. ACM, 2017, pp. 125–137. doi: 10.1145/3018610.3018621. url: https://doi.org/ 10.1145/3018610.3018621.
[17] Jean Goubault. “HimML: Standard ML with Fast Sets and Maps”. In: In 5th ACM SIGPLAN Workshop on ML and its Applications. Also IN- RIA RR-2265. ACM Press, 1994. url: http://citeseerx.ist.psu.edu/ viewdoc/download?doi=10.1.1.40.4967&rep=rep1&type=pdf.
[18] Jean Goubault. Implementing Functional Languages with Fast Equality, Sets and Maps: an Exercise in Hash Consing. Tech. rep. May 1994 version also available. Bull S.A. Corporate Research Center, 1992. url: http:// citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.41.1757&rep=rep1& type=pdf.
[19] Jean Goubault-Larrecq. The GimML reference manual. version 1.0. July 2021. url: http://www.lsv.fr/~goubault/GimML/refman.pdf.
[20] BenjaminGr ́egoireandXavierLeroy.“Acompiledimplementationof strong reduction”. In: Proceedings of the Seventh ACM SIGPLAN Inter- national Conference on Functional Programming (ICFP ’02), Pittsburgh, Pennsylvania, USA, October 4-6, 2002. Ed. by Mitchell Wand and Simon L. Peyton Jones. ACM, 2002, pp. 235–246. doi: 10.1145/581478.581501.
[21] International standard—Programming languages—C. Tech. rep. ISO/IEC, 9899:1999.
[22] International standard—Programming languages—C. Tech. rep. ISO/IEC, 9899:2011.
[23] Jacques-HenriJourdan,Franc ̧oisPottier,andXavierLeroy.“Validating LR(1) Parsers”. In: Programming Languages and Systems – 21st European Symposium on Programming, ESOP 2012. Vol. 7211. Lecture Notes in Computer Science. Springer, 2012, pp. 397–416. url: http://xavierleroy. org/publi/validated-parser.pdf.
[24] Jeehoon Kang et al. “Lightweight Verification of Separate Compilation”. In: SIGPLAN Not. 51.1 (Jan. 2016), 178–190. issn: 0362-1340. doi: 10.1145/2914770.2837642.
[25] Daniel K ̈astner et al. “Closing the gap – The formally verified optimizing compiler CompCert”. In: SSS’17: Developments in System Safety Engi- neering: Proceedings of the Twenty-fifth Safety-critical Systems Sympo- sium. CreateSpace, 2017, pp. 163–180.
[26] Stephen Kell, Dominic P. Mulligan, and Peter Sewell. “The missing link: explaining ELF static linking, semantically”. In: Proceedings of the 2016 ACM SIGPLAN International Conference on Object-Oriented Program- ming, Systems, Languages, and Applications, OOPSLA 2016, part of SPLASH 2016, Amsterdam, The Netherlands, October 30 - November 4, 2016. Ed.
by Eelco Visser and Yannis Smaragdakis. ACM, 2016, pp. 607–623. doi: 10.1145/2983990.2983996.
[27] Robbert Krebbers. “A Formal C Memory Model for Separation Logic”. In: J. Autom. Reason. 57.4 (2016), pp. 319–387. doi: 10.1007/s10817-016-9369-1.
[28] Robbert Krebbers, Xavier Leroy, and Freek Wiedijk. “Formal C semantics: CompCert and the C standard”. In: ITP 2014: Interactive Theorem Proving. LNCS 8558. Springer, 2014, pp. 543–548. doi: 10.1007/978-3-319-08970-6_36.
[29] Ramana Kumar et al. “Software Verification with ITPs Should Use Binary Code Extraction to Reduce the TCB - (Short Paper)”. In: Interactive Theorem Proving (ITP). Ed. by Jeremy Avigad and Assia Mahboubi. Vol. 10895. Lecture Notes in Computer Science. Springer, 2018, pp. 362– 369. doi: 10.1007/978-3-319-94821-8_21.
[30] Gyesik Lee and Benjamin Werner. “Proof-irrelevant model of CC with predicative induction and judgmental equality”. In: Log. Methods Com- put. Sci. 7.4 (2011). doi: 10.2168/LMCS-7(4:5)2011. url: https://doi. org/10.2168/LMCS-7(4:5)2011.
[31] Juneyoung Lee et al. “Taming undefined behavior in LLVM”. In: Proceed- ings of the 38th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2017, Barcelona, Spain, June 18-23, 2017. Ed. by Albert Cohen and Martin T. Vechev. ACM, 2017, pp. 633– 647. doi: 10.1145/3062341.3062343.
[32] Xavier Leroy. “A formally verified compiler back-end”. In: Journal of Au- tomated Reasoning 43.4 (2009), pp. 363–446. url: http://xavierleroy. org/publi/compcert-backend.pdf.
[33] Xavier Leroy. “Formal verification of a realistic compiler”. In: Communi- cations of the ACM 52.7 (2009). doi: 10.1145/1538788.1538814. HAL: inria-00415861.
[34] Xavier Leroy. The CompCert C verified compiler. 3.9. an up-to-date ver- sion is at https://compcert.org/man/. May 2021.
[35] Xavier Leroy et al. “CompCert – A formally verified optimizing compiler”. In: ERTS 2016: Embedded Real Time Software and Systems. SEE, 2016.
[36] Pierre Letouzey. “Extraction in Coq: An Overview”. In: Logic and Theory of Algorithms, Fourth Conference on Computability in Europe, CiE 2008. Vol. 5028. Lecture Notes in Computer Science. Springer, 2008, pp. 359– 369.
[37] Pierre Letouzey. “Programmation fonctionnelle certifi ́ee : L’extraction de programmes dans l’assistant Coq. (Certified functional programming : Program extraction within Coq proof assistant)”. PhD thesis. Univer- sity of Paris-Sud, Orsay, France, 2004. url: https://tel.archives- ouvertes.fr/tel-00150912.
[38] David Monniaux. “The pitfalls of verifying floating-point computations”.
In: TOPLAS 30.3 (May 2008), p. 12. issn: 0164-0925. doi: 10.1145/1353445.1353446. arXiv: cs/0701192. url: http://hal.archives-ouvertes.fr/hal-00128124/en/.
[39] David Monniaux and Cyril Six. “Simple, light, yet formally verified, global common subexpression elimination and loop-invariant code motion”. In: LCTES ’21: 22nd ACM SIGPLAN/SIGBED International Conference on Languages, Compilers, and Tools for Embedded Systems, Virtual Event, Canada, 22 June, 2021. Ed. by J ̈org Henkel and Xu Liu. ACM, 2021, pp. 85–96. doi: 10.1145/3461648.3463850.
[40] Eric Mullen et al. “Œuf: Minimizing the Coq Extraction TCB”. In: Pro- ceedings of the 7th ACM SIGPLAN International Conference on Certi- fied Programs and Proofs. CPP 2018. Los Angeles, CA, USA: Associa- tion for Computing Machinery, 2018, 172–185. isbn: 9781450355865. doi: 10.1145/3167089.
[41] Eric Mullen et al. “Verified Peephole Optimizations for CompCert”. In:
SIGPLAN Not. 51.6 (June 2016), 448–461. issn: 0362-1340. doi: 10.1145/2980983.2908109.
[42] Zoe Paraskevopoulou. “Verified Optimizations for Functional Languages”. PhD thesis. Princeton University, Nov. 2020. url: http://zoep.github. io/thesis_final.pdf.
[43] Zoe Paraskevopoulou, John M. Li, and Andrew W. Appel. “Composi- tional optimizations for CertiCoq”. In: Proc. ACM Program. Lang. 5.ICFP (2021), pp. 1–30. doi: 10.1145/3473591.
[44] Fr ́ed ́eric Recoules et al. “Interface Compliance of Inline Assembly: Auto- matically Check, Patch and Refine”. In: 43rd IEEE/ACM International Conference on Software Engineering, ICSE 2021, Madrid, Spain, 22-30 May 2021. IEEE, 2021, pp. 1236–1247. doi: 10.1109/ICSE43902.2021.00113. arXiv: 1903.06407.
[45] Requirements on the Use of Coq in the Context of Common Criteria Eval- uations. Tech. rep. French National Cybersecurity Agency (ANSSI) and INRIA, Sept. 2020. url: https://www.ssi.gouv.fr/uploads/2014/11/ anssi-requirements-on-the-use-of-coq-in-the-context-of-common- criteria-evaluations-v1.0-en.pdf.
[46] Cyril Six. “Optimized and formally-verified compilation for a VLIW pro- cessor”. PhD thesis. Universit ́e Grenoble Alpes, France, July 2021. url: https://hal.archives-ouvertes.fr/tel-03326923.
[47] Cyril Six, Sylvain Boulm ́e, and David Monniaux. “Certified and efficient instruction scheduling: application to interlocked VLIW processors”. In: Proc. ACM Program. Lang. 4.OOPSLA (2020), 129:1–129:29. doi: 10.1145/3428197. HAL: hal-02185883.
[48] Cyril Six et al. “Formally Verified Superblock Scheduling”. In: Certified Programs and Proofs (CPP ’22). Philadelphia, United States, Jan. 2022. doi: 10.1145/3497775.3503679.
[49] Youngju Song et al. “CompCertM: CompCert with C-Assembly Linking and Lightweight Modular Verification”. In: Proc. ACM Program. Lang. 4.POPL (Dec. 2019). doi: 10.1145/3371091.
[50] Matthieu Sozeau et al. “Coq Coq correct! verification of type checking and erasure for Coq, in Coq”. In: Proc. ACM Program. Lang. 4.POPL’20 (2020), 8:1–8:28. doi: 10.1145/3371076.
[51] Chengnian Sun et al. “Toward Understanding Compiler Bugs in GCC and LLVM”. In: Proceedings of the 25th International Symposium on Soft- ware Testing and Analysis. ISSTA 2016. Saarbru ̈cken, Germany: Associa- tion for Computing Machinery, 2016, 294–305. isbn: 9781450343909. doi: 10.1145/2931037.2931074.
[52] The Coq Reference Manual. 8.13.2. Apr. 2021. url: https://github. com/coq/coq/releases/download/V8.13.2/coq-8.13.2-reference-manual. pdf.
[53] Amin Timany and Matthieu Sozeau. Consistency of the Predicative Calcu- lus of Cumulative Inductive Constructions (pCuIC). Research Report RR- 9105. KU Leuven, Belgium ; Inria Paris, Oct. 2017, p. 32. url: https:// hal.inria.fr/hal-01615123.
[54] Jean-Baptiste Tristan and Xavier Leroy. “Formal verification of transla- tion validators: A case study on instruction scheduling optimizations”. In: Proceedings of the 35th ACM Symposium on Principles of Programming Languages (POPL’08). ACM Press, Jan. 2008, pp. 17–27. url: http:// xavierleroy.org/publi/validation-scheduling.pdf.
[55] Yuting Wang, Pierre Wilke, and Zhong Shao. “An Abstract Stack Based Approach to Verified Compositional Compilation to Machine Code”. In: Proc. ACM Program. Lang. 3.POPL (Jan. 2019). doi: 10.1145/3290375.
[56] Yuting Wang et al. “CompCertELF: Verified Separate Compilation of C Programs into ELF Object Files”. In: Proc. ACM Program. Lang. 4.OOP- SLA (Nov. 2020). doi: 10.1145/3428265.
[57] Xuejun Yang et al. “Finding and understanding bugs in C compilers”. In: Programming Language Design and Implementation (PLDI). Association
for Computing Machinery, 2011, pp. 283–294. doi: 10.1145/1993498.1993532.

Certifying C program correctness with respect to CompCert with VeriFast

Stefan Wils, Bart Jacobs
https://arxiv.org/pdf/1202.6472

References

D.Augustandal.Unisim:Anopensimulationenvironmentandlibraryforcomplex architecture design and collaborative development. Computer Architecture Letters, 6(2):45–48, Feb. 2007.
F. Bellard. QEMU, a fast and portable dynamic translator. In ATEC ’05: Pro- ceedings of the annual conference on USENIX Annual Technical Conference, pages 41–41, Berkeley, CA, USA, 2005. USENIX Association.
Y. Bertot and P. Cast ́eran. Interactive Theorem Proving and Program Develop- ment. Coq’Art: The Calculus of Inductive Constructions. Texts in Theoretical Computer Science. Springer-Verlag, 2004.
F. Blanqui, C. Helmstetter, V. Joloboff, J.-F. Monin, and X. Shi. Designing a CPU model: from a pseudo-formal document to fast code. In Proceedings of the 3rd Workshop on Rapid Simulation and Performance Evaluation: Methods and Tools, Heraklion, Greece, January 2011.
Coq Development Team. The Coq Reference Manual, Version 8.2. INRIA Roc- quencourt, France, 2008. http://coq.inria.fr/.
L.Correnson,P.Cuoq,A.Puccetti,andJ.Signoles.Frama-CUserManual,Release Boron-20100401. CEA LIST, Software Reliability Laboratory, Saclay, France, 2010.
A. C. J. Fox and M. O. Myreen. A Trustworthy Monadic Formalization of the ARMv7 Instruction Set Architecture. In ITP, pages 243–258, 2010.
C. Helmstetter, V. Joloboff, and H. Xiao. SimSoC: A full system simulation software for embedded systems. In IEEE, editor, OSSC’09, 2009.
W. A. Hunt, Jr. FM8501: A Verified Microprocessor, volume 795 of LNAI. Springer-Verlag, 1994.
X. Leroy. Formal verification of a realistic compiler. Communications of the ACM,
52(7):107–115, 2009.
X. Leroy and S. Blazy. Formal Verification of a C-like Memory Model and Its Uses for Verifying Program Transformations. J. Autom. Reason., 41(1):1–31, 2008.
P. S. Magnusson and al. Simics: A full system simulation platform. Computer, 35(2):50–58, 2002.
Open SystemC Initiative. SystemC v2.2.0 Language Reference Manual (IEEE Std 1666-2005), 2006. http://www.systemc.org/.
S. Peyton Jones. Tackling the Awkward Squad: monadic input/output, concurrency, exceptions, and foreign-language calls in Haskell. Online lecture notes, 2010.
OSCI SystemC TLM 2.0.1, 2007. http://www.systemc.org/.