• Mathemagix

  • Referenced in 42 articles [sw00553]
  • symbolic and certified numeric algorithms. This language can be compiled and interpreted, and it features ... will illustrate possibilities offered for certified numeric computations with balls and intervals...
  • 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 ... framework extends Leroy’s Coq-certified Compcert compiler and Cminor intermediate language...
  • Template-Coq

  • Referenced in 4 articles [sw27569]
  • used in the CertiCoq certified compiler project [4], as its front-end language, to derive...
  • CiaoPP

  • Referenced in 45 articles [sw12089]
  • assertions which cannot be checked completely at compile-time, etc. The abstract model ... analyzers is used in the system to certify that an untrusted mobile code is safe...
  • WebAssembly

  • Referenced in 1 article [sw40303]
  • self-certifying compilation framework for WebAssembly. A self-certifying compiler is designed to generate ... design and implementation of a self-certifying compilation framework for WebAssembly, a new intermediate language...
  • Fiat

  • Referenced in 14 articles [sw21357]
  • Fiat produces a formal proof trail certifying that the synthesized program meets the original specification ... equivalent OCaml program that can be compiled and run as normal...
  • Jakarta

  • Referenced in 18 articles [sw01269]
  • refinement; the JaKarTa Prover Interface (JPI), a compiler that translates JSL specifications into proof assistants ... Goal of the work is to derive certified Byte Code Verifiers by abstraction from...
  • MetaCoq

  • Referenced in 1 article [sw40004]
  • manipulating Coq terms and developing certified plugins (i.e. translations, compilers or tactics...
  • IML - Integer Matrix Library

  • Referenced in 16 articles [sw00440]
  • integers. IML is designed to be compiled with a CBLAS library (e.g., ATLAS/BLAS ... right nullspace of an integer matrix. Certified linear system solving: compute a minimal denominator solution...
  • FoCaLiZe

  • Referenced in 10 articles [sw12384]
  • providing a programming environment to develop certified programs. The environment is based on a functional ... FoCaLiZe source code development, the focalizec compiler produces three source files: a source file...
  • Bedrock

  • Referenced in 4 articles [sw28530]
  • core combining characteristics of assembly languages and compiler intermediate languages. From this foundation, we take ... language”: we introduce an expressive notion of certified low-level macros, sufficient to build ... level of these macros only imposes a compile-time cost, via the execution of functional...
  • Slicing

  • Referenced in 1 article [sw29542]
  • Towards Certified Slicing. Slicing is a widely-used technique with applications in e.g. compiler technology...
  • MMTTeX

  • Referenced in 2 articles [sw31595]
  • communicating mathematical knowledge and the latter at certifying its correctness. MMTTeX aims at combining ... content during Open image in new window compilation and substitutes it with Open image...
  • ACL2

  • Referenced in 283 articles [sw00060]
  • ACL2 is both a programming language in which...
  • Coq

  • Referenced in 1890 articles [sw00161]
  • Coq is a formal proof management system. It...
  • Dafny

  • Referenced in 73 articles [sw00183]
  • Dafny is an imperative object-based language with...
  • Isabelle

  • Referenced in 713 articles [sw00454]
  • Isabelle is a generic proof assistant. It allows...
  • Maple

  • Referenced in 5373 articles [sw00545]
  • The result of over 30 years of cutting...
  • Mathematica

  • Referenced in 6355 articles [sw00554]
  • Almost any workflow involves computing results, and that...
  • MiniSat

  • Referenced in 566 articles [sw00577]
  • An extensible SAT-solver. MiniSat is a minimalistic...