scientific article

Publication date: 1980

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

program semantics program verification program correctness program proving

Specification and verification (program logics, model checking, etc.) (68Q60) Research exposition (monographs, survey articles) pertaining to computer science (68-02)

Related Items (82)

Semantics of plan revision in intelligent agents ⋮ Extending separation logic with fixpoints and postponed substitution ⋮ Process algebra with guards: Combining hoare logic with process algebra ⋮ Correctness of fixpoint transformations ⋮ Merging regular processes by means of fixed-point theory ⋮ Reasoning about dynamically evolving process structures ⋮ De Bakker-Zucker processes revisited ⋮ Infinite streams and finite observations in the semantics of uniform concurrency ⋮ The weakest precondition calculus: Recursion and duality ⋮ Linear time and branching time semantics for recursion with merge ⋮ Relation-algebraic semantics ⋮ Recursive programs and denotational semantics in absolute logics of programs ⋮ The inheritance of dynamic and deontic integrity constraints or: Does the boss have more rights? ⋮ Applications of compactness in the Smyth powerdomain of streams ⋮ Full abstraction and recursion ⋮ Parallel constructions of maximal path sets and applications to short superstrings ⋮ Full abstraction for the second order subset of an Algol-like language ⋮ Interpretations of recursion under unbounded nondeterminacy ⋮ Hiding in stream semantics of uniform concurrency ⋮ The \(\mu\)-calculus as an assertion-language for fairness arguments ⋮ Specifying termination in CSP ⋮ On correct refinement of programs ⋮ Verification of object-oriented programs: a transformational approach ⋮ Command algebras, recursion and program transformation ⋮ Floyd's principle, correctness theories and program equivalence ⋮ Proving total correctness of recursive procedures ⋮ Semantical analysis of specification logic ⋮ A dual problem to least fixed points ⋮ Linear dependent types in a call-by-value scenario ⋮ Some natural structures which fail to possess a sound and decidable Hoare-like logic for their while-programs ⋮ On the completeness of modular proof systems ⋮ A first order logic for partial functions ⋮ Proof obligations for blocks and procedures ⋮ A specification structure for deadlock-freedom of synchronous processes ⋮ Fixed point theorems and semantics: A folk tale ⋮ Hoare's logic and Peano's arithmetic ⋮ A continuous semantics for unbounded nondeterminism ⋮ A mechanical analysis of program verification strategies ⋮ Domain theory in logical form ⋮ Process expressions and Hoare's logic: Showing and irreconcilability of context-free recursion with Scott's induction rule ⋮ Correctness and efficiency of pattern matching algorithms ⋮ The contraction principle as a particular case of Kleene's fixed point theorem ⋮ Completeness of ASM Refinement ⋮ A compositional axiomatization of statecharts ⋮ Formal semantics for mutual belief ⋮ Combining angels, demons and miracles in program specifications ⋮ Alternating states for dual nondeterminism in imperative programming ⋮ The axiomatization of override and update ⋮ ASM refinement and generalizations of forward simulation in data refinement: a comparison ⋮ A note on Coinduction and Weak Bisimilarity for While Programs ⋮ An axiomatic treatment of SIMD assignment ⋮ Fifty years of Hoare's logic ⋮ A Hoare logic for dynamic networks of asynchronously communicating deterministic processes ⋮ Dual unbounded nondeterminacy, recursion, and fixpoints ⋮ Relational Semantics Revisited ⋮ Hoare's logic and VDM ⋮ A fixed point approach to parallel discrete event simulation ⋮ Wythoff games, continued fractions, cedar trees and Fibonacci searches ⋮ Completeness of Hoare-calculi revisited ⋮ On the notion of expressiveness and the rule of adaptation ⋮ A weakest precondition semantics for communicating processes ⋮ Proving program inclusion using Hoare's logic ⋮ On infinite computations in denotational semantics ⋮ Programs as proofs: A synopsis ⋮ Correctness of programs with Pascal-like procedures without global variables ⋮ An algebraic approach to the syntax and semantics of languages with subscripted variables ⋮ Two theorems about the completeness of Hoare's logic ⋮ Hoare's logic for programming languages with two data types ⋮ Ten years of Hoare's logic: A survey. II: Nondeterminism ⋮ Average case optimality for linear problems ⋮ Expressiveness and the completeness of Hoare's logic ⋮ Specification-oriented semantics for communicating processes ⋮ The axiomatic semantics of programs based on Hoare's logic ⋮ Equivalences among logics of programs ⋮ Results on the propositional \(\mu\)-calculus ⋮ Rendez-vous with metric semantics ⋮ Combinatory reduction systems: Introduction and survey ⋮ A type-theoretical alternative to ISWIM, CUCH, OWHY ⋮ Weakly expressive models for Hoare logic ⋮ Closure functions and general iterates as reflectors ⋮ The generic approximation lemma ⋮ Proving partial order properties

This page was built for publication: