-
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 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]
- Hoare-style logic for unstructured programs. Enabling Hoare-style reasoning for low-level code ... found. We introduce the novel Hoare-style program logic (mathcal{L}_A), which interprets postconditions...
-
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 13 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 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...