Guarded commands, nondeterminacy and formal derivation of programs

Cited in

(only showing first 100 items - show all)

Symbolic model checking of timed guarded commands using difference decision diagrams
Semigroups with if-then-else and halting programs
A wide-spectrum language for verification of programs on weak memory models
A complete rule for equifair termination
Combining relational calculus and the Dijkstra-Gries method for deriving relational programs
Process algebra with four-valued logic
A survey of concurrent object-oriented languages
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
Probabilistic termination versus fair termination
Mitigating covert channels based on analysis of the potential for communication
Verifying Whiley programs with Boogie
Test generation from event system abstractions to cover their states and transitions
Action systems in incremental and aspect-oriented modeling
A theory for the derivation of combination C-mos circuit designs
An optimal self-stabilizing strarvation-free alternator
Phrase structures, non-determinism and backtracking
Flexible Correct-by-Construction Programming
Defining conditional independence using collapses
An evaluation of interaction paradigms for active objects
Domain and range for angelic and demonic compositions
The refinement calculus of reactive systems
Constructive polychronous systems
Proving the correctness of regular deterministic programs: A unifying survey using dynamic logic
An abstract interpretation-based model for safety semantics
A shared memory algorithm and proof for the generalized alternative construct in CSP
Automated Algebraic Reasoning for Collections and Local Variables with Lenses
Secure guarded commands
A proof system for distributed processes
Abstract program slicing: an abstract interpretation-based approach to program slicing
Refinement to certify abstract interpretations: illustrated on linearization for polyhedra
Verification of distributed programs using representative interleaving sequences
Alternating states for dual nondeterminism in imperative programming
Compiling quantum programs
The essence of higher-order concurrent separation logic
Kleene under a modal demonic star
A self-modifiable approach to scheduling and mapping algorithms in multiprocessor systems
A high-level language for modeling algorithms and their properties
Automated reasoning for probabilistic sequential programs with theorem proving
A relation-algebraic approach to multirelations and predicate transformers
Conditions of contracts for separating responsibilities in heterogeneous systems
Exits in the refinement calculus
Unifying theories of reactive design contracts
An automatic method for the dynamic construction of abstractions of states of a formal model
On distributability
Data centric workflows for crowdsourcing
Quantitative analysis under fairness constraints
Recounting the Rationals: Twice!
Transforming semantics by abstract interpretation
Verifiable properties of database transactions
The weakest prespecification
Programs as partial graphs. I: Flow equivalence and correctness
Quantum programming with mixed states
Axiomatic-like performance analysis (ALPA)
scientific article; zbMATH DE number 3688675 (Why is no real title available?)
Weakest preconditions in fibrations
Observable behavior of dynamic systems: component reasoning for concurrent objects
Benign interaction of security domains
Propositional dynamic logic of regular programs
Fifty years of Hoare's logic
Refinement-oriented models of Stateflow charts
THE Σλ-CALCULUS AND DERIVED PROGRAM FORMS
Relation-algebraic semantics
Assumption propagation through annotated programs
Weakest preconditions for pure Prolog programs
Developments in concurrent Kleene algebra
Predicate transformers as power operations
Programmed graph transformations and graph transformation units in GRACE
Iris from the ground up: a modular foundation for higher-order concurrent separation logic
Weakest preconditions in fibrations
Region analysis for deductive verification of C programs
Angelic processes for CSP via the UTP
Modelling declassification policies using abstract domain completeness
AXIOMATIC FRAMEWORKS FOR DEVELOPING BSP-STYLE PROGRAMS∗
Dynamic frames in Java dynamic logic
Formal correctness proofs of a nondeterministic program
Some Variants of the Weakest Precondition in Nondeterminism
Combining top-down and bottom-up techniques in program derivation
Formalisms for specifying Markovian population models
On the total correctness of nondeterministic programs
Stochastic dynamic programming with factored representations
Process algebra and conditional composition
\textsf{HHLPy}: practical verification of hybrid systems using Hoare logic
What else is undecidable about loops?
An elementary and unified approach to program correctness
Command-based importance sampling for statistical model checking
Indexed and fibered structures for partial and total correctness assertions
Combining model checking and testing
Appraising fairness in languages for distributed programming
Adaptive distributed mutual exclusion by dynamic topology switching
The weakest specifunction
A unified approach for studying the properties of transition systems
On termination problems for finitely interpreted ALGOL-like programs
A contribution to the programming calculus
Automating regression verification of pointer programs by predicate abstraction
Parallel actor monitors: disentangling task-level parallelism from data partitioning in the actor model
Operational semantics of Framed Tempura
Constructive design of a hierarchy of semantics of a transition system by abstract interpretation
A genetically modified Hoare logic

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)