• cminor

  • Referenced in 19 articles [sw09739]
  • Separation Logic for Small-Step cminor. cminor is a mid-level imperative programming language; there ... that it is suitable for Hoare Logic reasoning and we have designed a Separation Logic...
  • HasCasl

  • Referenced in 17 articles [sw00399]
  • expressive standard language for higher-order logic. Distinctive features of HasCasl include partial higher-order ... effects, including a monad-based generic Hoare logic...
  • Java+ITP

  • Referenced in 8 articles [sw32259]
  • verification tool based on Hoare logic and algebraic semantics. Java+ITP is an experimental tool ... supports compositional reasoning in a Hoare logic for this Java fragment that we propose ... algebraic semantics. After being decomposed, Hoare triples are translated into semantically equivalent first-order verification ... develop similarly extensible and modular Hoare logics on which generic program verification tools...
  • CertiCrypt

  • Referenced in 6 articles [sw09443]
  • programming language tools (observational equivalence, relational Hoare logic, semantics-preserving program transformations) to assist...
  • Crowfoot

  • Referenced in 5 articles [sw07706]
  • assertion language, based on separation logic, features nested Hoare triples which describe the behaviour ... developments in the mathematical foundations of Hoare logics with nested triples...
  • Bedrock

  • Referenced in 4 articles [sw28530]
  • Programming System: Combining Generative Metaprogramming and Hoare Logic in an Extensible Program Verifier. We report...
  • Simpl

  • Referenced in 1 article [sw32234]
  • Sequential Imperative Programming Language Syntax, Semantics, Hoare Logics and Verification Environment. We present the theory ... small-step operational semantics) and Hoare logics for both partial as well as total correctness ... prove soundness and completeness of the Hoare logic. We integrate and automate the Hoare logic...
  • VST-Floyd

  • Referenced in 2 articles [sw28118]
  • shallowly embedded higher-order separation Hoare logic which is proved sound in Coq with respect...
  • KAD

  • Referenced in 1 article [sw32231]
  • form a simple algebraic basis for Hoare logics, dynamic logics or predicate transformer semantics...
  • Algebraic_VCs

  • Referenced in 1 article [sw32217]
  • entry provides a verification component for Hoare logic based on Kleene algebra with tests, verification...
  • Tecton

  • Referenced in 9 articles [sw28905]
  • first-order logic formulas and of program specifications expressed using formulas in Hoare’s axiomatic...
  • Hoarescope

  • Referenced in 0 articles [sw05569]
  • programs over natural numbers using Hoare logic (Hoare calculus). It can be used...
  • Isabelle/UTP

  • Referenced in 11 articles [sw21184]
  • introduce Isabelle/UTP, a novel mechanisation of Hoare and He’s unifying theories of programming ... alphabetised predicates, supporting meta-logical reasoning that is parametric in the underlying notions of values...
  • VeriCon

  • Referenced in 5 articles [sw16297]
  • concrete counterexample. VeriCon uses first-order logic to specify admissible network topologies and desired network ... wide invariants, and then implements classical Floyd-Hoare-Dijkstra deductive verification using Z3. Our preliminary...
  • UTP2

  • Referenced in 5 articles [sw06342]
  • goal was to support the higher-order logic, alphabets, equational reasoning and “programs as predicates ... literature, from the seminal work by Hoare & He [HH98] onwards. This paper describes...
  • Saoithin

  • Referenced in 4 articles [sw06341]
  • goal was to support the higher-order logic, alphabets, equational reasoning and “programs as predicates ... literature, from the seminal work by Hoare & He [HH98] onwards. This paper describes...
  • Complx

  • Referenced in 0 articles [sw21502]
  • method. Our framework combines the approaches of Hoare-Parallel, a formalisation of OG in Isabelle/HOL ... synchronisation. We additionally define an OG logic, which we prove sound w.r.t. the semantics ... have a model-level OG proof using Hoare-Parallel...
  • ACL2

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

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

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