CompCert

The CompCert project investigates the formal verification of realistic compilers usable for critical embedded software. Such verified compilers come with a mathematical, machine-checked proof that the generated executable code behaves exactly as prescribed by the semantics of the source program. By ruling out the possibility of compiler-introduced bugs, verified compilers strengthen the guarantees that can be obtained by applying formal methods to source programs. The main result of the project is the CompCert C verified compiler, a high-assurance compiler for almost all of the ISO C90 / ANSI C language, generating efficient code for the PowerPC, ARM and x86 processors.


References in zbMATH (referenced in 45 articles , 3 standard articles )

Showing results 1 to 20 of 45.
Sorted by year (citations)

1 2 3 next

  1. Downen, Paul; Ariola, Zena M.: Compiling with classical connectives (2020)
  2. Sheng, Feng; Zhu, Huibiao; He, Jifeng; Yang, Zongyuan; Bowen, Jonathan P.: Theoretical and practical approaches to the denotational semantics for MDESL based on UTP (2020)
  3. Besson, Frédéric; Blazy, Sandrine; Wilke, Pierre: A verified CompCert front-end for a memory model supporting pointer arithmetic and uninitialised data (2019)
  4. Bouillaguet, Quentin; Bobot, François; Sighireanu, Mihaela; Yakobowski, Boris: Exploiting pointer analysis in memory models for deductive verification (2019)
  5. Kiam Tan, Yong; Myreen, Magnus O.; Kumar, Ramana; Fox, Anthony; Owens, Scott; Norrish, Michael: The verified CakeML compiler backend (2019)
  6. Preoteasa, Viorel; Dragomir, Iulia; Tripakis, Stavros: Mechanically proving determinacy of hierarchical block diagram translations (2019)
  7. Alex A. Alemi, Francois Chollet, Niklas Een, Geoffrey Irving, Christian Szegedy, Josef Urban: DeepMath - Deep Sequence Models for Premise Selection (2018) arXiv
  8. Chen, Hao; Wu, Xiongnan; Shao, Zhong; Lockerman, Joshua; Gu, Ronghui: Toward compositional verification of interruptible OS kernels and device drivers (2018)
  9. Kumar, Ramana; Mullen, Eric; Tatlock, Zachary; Myreen, Magnus O.: Software verification with ITPs should use binary code extraction to reduce the TCB (short paper) (2018)
  10. Zhao, Jinxu; Oliveira, Bruno C. d. S.; Schrijvers, Tom: Formalization of a polymorphic subtyping algorithm (2018)
  11. Besson, Frédéric; Blazy, Sandrine; Wilke, Pierre: Compcerts: a memory-aware verified C compiler using pointer as integer semantics (2017)
  12. Hoffmann, Jan; Das, Ankush; Weng, Shu-Chun: Towards automatic resource bound analysis for OCaml (2017)
  13. Krebbers, Robbert: A formal C memory model for separation logic (2016)
  14. Boldo, Sylvie; Jourdan, Jacques-Henri; Leroy, Xavier; Melquiond, Guillaume: Verified compilation of floating-point computations (2015)
  15. Chatzikyriakidis, Stergios; Luo, Zhaohui: Individuation criteria, dot-types and copredication: a view from modern type theories (2015)
  16. Stewart, Gordon; Beringer, Lennart; Cuellar, Santiago; Appel, Andrew W.: Compositional CompCert (2015)
  17. Théry, Laurent (ed.); Wiedijk, Freek (ed.): Foreword to the special focus on formal proofs for mathematics and computer science (2015)
  18. Wenzel, Makarius: Interactive theorem proving from the perspective of Isabelle/Isar (2015)
  19. Appel, Andrew W.; Dockins, Robert; Hobor, Aquinas; Beringer, Lennart; Dodds, Josiah; Stewart, Gordon; Blazy, Sandrine; Leroy, Xavier: Program logics for certified compilers (2014)
  20. Besson, Frédéric; Blazy, Sandrine; Wilke, Pierre: A precise and abstract memory model for C using symbolic values (2014) ioport

1 2 3 next


Further publications can be found at: http://compcert.inria.fr/publi.html