Guarded commands, nondeterminacy and formal derivation of programs
From MaRDI portal
Publication:4066568
DOI10.1145/360933.360975zbMath0308.68017OpenAlexW2066210260WikidataQ55878911 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
Related Items
Abstract Program Slicing, Indexed and fibered structures for partial and total correctness assertions, A predicative semantics for the refinement of real-time systems, Assumption propagation through annotated programs, Fairness for Infinitary Control, THE Σλ-CALCULUS AND DERIVED PROGRAM FORMS, Compositional Reasoning, Combining Model Checking and Testing, Constructive Polychronous Systems, Deriving Real-Time Action Systems Controllers from Multiscale System Specifications, Some Variants of the Weakest Precondition in Nondeterminism, Deadlock analysis in networks of communicating processes, Trusting computations: a mechanized proof from partial differential equations to actual program, Axioms for signatures with domain and demonic composition, A Relation-Algebraic Approach to Multirelations and Predicate Transformers, The refinement calculus of reactive systems, Automated Algebraic Reasoning for Collections and Local Variables with Lenses, Unnamed Item, Data Centric Workflows for Crowdsourcing, Knowledge forgetting in propositional \(\mu\)-calculus, A genetically modified Hoare logic, Programming with generators, Embedded domain specific verifiers, Flexible Correct-by-Construction Programming, What else is undecidable about loops?, \textsf{HHLPy}: practical verification of hybrid systems using Hoare logic, On the Introduction of Guarded Lists in Bach: Expressiveness, Correctness, and Efficiency Issues, Computing sufficient and necessary conditions in CTL: a forgetting approach, Automated reasoning for probabilistic sequential programs with theorem proving, A self-modifiable approach to scheduling and mapping algorithms in multiprocessor systems, Recounting the Rationals: Twice!, Unnamed Item, Synthesis of Strategies Using the Hoare Logic of Angelic and Demonic Nondeterminism, Iris from the ground up: A modular foundation for higher-order concurrent separation logic, The Essence of Higher-Order Concurrent Separation Logic, Action systems in incremental and aspect-oriented modeling, Secure Microkernels, State Monads and Scalable Refinement, An automatic method for the dynamic construction of abstractions of states of a formal model, Hoare type theory, polymorphism and separation, An abstract interpretation-based model for safety semantics, Secure Guarded Commands, ADAPTIVE DISTRIBUTED MUTUAL EXCLUSION BY DYNAMIC TOPOLOGY SWITCHING, A High-Level Language for Modeling Algorithms and Their Properties, Semantic models for total correctness and fairness, Programmed graph transformations and graph transformation units in GRACE, Association of Under-Approximation Techniques for Generating Tests from Models, FORMALISMS FOR SPECIFYING MARKOVIAN POPULATION MODELS, Inferring Sufficient Conditions with Backward Polyhedral Under-Approximations, The weakest specifunction, Compiling quantum programs, The algebra of multirelations, Combining Top-Down and Bottom-Up Techniques in Program Derivation, Explicit Fair Scheduling for Dynamic Control, A survey of concurrent object-oriented languages, Multiple Viewpoint Contract-Based Specification and Design, ON FORMAL AND COGNITIVE SEMANTICS FOR SEMANTIC COMPUTING, Dynamic Frames in Java Dynamic Logic, Precondition Inference from Intermittent Assertions and Application to Contracts on Collections, Process algebra with four-valued logic, Weakest preconditions in fibrations, Church-Rosser converters, Formalisms for Specifying Markovian Population Models, Quantitative Analysis under Fairness Constraints, Modelling declassification policies using abstract domain completeness, Computing Preconditions and Postconditions of While Loops, Defining Actions in Concurrent Declarative Programming, Set-Theoretic Models of Computations, AXIOMATIC FRAMEWORKS FOR DEVELOPING BSP-STYLE PROGRAMS∗, SEMIGROUPS WITH if–then–else AND HALTING PROGRAMS, An optimal self-stabilizing strarvation-free alternator, Quantum Programming With Mixed States, Observable Behavior of Dynamic Systems: Component Reasoning for Concurrent Objects, Credible autocoding of convex optimization algorithms, Dataflow computing and Eager and Lazy evaluations, On distributability, Comments on Morris's starvation-free solution to the mutual exclusion problem, A fixpoint theory for non-monotonic parallelism, Weakest preconditions in fibrations, A complete rule for equifair termination, Weakest preconditions for pure Prolog programs, Verifiable agent dialogues, A verification framework for agent programming with declarative goals, Developments in concurrent Kleene algebra, The weakest prespecification, Operational semantics of Framed Tempura, Command-based importance sampling for statistical model checking, Relation-algebraic semantics, A shared memory algorithm and proof for the generalized alternative construct in CSP, Predicate transformers as power operations, Creol: A type-safe object-oriented model for distributed concurrent systems, Trace, failure and testing equivalences for communicating processes, Benign interaction of security domains, A proof system for distributed processes, Automating regression verification of pointer programs by predicate abstraction, Parallel actor monitors: disentangling task-level parallelism from data partitioning in the actor model, LCTD: test-guided proofs for C programs on LLVM, Parallel constructions of maximal path sets and applications to short superstrings, Appraising fairness in languages for distributed programming, Empowering the Event-B method using external theories, Formal correctness proofs of a nondeterministic program, Applicability conditions for plans with loops: computability results and algorithms, A methodology for designing proof rules for fair parallel programs, An elementary and unified approach to program correctness, Revisiting sequential composition in process calculi, Proving the correctness of regular deterministic programs: A unifying survey using dynamic logic, On the total correctness of nondeterministic programs, Semigroup actions on posets and preimage quasi-orders, On Euclid's algorithm and elementary number theory, Refinement-oriented models of Stateflow charts, A simple relation between relational and predicate transformer semantics for nondeterministic programs, Branching versus linear logics yet again, Transforming generate-and-test programs to execute under committed-choice AND-parallelism, On termination problems for finitely interpreted ALGOL-like programs, A unified approach for studying the properties of transition systems, Combining relational calculus and the Dijkstra-Gries method for deriving relational programs, Region analysis for deductive verification of C programs, Test generation from event system abstractions to cover their states and transitions, Programs as partial graphs. I: Flow equivalence and correctness, Domain and range for angelic and demonic compositions, An evaluation of interaction paradigms for active objects, Axiomatic semantics for escape statements, Adaptive broadcast by fault-tolerant spanning tree switching, Smart office robot collaboration based on multi-agent programming, Refinement to certify abstract interpretations: illustrated on linearization for polyhedra, Formalizing Dijkstra's predicate transformer wp in weak second-order logic, Conditions of contracts for separating responsibilities in heterogeneous systems, Automatic generation of path conditions for concurrent timed systems, Defining conditional independence using collapses, Automatic distributed code generation from formal models of asynchronous processes interacting by multiway rendezvous, A model for synchronous switching circuits and its theory of correctness, Complete proof rules for strong fairness and strong extreme fairness, Verification of distributed programs using representative interleaving sequences, \(L\)-fuzzy strongest postcondition predicate transformers as \(L\)-idempotent linear or affine operators between semimodules of monotonic predicates, Angelic processes for CSP via the UTP, Mitigating covert channels based on analysis of the potential for communication, Semantic models for total correctness and fairness, From algebra to operational semantics, Verification and falsification of programs with loops using predicate abstraction, Unifying theories of reactive design contracts, Alternating states for dual nondeterminism in imperative programming, Modular verification of multithreaded programs, Transforming semantics by abstract interpretation, Language design methods based on semantic principles, Remarks on 'Program proving: Jumps and functions' by M. Clint and C.A.R. Hoare, A wide-spectrum language for verification of programs on weak memory models, A brief history of process algebra, Fifty years of Hoare's logic, Phrase structures, non-determinism and backtracking, A contribution to the programming calculus, Automated verification of reactive and concurrent programs by calculation, Propositional dynamic logic of regular programs, Exits in the refinement calculus, Integration of formal proof into unified assurance cases with Isabelle/SACM, Hoare's logic for nondeterministic regular programs: A nonstandard approach, Probabilistic termination versus fair termination, Verifiable properties of database transactions, Moment-based analysis of Bayesian network properties, Stochastic dynamic programming with factored representations, Nondeterministic three-valued logic: isotonic and guarded truth-functions, Ten years of Hoare's logic: A survey. II: Nondeterminism, BGSL: an imperative language for specification and refinement of backtracking programs, The axiomatic semantics of programs based on Hoare's logic, Verifying Whiley programs with Boogie, Symbolic model checking of timed guarded commands using difference decision diagrams, A theory for the derivation of combination C-mos circuit designs, Constructive design of a hierarchy of semantics of a transition system by abstract interpretation, Process algebra and conditional composition, Proving partial order properties, Normal form approach to compiler design, Models for reactivity, Axiomatic-like performance analysis (ALPA), Kleene under a modal demonic star
