Guarded commands, nondeterminacy and formal derivation of programs

DOI10.1145/360933.360975zbMATH Open0308.68017DBLPjournals/cacm/Dijkstra75OpenAlexW2066210260WikidataQ55878911 ScholiaQ55878911MaRDI QIDQ4066568FDOQ4066568

Cited In (only showing first 100 items - show all)

A wide-spectrum language for verification of programs on weak memory models
A survey of concurrent object-oriented languages
Probabilistic termination versus fair termination
A model for synchronous switching circuits and its theory of correctness
Complete proof rules for strong fairness and strong extreme fairness
\(L\)-fuzzy strongest postcondition predicate transformers as \(L\)-idempotent linear or affine operators between semimodules of monotonic predicates
Mitigating covert channels based on analysis of the potential for communication
A theory for the derivation of combination C-mos circuit designs
Defining conditional independence using collapses
An abstract interpretation-based model for safety semantics
Proving the correctness of regular deterministic programs: A unifying survey using dynamic logic
A shared memory algorithm and proof for the generalized alternative construct in CSP
Compiling quantum programs
The essence of higher-order concurrent separation logic
A self-modifiable approach to scheduling and mapping algorithms in multiprocessor systems
Kleene under a modal demonic star
A relation-algebraic approach to multirelations and predicate transformers
Exits in the refinement calculus
Quantitative analysis under fairness constraints
Recounting the Rationals: Twice!
Quantum programming with mixed states
Transforming semantics by abstract interpretation
The weakest prespecification
Observable behavior of dynamic systems: component reasoning for concurrent objects
Programs as partial graphs. I: Flow equivalence and correctness
Propositional dynamic logic of regular programs
Iris from the ground up: a modular foundation for higher-order concurrent separation logic
Relation-algebraic semantics
Refinement-oriented models of Stateflow charts
Weakest preconditions for pure Prolog programs
Developments in concurrent Kleene algebra
Formal correctness proofs of a nondeterministic program
Formalisms for specifying Markovian population models
Stochastic dynamic programming with factored representations
Process algebra and conditional composition
An elementary and unified approach to program correctness
Command-based importance sampling for statistical model checking
Appraising fairness in languages for distributed programming
A unified approach for studying the properties of transition systems
On termination problems for finitely interpreted ALGOL-like programs
Operational semantics of Framed Tempura
Constructive design of a hierarchy of semantics of a transition system by abstract interpretation
A fixpoint theory for non-monotonic parallelism
Credible autocoding of convex optimization algorithms
Knowledge forgetting in propositional \(\mu\)-calculus
Ten years of Hoare's logic: A survey. II: Nondeterminism
Inferring sufficient conditions with backward polyhedral under-approximations
Proving partial order properties
Deriving Real-Time Action Systems Controllers from Multiscale System Specifications
Verification and falsification of programs with loops using predicate abstraction
Semigroup actions on posets and preimage quasi-orders
LCTD: test-guided proofs for C programs on LLVM
A brief history of process algebra
Hoare's logic for nondeterministic regular programs: A nonstandard approach
Normal form approach to compiler design
On Euclid's algorithm and elementary number theory
Automatic distributed code generation from formal models of asynchronous processes interacting by multiway rendezvous
A verification framework for agent programming with declarative goals
Modular verification of multithreaded programs
A simple relation between relational and predicate transformer semantics for nondeterministic programs
Title not available (Why is that?)
Trace, failure and testing equivalences for communicating processes
Applicability conditions for plans with loops: computability results and algorithms
Formalisms for Specifying Markovian Population Models
Multiple Viewpoint Contract-Based Specification and Design
The algebra of multirelations
Creol: A type-safe object-oriented model for distributed concurrent systems
Deadlock analysis in networks of communicating processes
Nondeterministic three-valued logic: isotonic and guarded truth-functions
The axiomatic semantics of programs based on Hoare's logic
Adaptive broadcast by fault-tolerant spanning tree switching
From algebra to operational semantics
Computing Preconditions and Postconditions of While Loops
Hoare type theory, polymorphism and separation
Secure Microkernels, State Monads and Scalable Refinement
Formalizing Dijkstra's predicate transformer wp in weak second-order logic
Remarks on 'Program proving: Jumps and functions' by M. Clint and C.A.R. Hoare
Semigroups with if-then-else and halting programs
Comments on Morris's starvation-free solution to the mutual exclusion problem
Language design methods based on semantic principles
Symbolic model checking of timed guarded commands using difference decision diagrams
Process algebra with four-valued logic
Combining relational calculus and the Dijkstra-Gries method for deriving relational programs
A complete rule for equifair termination
Action systems in incremental and aspect-oriented modeling
Flexible Correct-by-Construction Programming
Verifying Whiley programs with Boogie
Test generation from event system abstractions to cover their states and transitions
An optimal self-stabilizing strarvation-free alternator
Phrase structures, non-determinism and backtracking
Constructive polychronous systems
The refinement calculus of reactive systems
An evaluation of interaction paradigms for active objects
Domain and range for angelic and demonic compositions
Automated Algebraic Reasoning for Collections and Local Variables with Lenses
Secure guarded commands
Abstract program slicing: an abstract interpretation-based approach to program slicing
A proof system for distributed processes
Refinement to certify abstract interpretations: illustrated on linearization for polyhedra
Verification of distributed programs using representative interleaving sequences

This page was built for publication: Guarded commands, nondeterminacy and formal derivation of programs

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4066568)