• ML

  • Referenced in 524 articles [sw01218]
  • provides pattern matching for function arguments, garbage collection, imperative programming, call-by-value and currying ... languages to be completely specified and verified using formal semantics. Its types and pattern matching...
  • CakeML

  • Referenced in 53 articles [sw08799]
  • have developed and mechanically verified an ML system called CakeML, which supports a substantial subset ... type checking, incremental and dynamic compilation, garbage collection, arbitrary-precision arithmetic, and compiler bootstrapping.Our contributions ... system that is end-to-end verified, demonstrating that each piece of such a verification...
  • dSPIN

  • Referenced in 31 articles [sw09888]
  • functions; function code references (function pointers); garbage collection; symmetry reductions. The design of dSPIN ... supported by both the random simulator and verifier generator. The tool is SPIN-backwards compatible...
  • Coq

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

  • Referenced in 153 articles [sw03136]
  • SLAM is a project for checking that software...
  • SPIN

  • Referenced in 727 articles [sw03455]
  • Spin is a popular open-source software tool...
  • PVS

  • Referenced in 634 articles [sw03484]
  • PVS is a verification system: that is, a...
  • Haskell

  • Referenced in 885 articles [sw03521]
  • Haskell is a standardized, general-purpose purely functional...
  • SLMC

  • Referenced in 74 articles [sw04604]
  • SLMC: A tool for model checking concurrent systems...
  • z3

  • Referenced in 606 articles [sw04887]
  • Z3 is a high-performance theorem prover being...
  • HOL

  • Referenced in 594 articles [sw05492]
  • Higher Order Logic (HOL) is a programming environment...
  • GHC

  • Referenced in 103 articles [sw06691]
  • Secrets of the Glasgow Haskell Compiler inliner. Higher...
  • Boogie

  • Referenced in 120 articles [sw07714]
  • Boogie: An Intermediate Verification Language. Boogie is an...
  • CompCertTSO

  • Referenced in 12 articles [sw08230]
  • CompCertTSO: a verified compiler for relaxed-memory concurrency...
  • CompCert

  • Referenced in 52 articles [sw09737]
  • The CompCert project investigates the formal verification of...
  • cminor

  • Referenced in 19 articles [sw09739]
  • Separation Logic for Small-Step cminor. cminor is...
  • Milawa

  • Referenced in 20 articles [sw09977]
  • The reflective milawa theorem prover is sound (down...
  • Jitawa

  • Referenced in 14 articles [sw12812]
  • Jitawa — a verified Lisp runtime for Milawa. This...
  • UNITY

  • Referenced in 185 articles [sw13461]
  • Simulation model development and analysis in UNITY. We...