• Z

  • Referenced in 286 articles [sw10291]
  • Using Z. Specification, refinement, and proof. The book is an in-depth introduction ... with the exception of the natural deduction calculus, see below -- only introduction ... integration of $Z$ with the refinement calculus and data refinement. The overall presentation is fluent ... tedious exposition of the natural deduction calculus, which is not used further...
  • JML

  • Referenced in 190 articles [sw04597]
  • languages, with some elements of the refinement calculus...
  • Circus

  • Referenced in 90 articles [sw21828]
  • imperative CSP, Z, and the refinement calculus. We describe the language of Circus...
  • qGCL

  • Referenced in 26 articles [sw39240]
  • body of laws, and provides a refinement calculus supporting the verification and derivation of programs...
  • ZRC

  • Referenced in 14 articles [sw21827]
  • Refinement Calculus for Z. The fact that Z is a specification language only, with ... that, we present ZRC, a refinement calculus based on Morgan’s work that incorporates ... conventions. This work builds upon existing refinement techniques for Z, but distinguishes itself mainly ... laws of ZRC. More than a refinement calculus, ZRC is a theory of refinement...
  • ArcAngel

  • Referenced in 14 articles [sw01812]
  • tactic language for refinement. Morgan’s refinement calculus is a successful technique for developing software ... present ArcAngel, a language for defining such refinement tactics; we present the language, its semantics...
  • Isabelle/Circus

  • Referenced in 13 articles [sw15208]
  • with a refinement calculus. Its semantics is based on Hoare and He’s unifying theories ... support that finally allows for proofs of refinement for Circus processes (involving both data...
  • VPM

  • Referenced in 11 articles [sw07364]
  • dynamic semantics (based on a refinement calculus and graph transformation) where the structure and operational...
  • LEGO

  • Referenced in 108 articles [sw09685]
  • Calculus of Constructions (CC), the Generalized Calculus of Constructions (GCC) and the Unified Theory ... natural deduction style. It supports refinement proof as a basic operation. The system design emphasizes...
  • F*

  • Referenced in 20 articles [sw27563]
  • dependent types, monadic effects, refinement types, and a weakest precondition calculus. Together, these features allow...
  • ArcAngelC

  • Referenced in 6 articles [sw06338]
  • refinement theory and calculus are distinctive, but since refinements may be long and repetitive...
  • ArgoCLP

  • Referenced in 12 articles [sw07192]
  • method). The calculus is made efficient by refinements such as having redundant axioms...
  • REFLP

  • Referenced in 1 article [sw01821]
  • logic programs, based on the refinement calculus presented by the authors [Refining specifications to logic...
  • Superposition Calculus

  • Referenced in 4 articles [sw28571]
  • together with the following refinement, inspired by the basic superposition calculus: each clause is associated...
  • Beagle

  • Referenced in 3 articles [sw13649]
  • theories. It implements a refined version of the hierarchic superposition calculus. This system description focuses...
  • FAUST2

  • Referenced in 14 articles [sw23682]
  • computations and fast manipulations based on vector calculus. The abstract model is formally ... reach-avoid) over the abstract model, and refine the outcomes over the concrete dtMP...
  • JavaSPI

  • Referenced in 3 articles [sw23647]
  • language that corresponds to applied $pi$-calculus. This Java model can be symbolically executed ... debugger, formally verified with ProVerif, and further refined to an interoperable Java implementation...
  • Alpha

  • Referenced in 6 articles [sw13717]
  • uniformization, parallelization for instance), the description is refined until it may be interpreted ... parallelization, code generation, language semantics, convex polyhedra calculus, abstract and non-standard interpretation, program verification...
  • TimeSquare

  • Referenced in 4 articles [sw15830]
  • functional, elastic (can be abstracted or refined) and multiform. TimeSquare is based on the latest ... based editor of constraints, a polychronous clock calculus engine able to process a partial order...
  • mkbTT

  • Referenced in 6 articles [sw10018]
  • tools. Knuth-Bendix completion is a classical calculus in automated deduction for transforming ... pair criteria and isomorphisms are presented as refinements together with all proofs. We furthermore describe...