Guarded commands, nondeterminacy and formal derivation of programs

DOI10.1145/360933.360975zbMath0308.68017WikidataQ55878911 ScholiaQ55878911MaRDI QIDQ4066568

Publication date: 1975

Published in: Communications of the ACM (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1145/360933.360975

Mathematics Subject Classification ID

68N01: General topics in the theory of software

Related Items

Process algebra with four-valued logic, AXIOMATIC FRAMEWORKS FOR DEVELOPING BSP-STYLE PROGRAMS∗, Unnamed Item, A self-modifiable approach to scheduling and mapping algorithms in multiprocessor systems, Explicit Fair Scheduling for Dynamic Control, SEMIGROUPS WITH if–then–else AND HALTING PROGRAMS, Modular verification of multithreaded programs, Transforming semantics by abstract interpretation, Formal correctness proofs of a nondeterministic program, Formalizing Dijkstra's predicate transformer wp in weak second-order logic, A model for synchronous switching circuits and its theory of correctness, Complete proof rules for strong fairness and strong extreme fairness, Nondeterministic three-valued logic: isotonic and guarded truth-functions, The axiomatic semantics of programs based on Hoare's logic, A theory for the derivation of combination C-mos circuit designs, Kleene under a modal demonic star, Creol: A type-safe object-oriented model for distributed concurrent systems, Branching versus linear logics yet again, Transforming generate-and-test programs to execute under committed-choice AND-parallelism, Automatic generation of path conditions for concurrent timed systems, Verification and falsification of programs with loops using predicate abstraction, Alternating states for dual nondeterminism in imperative programming, Ten years of Hoare's logic: A survey. II: Nondeterminism, Dataflow computing and Eager and Lazy evaluations, Comments on Morris's starvation-free solution to the mutual exclusion problem, A complete rule for equifair termination, The weakest prespecification, A shared memory algorithm and proof for the generalized alternative construct in CSP, Trace, failure and testing equivalences for communicating processes, A proof system for distributed processes, Appraising fairness in languages for distributed programming, Proving the correctness of regular deterministic programs: A unifying survey using dynamic logic, On the total correctness of nondeterministic programs, A simple relation between relational and predicate transformer semantics for nondeterministic programs, On termination problems for finitely interpreted ALGOL-like programs, A unified approach for studying the properties of transition systems, Programs as partial graphs. I: Flow equivalence and correctness, Axiomatic semantics for escape statements, Defining conditional independence using collapses, Verification of distributed programs using representative interleaving sequences, Semantic models for total correctness and fairness, From algebra to operational semantics, Language design methods based on semantic principles, Remarks on 'Program proving: Jumps and functions' by M. Clint and C.A.R. Hoare, Phrase structures, non-determinism and backtracking, A contribution to the programming calculus, Propositional dynamic logic of regular programs, Verifiable properties of database transactions, Proving partial order properties, Normal form approach to compiler design, Models for reactivity, Axiomatic-like performance analysis (ALPA), Relation-algebraic semantics, Parallel constructions of maximal path sets and applications to short superstrings, A methodology for designing proof rules for fair parallel programs, Stochastic dynamic programming with factored representations, Constructive design of a hierarchy of semantics of a transition system by abstract interpretation, Process algebra and conditional composition, A brief history of process algebra, Exits in the refinement calculus, Hoare's logic for nondeterministic regular programs: A nonstandard approach, Probabilistic termination versus fair termination, Symbolic model checking of timed guarded commands using difference decision diagrams, A fixpoint theory for non-monotonic parallelism, Predicate transformers as power operations, Combining relational calculus and the Dijkstra-Gries method for deriving relational programs, Smart office robot collaboration based on multi-agent programming, Verifiable agent dialogues, A verification framework for agent programming with declarative goals, Operational semantics of Framed Tempura, The weakest specifunction, Compiling quantum programs, An optimal self-stabilizing strarvation-free alternator, Deadlock analysis in networks of communicating processes, Recounting the Rationals: Twice!, Secure Microkernels, State Monads and Scalable Refinement, Hoare type theory, polymorphism and separation, Multiple Viewpoint Contract-Based Specification and Design, Formalisms for Specifying Markovian Population Models, Quantitative Analysis under Fairness Constraints, Some Variants of the Weakest Precondition in Nondeterminism, Unnamed Item, Programming with generators, Church-Rosser converters, THE Σλ-CALCULUS AND DERIVED PROGRAM FORMS