• seL4

  • Referenced in 91 articles [sw15222]
  • implementation. We assume correctness of compiler, assembly code, and hardware, and we used a unique ... first formal proof of functional correctness of a complete, general-purpose operating-system kernel. Functional...
  • cminor

  • Referenced in 19 articles [sw09739]
  • imperative programming language; there are proved-correct optimizing compilers from C to cminor and from ... step of the proved-correct compiler) that is motivated by the need to support future ... also compiled by a proved-correct compiler with formal end-to-end correctness guarantees...
  • AXIOM

  • Referenced in 173 articles [sw00063]
  • mathematically correct type hierarchy. It has a programming language and a built-in compiler...
  • MizarMode

  • Referenced in 18 articles [sw01973]
  • developed in the traditional “write-compile-correct” software programming loop. While this method...
  • CertiCoq

  • Referenced in 11 articles [sw22728]
  • project aims to build a proven-correct compiler for dependently-typed, functional languages, such ... proof assistant. A proved-correct compiler consists of a high-level functional specification, machine-verified ... important properties, such as safety and correctness, and a mechanism to transport those proofs ... both engineering challenges and foundational questions about compilers for dependently-typed languages...
  • Pilsner

  • Referenced in 6 articles [sw20004]
  • develop a compositional notion of compiler correctness that is modular (preserved under linking), transitive (supports ... compiler for S, and (2) a hand-coded self-modifying T module, proven correct w.r.t...
  • GCminor

  • Referenced in 4 articles [sw22622]
  • certified framework for compiling and executing garbage-collected languages. We describe the design, implementation ... machine-certified framework for correct compilation and execution of programs in garbage-collected languages...
  • IBM Scratchpad

  • Referenced in 34 articles [sw00429]
  • mathematically correct type hierarchy. It has a programming language and a built-in compiler. Axiom...
  • FISHPAK

  • Referenced in 99 articles [sw08012]
  • demonstration on your computer that you can correctly produce FISHPACK executables. The FISHPACK library ... library and driver executables under the compiler you specify when you run ”make”. If your...
  • SVM Toolbox

  • Referenced in 9 articles [sw14742]
  • sure you have the mex compiler set up correctly - you may need to see your...
  • CVT

  • Referenced in 16 articles [sw09952]
  • code-generator (equivalently, a compiler or a translator) is a correct implementation of the source...
  • CakeML

  • Referenced in 53 articles [sw08799]
  • REPL) in x86-64 machine code. Our correctness theorem ensures that this REPL implementation prints ... lexing, parsing, type checking, incremental and dynamic compilation, garbage collection, arbitrary-precision arithmetic, and compiler...
  • Dafny

  • Referenced in 73 articles [sw00183]
  • used to verify the functional correctness of programs.The Dafny programming language is designed to support ... constructs are used only during verification; the compiler omits them from the executable code.The Dafny...
  • ftnchek

  • Referenced in 1 article [sw20720]
  • user should verify that the program compiles correctly...
  • Pochoir

  • Referenced in 10 articles [sw25851]
  • compiler. Pochoir (pronounced ”PO-shwar”) is a compiler and run-time system for implementing stencil ... checking functional correctness or performance, user can employ either a native C++ compiler or Pochoir...
  • VeriStar

  • Referenced in 3 articles [sw09393]
  • machine-verified program logics and compilers giving foundational correctness guarantees.par VeriStar is (1) purely functional ... program is safe, the program will be compiled to a semantically equivalent assembly program that...
  • Frigate

  • Referenced in 2 articles [sw41616]
  • secure computation. To ensure correctness we apply bestpractices for compiler design and development, including ... compiler will allow future secure computationimplementations to be developed quickly and correctly...
  • Pinocchio

  • Referenced in 42 articles [sw10193]
  • evaluation key to produce a proof of correctness. The proof is only 288 bytes, regardless ... provides an end-to-end toolchain that compiles a subset of C into programs that...
  • Joogie

  • Referenced in 4 articles [sw13771]
  • provide assistance to the compiler optimization. Compared to verification of correctness properties, the translation from...
  • ScaffCC

  • Referenced in 10 articles [sw21654]
  • quantum computing applications. ScaffCC enables researchers to compile quantum applications written in Scaffold ... level quantum assembly format (QASM), apply error correction, and generate time and area metrics...