- Referenced in 7 articles
- 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...
- Referenced in 2 articles
- imperative verification is based on Imperative HOL and its separation logic framework. A major goal...
- Referenced in 14 articles
- 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...
- Referenced in 1 article
- state monad or the Imperative HOL heap monad, and prove a correspondence theorem. We provide...
- Referenced in 283 articles
- ACL2 is both a programming language in which...
- Referenced in 1880 articles
- Coq is a formal proof management system. It...
- Referenced in 698 articles
- Isabelle is a generic proof assistant. It allows...
- Referenced in 522 articles
- ML (’Meta Language’) is a general-purpose functional...
- Referenced in 270 articles
- Programming Perl. Perl is a language for easily...
- Referenced in 95 articles
- Building formal method tools in the Isabelle/Isar framework...
- Referenced in 104 articles
- The Larch family of languages supports a two...
- Referenced in 89 articles
- The KRAKATOA tool for certification of JAVA/JAVACARD programs...
- Referenced in 629 articles
- PVS is a verification system: that is, a...
- Referenced in 879 articles
- Haskell is a standardized, general-purpose purely functional...
- Referenced in 134 articles
- Why3 is a platform for deductive program verification...
- Referenced in 63 articles
- Caduceus used to be a verification tool for...
- Referenced in 583 articles
- Higher Order Logic (HOL) is a programming environment...
- Referenced in 394 articles
- The Nuprl system is a framework for reasoning...
- Referenced in 171 articles
- Twelf is a language used to specify, implement...