• Z

  • Referenced in 286 articles [sw10291]
  • Using Z. Specification, refinement, and proof. The book is an in-depth 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...
  • CSP-prover

  • 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 non-determinism. For this reason ... fixed points, and (2) to prove CSP refinement between two fixed points. CSP-Prover 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...
  • HOL-Z

  • 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 proof-oriented ... then refine it to an efficient computation-oriented 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 correct-by-construction ... 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...
  • Edmonds-Karp

  • 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 Edmonds-Karp 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 coarse-grain 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...