• Separation Logic

  • Referenced in 7 articles [sw28549]
  • Separation Logic Framework for Imperative HOL. We provide a framework for separation-logic based correctness ... proofs of Imperative HOL programs. Our framework comes with a set of proof methods ... sets, that allow to develop generic imperative algorithms ... data-refinement techniques. As we target Imperative HOL, our programs can be translated to efficiently...
  • Auto2_Imperative_HOL

  • Referenced in 2 articles [sw32246]
  • imperative verification is based on Imperative HOL and its separation logic framework. A major goal...
  • HOL-Boogie

  • Referenced in 14 articles [sw00409]
  • program verification condition generator for an imperative core language. It has front-ends ... paper, however, we present a proof-environment, HOL-BoogieP, that combines Boogie with the interactive...
  • Memoization

  • Referenced in 1 article [sw28640]
  • state monad or the Imperative HOL heap monad, and prove a correspondence theorem. We provide...
  • ACL2

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

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

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

  • Referenced in 522 articles [sw01218]
  • ML (’Meta Language’) is a general-purpose functional...
  • PERL

  • Referenced in 270 articles [sw01225]
  • Programming Perl. Perl is a language for easily...
  • LARCH

  • Referenced in 104 articles [sw02126]
  • The Larch family of languages supports a two...
  • KRAKATOA

  • Referenced in 89 articles [sw03159]
  • The KRAKATOA tool for certification of JAVA/JAVACARD programs...
  • PVS

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

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

  • Referenced in 134 articles [sw04438]
  • Why3 is a platform for deductive program verification...
  • HOL

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

  • Referenced in 394 articles [sw06751]
  • The Nuprl system is a framework for reasoning...
  • Twelf

  • Referenced in 171 articles [sw06888]
  • Twelf is a language used to specify, implement...