
cminor
 Referenced in 19 articles
[sw09739]
 Separation Logic for SmallStep cminor. cminor is a midlevel 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 higherorder logic. Distinctive features of HasCasl include partial higherorder ... effects, including a monadbased 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 firstorder 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, semanticspreserving 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 ... smallstep 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...

VSTFloyd
 Referenced in 2 articles
[sw28118]
 shallowly embedded higherorder separation Hoare logic which is proved sound in Coq with respect...

KAD
 Referenced in 2 articles
[sw32231]
 form a simple algebraic basis for Hoare logics, dynamic logics or predicate transformer semantics...

Algebraic_VCs
 Referenced in 2 articles
[sw32217]
 entry provides a verification component for Hoare logic based on Kleene algebra with tests, verification...

HolBA
 Referenced in 1 article
[sw40808]
 Hoarestyle logic for unstructured programs. Enabling Hoarestyle reasoning for lowlevel code ... found. We introduce the novel Hoarestyle program logic (mathcal{L}_A), which interprets postconditions...

Tecton
 Referenced in 9 articles
[sw28905]
 firstorder 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 13 articles
[sw21184]
 introduce Isabelle/UTP, a novel mechanisation of Hoare and He’s unifying theories of programming ... alphabetised predicates, supporting metalogical reasoning that is parametric in the underlying notions of values...

VeriCon
 Referenced in 5 articles
[sw16297]
 concrete counterexample. VeriCon uses firstorder logic to specify admissible network topologies and desired network ... wide invariants, and then implements classical FloydHoareDijkstra deductive verification using Z3. Our preliminary...

UTP2
 Referenced in 5 articles
[sw06342]
 goal was to support the higherorder 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 higherorder 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 HoareParallel, 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 modellevel OG proof using HoareParallel...

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...