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)
- 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
- Unifying theories of programming in Isabelle
- Programming interfaces and basic topology
- Safe Modification of Pointer Programs in Refinement Calculus
- Relating computer systems to sequence diagrams: the impact of underspecification and inherent nondeterminism
- Abstractions of non-interference security: probabilistic versus possibilistic
- Designing a semantic model for a wide-spectrum language with concurrency
- Computer-aided development of a real-time program
- Algebra for quantitative information flow
- Intuitionistic Refinement Calculus
- On hierarchically developing reactive systems
- Automatic refinement to efficient data structures: a comparison of two approaches
- Consistency-preserving refactoring of refinement structures in Event-B models
- Towards patterns for heaps and imperative lambdas
- Synthesis of strategies using the Hoare logic of angelic and demonic nondeterminism
- Program algebra for quantitative information flow
- Unifying Semantics for Concurrent Programming
- Automated verification of reactive and concurrent programs by calculation
- Hidden-Markov program algebra with iteration
- Flexible Correct-by-Construction Programming
- Bunch theory: axioms, logic, applications and model
- Automated Algebraic Reasoning for Collections and Local Variables with Lenses
- Verifying the Correctness of Disjoint-Set Forests with Kleene Relation Algebras
- Verified Compilation and the B Method: A Proposal and a First Appraisal
- A Multi-level Refinement Approach for Structural Synthesis of Optimal Probabilistic Models
- Relation-algebraic verification of disjoint-set forests
- A Practical Single Refinement Method for B
- Effect polymorphism in higher-order logic (proof pearl)
- IsaVODEs: Interactive verification of cyber-physical systems at scale
- Building Specifications in the Event-B Institution
- A refinement methodology for object-oriented programs
- UTP, \textsf{\textit{Circus}}, and Isabelle
- 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
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)
