scientific article; zbMATH DE number 3705887
From MaRDI portal
Publication:3898009
zbMATH Open0451.68018MaRDI QIDQ3898009FDOQ3898009
Authors: Ralph-Johan Back
Publication date: 1980
Title of this publication is not available (Why is that?)
General topics in the theory of software (68N01) Specification and verification (program logics, model checking, etc.) (68Q60)
Cited In (45)
- Proving total correctness of nondeterministic programs in infinitary logic
- Program derivation using the refinement calculator
- The refinement calculus of reactive systems
- 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
- Exits in the refinement calculus
- Refinement concepts formalised in higher order logic
- A continuous semantics for unbounded nondeterminism
- Combining angels, demons and miracles in program specifications
- Non-deterministic expressions and predicate transformers
- On the lattice of specifications: Applications to a specification methodology
- Fifty years of Hoare's logic
- Blaming the client: on data refinement in the presence of pointers
- 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
- Contracts, games, and refinement.
- Data refinement of predicate transformers
- 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
- Data refinement of invariant based programs
- Invariants and closures in the theory of rewrite systems
- 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)