Refinement Calculus
From MaRDI portal
Publication:4396958
DOI10.1007/978-1-4612-1674-2zbMATH Open0949.68094OpenAlexW4253748132MaRDI QIDQ4396958FDOQ4396958
Authors: Ralph-Johan Back, Joakim von Wright 
Publication date: 21 June 1998
Full work available at URL: https://doi.org/10.1007/978-1-4612-1674-2
Recommendations
General topics in the theory of software (68N01) Introductory exposition (textbooks, tutorial papers, etc.) pertaining to computer science (68-01) Semantics in the theory of computing (68Q55) Introductory exposition (textbooks, tutorial papers, etc.) pertaining to mathematical logic and foundations (03-01)
Cited In (only showing first 100 items - show all)
- Specification and refinement of mobile systems in MTLA and mobile UML
- A wide-spectrum language for verification of programs on weak memory models
- Formal verification of an executable LTL model checker with partial order reduction
- Modelling and analysing neural networks using a hybrid process algebra
- Predicate transformer semantics for hybrid systems. Verification components for Isabelle/HOL
- Splitting atoms safely
- Multirelations with infinite computations
- Title not available (Why is that?)
- Dual choice and iteration in an abstract algebra of action
- Automating Induction with an SMT Solver
- Continuous functions on final coalgebras
- Alternating states for dual nondeterminism in imperative programming
- Kleene under a modal demonic star
- Algebra of monotonic Boolean transformers
- Normal forms in total correctness for while programs and action systems
- A relation-algebraic approach to multirelations and predicate transformers
- Soundness of data refinement for a higher-order imperative language
- Balancing expressiveness in formal approaches to concurrency
- Concurrent dynamic algebra
- Taming multirelations
- Title not available (Why is that?)
- Frame rule for mutually recursive procedures manipulating pointers
- The specification logic \(\nu \)Z
- Verification conditions are code
- Compositional noninterference from first principles
- Invariant diagrams with data refinement
- Connectors as designs: modeling, refinement and test case generation
- Developments in concurrent Kleene algebra
- Algebraic separation logic
- Using probabilistic Kleene algebra pKA for protocol verification
- Derivation of concurrent programs by stepwise scheduling of Event-B models
- Imperative abstractions for functional actions
- An algebraic approach to the design of compilers for object-oriented languages
- A calculus of refinements for program derivations
- Enabledness and termination in refinement algebra
- An analysis of refinement in an abortive paradigm
- Deriving Real-Time Action Systems Controllers from Multiscale System Specifications
- Formal communication elimination and sequentialization equivalence proofs for distributed system models
- Reasoning about orchestrations of web services using partial correctness
- Title not available (Why is that?)
- Generalised rely-guarantee concurrency: an algebraic foundation
- Patterns for refinement automation
- Structured calculational proof
- Refinement algebra for probabilistic programs
- Knowledge and Games in Modal Semirings
- Integrating stochastic reasoning into Event-B development
- A formal model of real-time program compilation
- Exploring an interface model for CKA
- A program construction and verification tool for separation logic
- The behavioural semantics of Event-B refinement
- A programming model for BSP with partitioned synchronisation
- rCOS: a refinement calculus of object systems
- Types and invariants in the refinement calculus
- Generic models of the laws of programming
- Multiple Viewpoint Contract-Based Specification and Design
- The algebra of multirelations
- Hybrid action systems
- Algebraic reasoning for probabilistic action systems and while-loops
- Modelling higher-order dual nondeterminacy
- Differential Hoare Logics and Refinement Calculi for Hybrid Systems with Isabelle/HOL
- An algebraic approach to multirelations and their properties
- Data refinement of invariant based programs
- Formalizing the Edmonds-Karp algorithm
- On the Purpose of Event-B Proof Obligations
- Formalizing network flow algorithms: a refinement approach in Isabelle/HOL
- An axiomatic approach to existence and liveness for differential equations
- Investigating the limits of rely/guarantee relations based on a concurrent garbage collector example
- Annotation inference for modular checkers
- Calculating sharp adaptation rules.
- The laws of programming unify process calculi
- The refinement calculus of reactive systems
- Kleisli, Parikh and Peleg compositions and liftings for multirelations
- A theory for execution-time derivation in real-time programs
- Refinement to imperative HOL
- On the relation between concurrent separation logic and concurrent Kleene algebra
- Evolution of rule-based programs
- Laws of programming for references
- Conditions of contracts for separating responsibilities in heterogeneous systems
- Unifying theories of reactive design contracts
- Efficient verified (UN)SAT certificate checking
- Assumption propagation through annotated programs
- An algebraic approach to refinement with fair choice
- Angelicism in the theory of reactive processes
- Refinement and verification in component-based model-driven design
- Angelic processes for CSP via the UTP
- Don't care non-determinism in logic program refinement
- Combining top-down and bottom-up techniques in program derivation
- Mechanical synthesis of sorting algorithms for binary trees by logic and combinatorial techniques
- The weakest specifunction
- A synchronous program algebra: a basis for reasoning about shared-memory and event-based concurrency
- Integrating formal specifications into applications: the ProB Java API
- Bridging arrays and ADTs in recursive proofs
- Towards an algebra for real-time programs
- A verified ODE solver and the Lorenz attractor
- Information Flow Control-by-Construction for an Object-Oriented Language
- On the design of correct and optimal dynamical systems and games
- Verification-Led Smart Contracts
- Contracts, games, and refinement.
- Full abstraction at package boundaries of object-oriented languages
- Traits: correctness-by-construction for free
This page was built for publication: Refinement Calculus
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4396958)
