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 49 articles , 3 standard articles )

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

1 2 3 next

  1. Farka, František: \textttslepice: towards a verified implementation of type theory in type theory (2021)
  2. Hóu, Zhé; Sanan, David; Tiu, Alwen; Liu, Yang; Hoa, Koh Chuen; Dong, Jin Song: An Isabelle/HOL formalisation of the SPARC instruction set architecture and the TSO memory model (2021)
  3. Namjoshi, Kedar S.; Xue, Anton: A self-certifying compilation framework for WebAssembly (2021)
  4. Downen, Paul; Ariola, Zena M.: Compiling with classical connectives (2020)
  5. 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)
  6. Vasilyev, A. A.; Mutilin, V. S.: Predicate extension of symbolic memory graphs for the analysis of memory safety correctness (2020)
  7. Besson, Frédéric; Blazy, Sandrine; Wilke, Pierre: A verified CompCert front-end for a memory model supporting pointer arithmetic and uninitialised data (2019)
  8. Bouillaguet, Quentin; Bobot, François; Sighireanu, Mihaela; Yakobowski, Boris: Exploiting pointer analysis in memory models for deductive verification (2019)
  9. Kiam Tan, Yong; Myreen, Magnus O.; Kumar, Ramana; Fox, Anthony; Owens, Scott; Norrish, Michael: The verified CakeML compiler backend (2019)
  10. Preoteasa, Viorel; Dragomir, Iulia; Tripakis, Stavros: Mechanically proving determinacy of hierarchical block diagram translations (2019)
  11. Alex A. Alemi, Francois Chollet, Niklas Een, Geoffrey Irving, Christian Szegedy, Josef Urban: DeepMath - Deep Sequence Models for Premise Selection (2018) arXiv
  12. Chen, Hao; Wu, Xiongnan; Shao, Zhong; Lockerman, Joshua; Gu, Ronghui: Toward compositional verification of interruptible OS kernels and device drivers (2018)
  13. 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)
  14. Zhao, Jinxu; Oliveira, Bruno C. d. S.; Schrijvers, Tom: Formalization of a polymorphic subtyping algorithm (2018)
  15. Besson, Frédéric; Blazy, Sandrine; Wilke, Pierre: CompCertS: a memory-aware verified C compiler using pointer as integer semantics (2017)
  16. Hoffmann, Jan; Das, Ankush; Weng, Shu-Chun: Towards automatic resource bound analysis for OCaml (2017)
  17. Krebbers, Robbert: A formal C memory model for separation logic (2016)
  18. Boldo, Sylvie; Jourdan, Jacques-Henri; Leroy, Xavier; Melquiond, Guillaume: Verified compilation of floating-point computations (2015)
  19. Chatzikyriakidis, Stergios; Luo, Zhaohui: Individuation criteria, dot-types and copredication: a view from modern type theories (2015)
  20. Stewart, Gordon; Beringer, Lennart; Cuellar, Santiago; Appel, Andrew W.: Compositional CompCert (2015)

1 2 3 next


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