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

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

1 2 3 next

  1. Larchey-Wendling, Dominique; Monin, Jean-François: The Braga method: extracting certified algorithms from complex recursive schemes in Coq (2022)
  2. Farka, František: \textttslepice: towards a verified implementation of type theory in type theory (2021)
  3. 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)
  4. Liu, Yezhou; Nicolescu, Radu; Sun, Jing: Formal verification of cP systems using Coq (2021)
  5. Namjoshi, Kedar S.; Xue, Anton: A self-certifying compilation framework for WebAssembly (2021)
  6. Smith, Graeme; Coughlin, Nicholas; Murray, Toby: Information-flow control on ARM and POWER multicore processors (2021)
  7. Downen, Paul; Ariola, Zena M.: Compiling with classical connectives (2020)
  8. 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)
  9. Vasilyev, A. A.; Mutilin, V. S.: Predicate extension of symbolic memory graphs for the analysis of memory safety correctness (2020)
  10. Besson, Frédéric; Blazy, Sandrine; Wilke, Pierre: A verified CompCert front-end for a memory model supporting pointer arithmetic and uninitialised data (2019)
  11. Bouillaguet, Quentin; Bobot, François; Sighireanu, Mihaela; Yakobowski, Boris: Exploiting pointer analysis in memory models for deductive verification (2019)
  12. Kiam Tan, Yong; Myreen, Magnus O.; Kumar, Ramana; Fox, Anthony; Owens, Scott; Norrish, Michael: The verified CakeML compiler backend (2019)
  13. Preoteasa, Viorel; Dragomir, Iulia; Tripakis, Stavros: Mechanically proving determinacy of hierarchical block diagram translations (2019)
  14. Alex A. Alemi, Francois Chollet, Niklas Een, Geoffrey Irving, Christian Szegedy, Josef Urban: DeepMath - Deep Sequence Models for Premise Selection (2018) arXiv
  15. Chen, Hao; Wu, Xiongnan; Shao, Zhong; Lockerman, Joshua; Gu, Ronghui: Toward compositional verification of interruptible OS kernels and device drivers (2018)
  16. 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)
  17. Zhao, Jinxu; Oliveira, Bruno C. d. S.; Schrijvers, Tom: Formalization of a polymorphic subtyping algorithm (2018)
  18. Besson, Frédéric; Blazy, Sandrine; Wilke, Pierre: CompCertS: a memory-aware verified C compiler using pointer as integer semantics (2017)
  19. Hoffmann, Jan; Das, Ankush; Weng, Shu-Chun: Towards automatic resource bound analysis for OCaml (2017)
  20. Krebbers, Robbert: A formal C memory model for separation logic (2016)

1 2 3 next

Further publications can be found at: