• Boogie

  • Referenced in 118 articles [sw07714]
  • verifiers for Dafny, Chalice, and Spec#. A previous version of the language was called BoogiePL...
  • Chalice

  • Referenced in 7 articles [sw07704]
  • Chalice is an experimental language that explores specification and verification of concurrency in programs ... includes an automatic static program verifier for Chalice...
  • Dafny

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

  • Referenced in 290 articles [sw03522]
  • Eiffel is an ISO-standardized, object-oriented programming...
  • ACSL

  • Referenced in 48 articles [sw04216]
  • The Advanced Continuous Simulation Language, or ACSL (pronounced...
  • Spec#

  • Referenced in 121 articles [sw04598]
  • The Spec# programming system is a new attempt...
  • z3

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

  • Referenced in 80 articles [sw07083]
  • The Rodin Platform is an Eclipse-based IDE...
  • ProB

  • Referenced in 62 articles [sw07084]
  • ProB: an automated analysis toolset for the B...
  • VCC

  • Referenced in 68 articles [sw07220]
  • VCC is a mechanical verifier for concurrent C...
  • VeriFast

  • Referenced in 57 articles [sw07705]
  • The VeriFast program verifier. This note describes a...
  • cminor

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

  • Referenced in 278 articles [sw10291]
  • Using Z. Specification, refinement, and proof. The book...