• Ynot

  • Referenced in 35 articles [sw12334]
  • Ynot, dependent types for imperative programs. We describe an axiomatic extension to the Coq proof ... contribution of our extension, which we call Ynot, is the added support for computations that ... mutable store, and throwing/catching exceptions.The axioms of Ynot form a small trusted computing base which...
  • ACL2

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

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

  • Referenced in 90 articles [sw15222]
  • seL4: formal verification of an OS kernel. Complete...