Mathematical software

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

cminor