
Z
 Referenced in 286 articles
[sw10291]
 Using Z. Specification, refinement, and proof. The book is an indepth introduction ... integration of $Z$ with the refinement calculus and data refinement. The overall presentation is fluent ... further on in the book. Rather, most proofs are omitted and replaced by an appeal...

LEGO
 Referenced in 108 articles
[sw09685]
 natural deduction style. It supports refinement proof as a basic operation. The system design emphasizes...

Rodin
 Referenced in 92 articles
[sw07083]
 that provides effective support for refinement and mathematical proof. The platform is open source, contributes...

CSPprover
 Referenced in 17 articles
[sw11465]
 interactive theorem prover dedicated to refinement proofs within the process algebra CSP. It aims specifically ... proofs on infinite state systems, which may also involve infinite nondeterminism. For this reason ... fixed points, and (2) to prove CSP refinement between two fixed points. CSPProver implements...

Isabelle/Circus
 Referenced in 13 articles
[sw15208]
 integration of Z and CSP with a refinement calculus. Its semantics is based on Hoare ... based on Isabelle/HOL). We derive proof rules from this semantics and implement ... tactic support that finally allows for proofs of refinement for Circus processes (involving both data...

ProofPower
 Referenced in 57 articles
[sw06339]
 ProofPower provides support for specification and proof in Z using a semantic embedding ... into HOL. The DAZ tool supporting refinement of Z to the SPARK subset...

HOLZ
 Referenced in 11 articles
[sw02996]
 their proof, and  generating proof obligations resulting from refinement statements for functional and data refinement...

CAVA LTL Modelchecker
 Referenced in 17 articles
[sw28830]
 Isabelle Refinement Framework, which allows us to split its correctness proof into (1) the proof ... formalized pseudocode”, and (2) a verified refinement step in which mathematical sets and other abstract...

mkbTT
 Referenced in 6 articles
[sw10018]
 describe the inference system, give the full proof of its correctness and comment on completeness ... isomorphisms are presented as refinements together with all proofs. We furthermore describe the implementation...

csp2B
 Referenced in 21 articles
[sw07703]
 proof obligations may be generated. Use of csp2B means that abstract specifications and refinements...

ArcAngel
 Referenced in 14 articles
[sw01812]
 present ArcAngel, a language for defining such refinement tactics; we present the language, its semantics ... tactic language has a denotational semantics and proof theory...

Jakarta
 Referenced in 18 articles
[sw01269]
 refinement; the JaKarTa Prover Interface (JPI), a compiler that translates JSL specifications into proof assistants...

CoqEAL
 Referenced in 5 articles
[sw03703]
 refinements which allows us to prove the correctness of our algorithms on a prooforiented ... then refine it to an efficient computationoriented version. The proofs are transported mostly automatically...

Fiat
 Referenced in 14 articles
[sw21357]
 Fiat is a library for the Coq proof assistant for synthesizing efficient correctbyconstruction ... refined into efficient implementations via automated tactics. Each derivation in Fiat produces a formal proof...

F*
 Referenced in 20 articles
[sw27563]
 tool with the expressive power of a proof assistant based on dependent types. After verification ... type system includes dependent types, monadic effects, refinement types, and a weakest precondition calculus. Together ... combination of SMT solving and interactive proofs...

ArgoCLP
 Referenced in 12 articles
[sw07192]
 constructive calculus, and thirdly the proofs generated can be transformed into a human readable format ... method). The calculus is made efficient by refinements such as having redundant axioms...

Gabow SCC
 Referenced in 8 articles
[sw28915]
 components of a directed graph. Using data refinement techniques, we extract efficient code that performs ... using large parts of the proofs when defining variants of the algorithm. We demonstrate this...

EdmondsKarp
 Referenced in 6 articles
[sw28548]
 formal proof closely follows a standard textbook proof, and is accessible even without being ... formalization. We then use stepwise refinement to obtain the EdmondsKarp algorithm, and formally prove...

FoCaLiZe
 Referenced in 10 articles
[sw12384]
 proof assistant to check the proofs, a source file for the OCaml compiler to build ... inheritance mechanisms, the language allows to refine a development from the coarsegrain specification...

ellipticcovers.lib
 Referenced in 11 articles
[sw20805]
 tropical elliptic curve to more refined Feynman integrals. This result easily implies the tropical analogue ... tropical generalization leads to an alternative proof of mirror symmetry for elliptic curves. We believe...