Results 1 to 20 of 347
Sort by:

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