
Z
 Referenced in 286 articles
[sw10291]
 Using Z. Specification, refinement, and proof. The book is an indepth 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 ... reachavoid) 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 nonstandard 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. KnuthBendix 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...