scientific article; zbMATH DE number 3705887

Cited in

(45)

Proving total correctness of nondeterministic programs in infinitary logic
The refinement calculus of reactive systems
Program derivation using the refinement calculator
A recursion theorem for predicate transformers on inductive data types
Program inversion in the refinement calculus
Data refinement, call by value and higher order programs
Algebra of monotonic Boolean transformers
Refinement concepts formalised in higher order logic
Exits in the refinement calculus
A continuous semantics for unbounded nondeterminism
Non-deterministic expressions and predicate transformers
Combining angels, demons and miracles in program specifications
On the lattice of specifications: Applications to a specification methodology
Blaming the client: on data refinement in the presence of pointers
Fifty years of Hoare's logic
Invariant diagrams with data refinement
Real-time refinement in Manna and Pnueli's temporal logic
Correctness of programs with Pascal-like procedures without global variables
An algebraic approach to the design of compilers for object-oriented languages
An elementary and unified approach to program correctness
Structured derivations: a unified proof style for teaching mathematics
A calculus of refinements for program derivations
Enabledness and termination in refinement algebra
Mechanizing some advanced refinement concepts
Average case optimality for linear problems
Data refinement of predicate transformers
Contracts, games, and refinement.
Program refinement in fair transition systems
The weakest precondition calculus: Recursion and duality
Superposition refinement of reactive systems
A specification-oriented semantics for the refinement of real-time systems
Program composition via unification
Stratified least fixpoint logic
Program composition via unification
Action systems, unbounded nondeterminism, and infinite traces
A simple fixpoint argument without the restriction to continuity
On correct refinement of programs
The lattice of data refinement
Proving program inclusion using Hoare's logic
In praise of algebra
Dual unbounded nondeterminacy, recursion, and fixpoints
Invariants and closures in the theory of rewrite systems
Data refinement of invariant based programs
Wythoff games, continued fractions, cedar trees and Fibonacci searches
Predicate transformers and higher-order programs

This page was built for publication:

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3898009)