Publication:4692630
From MaRDI portal
zbMath0698.68011MaRDI QIDQ4692630
Edsger W. Dijkstra, C. S. Scholten
Publication date: 5 June 1993
03B70: Logic in computer science
68Q55: Semantics in the theory of computing
68Q60: Specification and verification (program logics, model checking, etc.)
68-02: Research exposition (monographs, survey articles) pertaining to computer science
Related Items
European summer meeting of the Association for Symbolic Logic, Demonic operators and monotype factors, Equality algebras, Unnamed Item, Discovering boundary algebra: A simple notation for Boolean algebra and the truth functors, State-space supervisory control of reconfigurable discrete event systems, Extended Static Checking by Calculation Using the Pointfree Transform, Computing and the cultures of proving, Toward an Automatic Approach to Greedy Algorithms, On strongest necessary and weakest sufficient conditions, On calculational proofs, Mechanical inference of invariants for FOR-loops, Structured derivations: a unified proof style for teaching mathematics, An elementary and unified approach to program correctness, A temporal logic approach to discrete event control for the safety canonical class, Duality beyond sober spaces: Topological spaces and observation frames, Predicate transformers and higher-order programs, Extremal solutions of inequations over lattices with applications to supervisory control, Embedding a demonic semilattice in a relation algebra, Formalizing Dijkstra's predicate transformer wp in weak second-order logic, An experiment with the use of predicate transformers in UNITY, Equational propositional logic, Calculating with procedure calls, Unity properties and sequences of states, some observations, Eliminating the substitution axiom from UNITY logic, Regular algebra applied to language problems, Efficient weakest preconditions, Command algebras, recursion and program transformation, Equational reasoning about nondeterministic processes, Axioms and models of linear logic, Applying relation algebra and RelView to solve problems on orders and lattices, Algebraic reasoning for probabilistic action systems and while-loops, Modelling higher-order dual nondeterminacy, Alternating states for dual nondeterminism in imperative programming, A new taxonomy of sublinear right-to-left scanning keyword pattern matching algorithms, A general technique for proving lock-freedom, Local proofs for global safety properties, Derivation of logic programs by functional methods, Repetitions, known or unknown?, Weakest preconditions for progress, Calculate categorically!, Structured calculational proof, Joining specification statements, Mechanizing some advanced refinement concepts, Nondeterminacy and recursion via stacks and games, The lattice of data refinement, Proof rules for recursive procedures, Properties of concurrent programs, The weakest precondition calculus: Recursion and duality, ``Everywhere in predicate algebra and modal logic, A relation algebraic model of robust correctness, Relation-algebraic semantics, Parallel constructions of maximal path sets and applications to short superstrings, A methodology for designing proof rules for fair parallel programs, A predicate transformer for the progress property `to-always', A foundation for modular reasoning about safety and progress properties of state-based concurrent programs, How to progress a database, Fixpoint semantics and simulation, Composing leads-to properties, A generalization of Naundorf's fixpoint theorem, Constructive design of a hierarchy of semantics of a transition system by abstract interpretation, The associativity of equivalence and the Towers of Hanoi problem, Model-based specification, The joy of formula manipulation, Annotation inference for modular checkers, On the desirability of mechanizing calculational proofs, The sliding-window protocol revisited, Stabilization and blocking in state feedback control of discrete event systems, From Boolean algebra to unified algebra, Predicate transformers as power operations, DUALITY: A simple formalism for the analysis of UNITY, Safety and progress of recursive procedures, Parallelization of divide-and-conquer in the Bird-Meertens formalism, Conditional composition, An approach to literate and structured formal developments, Towards reasoning about Hoare relations, Refinement algebra for probabilistic programs, Quasi-boolean equivalence, Observations in using parallel and sequential evolutionary algorithms for automatic software testing, Syntax-based synthesis for temporal-safety supervision, A theory for execution-time derivation in real-time programs, Probabilistic Choice in Refinement Algebra, A Practical Single Refinement Method for B, Resolution-Like Theorem Proving for High-Level Conditions, Correctness of high-level transformation systems relative to nested conditions, Pre-adjunctions in order enriched categories
