scientific article
From MaRDI portal
Publication:3898009
zbMath0451.68018MaRDI QIDQ3898009
Publication date: 1980
Title: zbMATH Open Web Interface contents unavailable due to conflicting licenses.
Specification and verification (program logics, model checking, etc.) (68Q60) General topics in the theory of software (68N01)
Related Items (44)
A recursion theorem for predicate transformers on inductive data types ⋮ A specification-oriented semantics for the refinement of real-time systems ⋮ Program composition via unification ⋮ Stratified least fixpoint logic ⋮ Non-deterministic expressions and predicate transformers ⋮ The weakest precondition calculus: Recursion and duality ⋮ Data refinement, call by value and higher order programs ⋮ A calculus of refinements for program derivations ⋮ Superposition refinement of reactive systems ⋮ An algebraic approach to the design of compilers for object-oriented languages ⋮ Blaming the client: on data refinement in the presence of pointers ⋮ Structured derivations: a unified proof style for teaching mathematics ⋮ An elementary and unified approach to program correctness ⋮ Program composition via unification ⋮ The refinement calculus of reactive systems ⋮ In praise of algebra ⋮ Invariant diagrams with data refinement ⋮ Proving total correctness of nondeterministic programs in infinitary logic ⋮ On correct refinement of programs ⋮ Refinement concepts formalised in higher order logic ⋮ Enabledness and termination in refinement algebra ⋮ A continuous semantics for unbounded nondeterminism ⋮ Data Refinement of Invariant Based Programs ⋮ Data refinement of predicate transformers ⋮ Predicate transformers and higher-order programs ⋮ Combining angels, demons and miracles in program specifications ⋮ On the lattice of specifications: Applications to a specification methodology ⋮ Fifty years of Hoare's logic ⋮ Dual unbounded nondeterminacy, recursion, and fixpoints ⋮ Action systems, unbounded nondeterminism, and infinite traces ⋮ Exits in the refinement calculus ⋮ Program inversion in the refinement calculus ⋮ Real-time refinement in Manna and Pnueli's temporal logic ⋮ Invariants and closures in the theory of rewrite systems ⋮ Algebra of Monotonic Boolean Transformers ⋮ Wythoff games, continued fractions, cedar trees and Fibonacci searches ⋮ Proving program inclusion using Hoare's logic ⋮ Correctness of programs with Pascal-like procedures without global variables ⋮ Average case optimality for linear problems ⋮ Contracts, games, and refinement. ⋮ Mechanizing some advanced refinement concepts ⋮ Program refinement in fair transition systems ⋮ The lattice of data refinement ⋮ A simple fixpoint argument without the restriction to continuity
This page was built for publication:
