scientific article; zbMATH DE number 194642

Publication date: 5 June 1993

Title: zbMATH Open Web Interface contents unavailable due to conflicting licenses.

foundations of computer science program proof methodology use of logic in program development

Logic in computer science (03B70) Semantics in the theory of computing (68Q55) Specification and verification (program logics, model checking, etc.) (68Q60) Research exposition (monographs, survey articles) pertaining to computer science (68-02)

Related Items

Abstract Program Slicing, Unnamed Item, Categorical fixed point calculus, Discovering boundary algebra: A simple notation for Boolean algebra and the truth functors, Computing and the cultures of proving, Toward an Automatic Approach to Greedy Algorithms, Equality algebras, On mechanizing proofs within a complete proof system for Unity, An Arithmetically Complete Predicate Modal Logic, Why3-do: the way of harmonious distributed system proofs, State-space supervisory control of reconfigurable discrete event systems, Unnamed Item, On deadlocks of exclusive AND-requests for resources, Cut Elimination in a Class of Sequent Calculi for Pure Type Systems, On strongest necessary and weakest sufficient conditions, Extended Static Checking by Calculation Using the Pointfree Transform, On calculational proofs, Proof rules for recursive procedures, A formalization of programs in first-order logic with a discrete linear order, Quasi-boolean equivalence, Finite representability of semigroups with demonic refinement, Local Symmetry and Compositional Verification, Non-deterministic expressions and predicate transformers, Efficient weakest preconditions, Assumption propagation through annotated programs, From Boolean algebra to unified algebra, Properties of concurrent programs, Compositional Reasoning, The weakest precondition calculus: Recursion and duality, ``Everywhere in predicate algebra and modal logic, A relation algebraic model of robust correctness, Relation-algebraic semantics, European summer meeting of the Association for Symbolic Logic, Predicate transformers as power operations, DUALITY: A simple formalism for the analysis of UNITY, Safety and progress of recursive procedures, Demonic operators and monotype factors, Parallelization of divide-and-conquer in the Bird-Meertens formalism, Conditional composition, Parallel constructions of maximal path sets and applications to short superstrings, An approach to literate and structured formal developments, Pre-adjunctions in order enriched categories, A methodology for designing proof rules for fair parallel programs, A predicate transformer for the progress property `to-always', Mechanical inference of invariants for FOR-loops, Structured derivations: a unified proof style for teaching mathematics, An elementary and unified approach to program correctness, Towards reasoning about Hoare relations, The Formal System of Dijkstra and Scholten, rCOS: Defining Meanings of Component-Based Software Architectures, From probability monads to commutative effectuses, A foundation for modular reasoning about safety and progress properties of state-based concurrent programs, Dijkstra and Hoare monads in monadic computation, Weakest preconditioned goto axiom, How to progress a database, Pointfree expression and calculation: From quantification to temporal logic, Probabilistic Choice in Refinement Algebra, Command algebras, recursion and program transformation, Equational reasoning about nondeterministic processes, Axioms and models of linear logic, A Practical Single Refinement Method for B, Indexed and fibred structures for Hoare logic, Resolution-Like Theorem Proving for High-Level Conditions, Applying relation algebra and RelView to solve problems on orders and lattices, Of wlp and CSP, Algebraic reasoning for probabilistic action systems and while-loops, Modelling higher-order dual nondeterminacy, Derivation of logic programs by functional methods, Repetitions, known or unknown?, A self-certifying compilation framework for WebAssembly, Defense in Depth Formulation and Usage in Dynamic Access Control, A temporal logic approach to discrete event control for the safety canonical class, POLYNOMIAL RING CALCULUS FOR MODAL LOGICS: A NEW SEMANTICS AND PROOF METHOD FOR MODALITIES, 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, Weakest preconditions for progress, Calculating with procedure calls, Unity properties and sequences of states, some observations, Calculate categorically!, Mitigating covert channels based on analysis of the potential for communication, Observations in using parallel and sequential evolutionary algorithms for automatic software testing, Alternating states for dual nondeterminism in imperative programming, Refinement algebra for probabilistic programs, A new taxonomy of sublinear right-to-left scanning keyword pattern matching algorithms, Fifty years of Hoare's logic, A general technique for proving lock-freedom, Formalizing Single-Assignment Program Verification: An Adaptation-Complete Approach, On integrating confidentiality and functionality in a formal method, Correctness of high-level transformation systems relative to nested conditions, The sliding-window protocol revisited, Structured calculational proof, Eliminating the substitution axiom from UNITY logic, Joining specification statements, Local proofs for global safety properties, Fixpoint semantics and simulation, Composing leads-to properties, A generalization of Naundorf's fixpoint theorem, Stabilization and blocking in state feedback control of discrete event systems, Formalization of universal algebra in Agda, Syntax-based synthesis for temporal-safety supervision, A theory for execution-time derivation in real-time programs, Mechanizing some advanced refinement concepts, Building Verification Condition Generators by Compositional Extension, Nondeterminacy and recursion via stacks and games, 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 lattice of data refinement, Regular algebra applied to language problems