• Mizar

  • Referenced in 505 articles [sw04704]
  • system (including verifier) is coded in Pascal using the Free Pascal compiler...
  • CompCert

  • Referenced in 49 articles [sw09737]
  • usable for critical embedded software. Such verified compilers come with a mathematical, machine-checked proof ... possibility of compiler-introduced bugs, verified compilers strengthen the guarantees that can be obtained ... project is the CompCert C verified compiler, a high-assurance compiler for almost...
  • CakeML

  • Referenced in 53 articles [sw08799]
  • have developed and mechanically verified an ML system called CakeML, which supports a substantial subset ... lexing, parsing, type checking, incremental and dynamic compilation, garbage collection, arbitrary-precision arithmetic, and compiler ... verification. In particular, our formally verified compiler can bootstrap itself: we apply the verified compiler ... itself to produce a verified machine-code implementation of the compiler. Additionally, our compiler proof...
  • Spec#

  • Referenced in 123 articles [sw04598]
  • programming language, the Spec# compiler, and the Boogie static program verifier. The language includes constructs ... compiler emits run-time checks to enforce these specifications, and the verifier can check...
  • ML

  • Referenced in 522 articles [sw01218]
  • languages to be completely specified and verified using formal semantics. Its types and pattern matching ... other formal languages, such as in compiler writing, automated theorem proving and formal verification. (wikipedia...
  • Dafny

  • Referenced in 73 articles [sw00183]
  • static program verifier can be used to verify the functional correctness of programs.The Dafny programming ... constructs are used only during verification; the compiler omits them from ... executable code.The Dafny verifier is run as part of the compiler. As such, a programmer...
  • CompCertTSO

  • Referenced in 12 articles [sw08230]
  • CompCertTSO: a verified compiler for relaxed-memory concurrency. In this article, we consider the semantic ... design and verified compilation of a C-like programming language for concurrent shared-memory computation ... model. In turn, this complexity makes verified compilation both essential and challenging.We describe ClightTSO ... performance code, and CompCertTSO, a formally verified compiler from ClightTSO to x86 assembly language, building...
  • EasyCrypt

  • Referenced in 33 articles [sw09738]
  • automated theorem provers, and then compiled into verifiable proofs in the CertiCrypt framework. The tool...
  • Piton

  • Referenced in 12 articles [sw28721]
  • object code produced by verified compilers. Thus, I envisioned the language as the first software ... link in a trusted chain from verified hardware to verified applications programs. Thinking...
  • CertiCoq

  • Referenced in 11 articles [sw22728]
  • CertiCoq: a verified compiler for Coq. The CertiCoq project aims to build a proven-correct ... proved-correct compiler consists of a high-level functional specification, machine-verified proofs of important ... both engineering challenges and foundational questions about compilers for dependently-typed languages...
  • C-XSC

  • Referenced in 110 articles [sw00181]
  • numerical algorithms delivering highly accurate and automatically verified results. It provides a large number ... available for all computers with a C++ compiler translating the AT&T language standard...
  • Pilsner

  • Referenced in 6 articles [sw20004]
  • Pilsner: a compositionally verified compiler for a higher-order imperative language. Compiler verification is essential ... CompCert) has focused on verifying whole-program compilers. To support separate compilation ... enable linking of results from different verified compilers, it is important to develop a compositional ... them to additionally verify (1) Zwickel, a direct non-optimizing compiler...
  • Density Compiler

  • Referenced in 6 articles [sw28659]
  • Verified Compiler for Probability Density Functions. Bhat et al. [TACAS 2013] developed an inductive compiler ... this work, we implement such a compiler for a modified version of this language within ... predicates, this yields a fully verified, executable density compiler. The proof is done...
  • Pinocchio

  • Referenced in 42 articles [sw10193]
  • introduce Pinocchio, a built system for efficiently verifying general computations while relying only on cryptographic ... toolchain that compiles a subset of C into programs that implement the verifiable computation protocol...
  • F@BOOL@

  • Referenced in 3 articles [sw21004]
  • BOOL@: Experiment with a simple verifying compiler based on SAT-solvers. A verifying compiler ... language to equivalent executable programs and proves (verifies) mathematical statements specified by a human concerning ... user friendly, compact, and portable verifying compiler of annotated computational programs that uses efficient...
  • cminor

  • Referenced in 19 articles [sw09739]
  • step of the proved-correct compiler) that is motivated by the need to support future ... cminor programs can be verified using Separation Logic and also compiled by a proved-correct...
  • Toolchain

  • Referenced in 27 articles [sw09517]
  • Verified Software Toolchain: The software toolchain includes static analyzers to check assertions about your program ... optimizing compilers to translate your program to machine language; operating systems and libraries to supply ... context for your program. The Verified Software Toolchain project assures with machine-checked proofs that...
  • HACL*

  • Referenced in 4 articles [sw36852]
  • Verified Modern Cryptographic Library. HACL* is a verified portable C cryptographic library that implements modern ... compiled to readable C code. The F* source code for each cryptographic primitive is verified ... itself be compiled via the CompCert verified C compiler or mainstream compilers like ... CLANG. When compiled with GCC on 64-bit platforms, our primitives are as fast...
  • CVT

  • Referenced in 16 articles [sw09952]
  • verifying that the target code produced by a code-generator (equivalently, a compiler...
  • CompCertS

  • Referenced in 3 articles [sw22722]
  • Compcerts: a memory-aware verified C compiler using pointer as integer semantics. The CompCert ... guarantee that the observable behaviour of the compiled code improves on the observable behaviour ... this paper, we present a formally verified C compiler, CompCertS, which is essentially the CompCert...