• BLAST

  • Referenced in 125 articles [sw02937]
  • Linux Driver Verification project. You may download source code or binary releases of BLAST...
  • WhyML

  • Referenced in 25 articles [sw09709]
  • present Why3, a tool for deductive program verification, and WhyML, its programming and specification language ... mutable fields, type invariants, and ghost code. Verification conditions are discharged by Why3 with...
  • HOL-Boogie

  • Referenced in 14 articles [sw00409]
  • annotations in first-order logic.\parIts verification conditions -- constructed via a wp calculus from these ... automated and interactive proof methods for code-verification.\parWe will exploit our proof-environment...
  • CVT

  • Referenced in 15 articles [sw09952]
  • code validation tool (CVT). Automatic verification of a compilation process. We describe CVT -- a fully ... that the target code produced by a code-generator (equivalently, a compiler or a translator ... alternative to a full formal verification of the code-generator program, and has the advantage ... freezing” the code generator design after verification. CVT was developed in the context...
  • SCADE

  • Referenced in 20 articles [sw00829]
  • requirements management, model-based design, simulation, verification, qualifiable/certified code generation, and interoperability with other development...
  • Theano

  • Referenced in 74 articles [sw05894]
  • optimizations, dynamic C code generation, and extensive unit-testing and self-verification. Theano has been...
  • ISP

  • Referenced in 12 articles [sw04895]
  • Order”) is a tool for the formal verification of MPI(Message Passing Interface) programs developed ... However, unlike model checkers, ISP performs code level verification. This means that the tool verifies ... replaying the actual program code without building verification models. ISP has been used to successfully ... lines of MPI/C code for deadlocks and assertion violations. It currently supports over...
  • MAGIC

  • Referenced in 37 articles [sw14159]
  • MAGIC is a software verification project for C source code which verifies conformance of software ... core principles implemented in the MAGIC verification engine, i.e., specification conformance using simulation and abstraction...
  • seL4

  • Referenced in 80 articles [sw15222]
  • experience in performing the formal, machine-checked verification of the seL4 microkernel from an abstract ... implementation. We assume correctness of compiler, assembly code, and hardware, and we used a unique...
  • CakeML

  • Referenced in 44 articles [sw08799]
  • print loop (REPL) in x86-64 machine code. Our correctness theorem ensures that this REPL ... permitted by the semantics of CakeML. Our verification effort touches on a breadth of topics ... more challenging aspects of the verification. In particular, our formally verified compiler can bootstrap itself ... itself to produce a verified machine-code implementation of the compiler. Additionally, our compiler proof...
  • Milawa

  • Referenced in 20 articles [sw09977]
  • logic sound, and prove that the source code for the Milawa kernel (2,000 lines ... results with our previous verification of an x86 machine-code implementation of a Lisp runtime...
  • Checkfence

  • Referenced in 19 articles [sw09939]
  • based formal verification tool that analyzes C code implementing concurrent data types on multiprocessors (concurrent...
  • CompCert

  • Referenced in 44 articles [sw09737]
  • CompCert project investigates the formal verification of realistic compilers usable for critical embedded software. Such ... machine-checked proof that the generated executable code behaves exactly as prescribed by the semantics...
  • Esterel

  • Referenced in 162 articles [sw20012]
  • reactive program. It can generate C-code to be embedded as a reactive kernel ... provide support for explicit or BDD-based verification tools that perform either bisimulation reduction...
  • CSIsat

  • Referenced in 15 articles [sw11407]
  • benchmarks from software verification. Binaries and the source code of CSIsat are publicly available...
  • SeaHorn

  • Referenced in 13 articles [sw18274]
  • customizable framework for experimenting with new software verification techniques. The effectiveness and scalability of SeaHorn ... from SV-COMP 2015 and real avionics code...
  • Lava

  • Referenced in 13 articles [sw28643]
  • such as simulation, formal verification and the generation of code for the production of real...
  • TOKAM-3D

  • Referenced in 9 articles [sw02765]
  • field of application of the code as well as verification results are also presented...
  • PeRIPLO

  • Referenced in 7 articles [sw07896]
  • bounded model checking applications: verification of a given source code incrementally with respect to various...
  • Vertaf

  • Referenced in 4 articles [sw08200]
  • application framework for the design and verification of embedded real-time software. The growing complexity ... components, the synthesis and generation of software code, and the automatic guarantee of nonfunctional properties ... component-based reuse, formal synthesis, and formal verification. A formal UML-based embedded real-time ... automatic generation of multilayer portable efficient code. Formal verification integrates a model checker kernel from...