Countable nondeterminism and random assignment
DOI10.1145/6490.6494zbMATH Open0627.68015OpenAlexW2014552079MaRDI QIDQ3763571FDOQ3763571
Authors: Krzysztof R. Apt, Gordon D. Plotkin
Publication date: 1986
Published in: Journal of the ACM (Search for Journal in Brave)
Full work available at URL: https://ir.cwi.nl/pub/10281
Recommendations
fairnessequivalencecontinuitynondeterminismpowerdomainsoperational semanticspredicate transformerstotal correctnesssoundness and completenessweakest precondition semanticsHoare-like proof systemrecursive theoretic complexitysmall programming languagetransformation semantics
General topics in the theory of software (68N01) Specification and verification (program logics, model checking, etc.) (68Q60)
Cited In (55)
- Liminf progress measures
- Two guarded recursive powerdomains for applicative simulation
- Verified exact real computation with nondeterministic functions and limits
- Strong fairness and full abstraction for communicating processes
- Metric semantics for concurrency
- A complete rule for equifair termination
- While-programs with nondeterministic assignments and the logic ALNA
- Foundations of Software Science and Computation Structures
- An abstract interpretation-based model for safety semantics
- Full abstraction and recursion
- A logic of recursion
- Sequential algorithms for unbounded nondeterminism
- Title not available (Why is that?)
- Alternating states for dual nondeterminism in imperative programming
- Contractions in comparing concurrency semantics
- The origins of structural operational semantics
- Soundness of data refinement for a higher-order imperative language
- Step-indexed relational reasoning for countable nondeterminism
- Merging regular processes by means of fixed-point theory
- Precise interprocedural dependence analysis of parallel programs
- A fully abstract semantics for concurrent constraint programming
- Transforming semantics by abstract interpretation
- There is no fully abstract fixpoint semantics for non-deterministic languages with infinite computations
- Fifty years of Hoare's logic
- ``A la Burstall intermittent assertions induction principles for proving inevitability properties of programs
- Verification of concurrent programs: The automata-theoretic framework
- A relation algebraic model of robust correctness
- A calculus of refinements for program derivations
- Hiding Software Watermarks in Loop Structures
- Constructive design of a hierarchy of semantics of a transition system by abstract interpretation
- Ten years of Hoare's logic: A survey. II: Nondeterminism
- The weakest precondition calculus: Recursion and duality
- Equational reasoning about nondeterministic processes
- Completing the temporal picture
- Interpretations of recursion under unbounded nondeterminacy
- The expressive power of indeterminate dataflow primitives
- A unified rule format for bounded nondeterminism in SOS with terms as labels
- Computing polynomial program invariants
- A domain equation for bisimulation
- Nonexpressibility of fairness and signaling
- A Case Study in Abstract Interpretation Based Program Transformation
- Semantic models for total correctness and fairness
- m-Algebraic lattices in formal concept analysis
- Modelling higher-order dual nondeterminacy
- Step-indexed relational reasoning for countable nondeterminism
- Dual unbounded nondeterminacy, recursion, and fixpoints
- Comparative semantics for flow of control in logic programming without logic
- The \(\mu\)-calculus as an assertion-language for fairness arguments
- Generated models and the ω-rule: The nondeterministic case
- Comparative metric semantics for concurrent PROLOG
- On Fixpoint/Iteration/Variant Induction Principles for Proving Total Correctness of Programs with Denotational Semantics
- A methodology for designing proof rules for fair parallel programs
- Counting successes: effects and transformations for non-deterministic programs
- On the logic of UNITY
- A category-theoretic semantics for unbounded indeterminacy
This page was built for publication: Countable nondeterminism and random assignment
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3763571)