Refinement Calculus
From MaRDI portal
Introductory exposition (textbooks, tutorial papers, etc.) pertaining to mathematical logic and foundations (03-01) Introductory exposition (textbooks, tutorial papers, etc.) pertaining to computer science (68-01) General topics in the theory of software (68N01) Semantics in the theory of computing (68Q55)
Recommendations
Cited in
(only showing first 100 items - show all)- Refinement and verification in component-based model-driven design
- On the design of correct and optimal dynamical systems and games
- A calculus of refinements for program derivations
- Structured calculational proof
- Fusion and simultaneous execution in the refinement calculus
- A formal model of real-time program compilation
- Soundness of data refinement for a higher-order imperative language
- Annotation inference for modular checkers
- Calculating sharp adaptation rules.
- Mechanical synthesis of sorting algorithms for binary trees by logic and combinatorial techniques
- A verified ODE solver and the Lorenz attractor
- Designing a semantic model for a wide-spectrum language with concurrency
- Formalizing network flow algorithms: a refinement approach in Isabelle/HOL
- Refinement to imperative HOL
- Conditions of contracts for separating responsibilities in heterogeneous systems
- Angelic processes for CSP via the UTP
- Hybrid action systems
- Contracts, games, and refinement.
- Evolution of rule-based programs
- Relating computer systems to sequence diagrams: the impact of underspecification and inherent nondeterminism
- On hierarchically developing reactive systems
- An axiomatic approach to existence and liveness for differential equations
- Unifying theories of reactive design contracts
- Abstractions of non-interference security: probabilistic versus possibilistic
- A wide-spectrum language for verification of programs on weak memory models
- Automated verification of reactive and concurrent programs by calculation
- Integrating formal specifications into applications: the ProB Java API
- Traits: correctness-by-construction for free
- Bridging arrays and ADTs in recursive proofs
- Refinement algebra for probabilistic programs
- On the relation between concurrent separation logic and concurrent Kleene algebra
- Kleisli, Parikh and Peleg compositions and liftings for multirelations
- Towards patterns for heaps and imperative lambdas
- A synchronous program algebra: a basis for reasoning about shared-memory and event-based concurrency
- Automatic refinement to efficient data structures: a comparison of two approaches
- Consistency-preserving refactoring of refinement structures in Event-B models
- Investigating the limits of rely/guarantee relations based on a concurrent garbage collector example
- Program algebra for quantitative information flow
- The weakest specifunction
- Programming interfaces and basic topology
- A theory for execution-time derivation in real-time programs
- Assumption propagation through annotated programs
- Modelling and analysing neural networks using a hybrid process algebra
- The refinement calculus of reactive systems
- Continuous functions on final coalgebras
- Angelicism in the theory of reactive processes
- Formalizing the Edmonds-Karp algorithm
- Don't care non-determinism in logic program refinement
- Generic models of the laws of programming
- Automating Induction with an SMT Solver
- The laws of programming unify process calculi
- Deriving Real-Time Action Systems Controllers from Multiscale System Specifications
- Towards an algebra for real-time programs
- Laws of programming for references
- Exploring an interface model for CKA
- A relation-algebraic approach to multirelations and predicate transformers
- A program construction and verification tool for separation logic
- Unifying theories of programming in Isabelle
- Synthesis of strategies using the Hoare logic of angelic and demonic nondeterminism
- Developments in concurrent Kleene algebra
- Data refinement of invariant based programs
- Patterns for refinement automation
- A refinement methodology for object-oriented programs
- Full abstraction at package boundaries of object-oriented languages
- Algebra of monotonic Boolean transformers
- Generalised rely-guarantee concurrency: an algebraic foundation
- Knowledge and Games in Modal Semirings
- Safe Modification of Pointer Programs in Refinement Calculus
- On the Purpose of Event-B Proof Obligations
- A Practical Single Refinement Method for B
- Multiple Viewpoint Contract-Based Specification and Design
- Intuitionistic Refinement Calculus
- Multirelations with infinite computations
- scientific article; zbMATH DE number 517333 (Why is no real title available?)
- Invariant diagrams with data refinement
- Compositional noninterference from first principles
- Connectors as designs: modeling, refinement and test case generation
- scientific article; zbMATH DE number 1512629 (Why is no real title available?)
- Formal communication elimination and sequentialization equivalence proofs for distributed system models
- scientific article; zbMATH DE number 194642 (Why is no real title available?)
- Reasoning about orchestrations of web services using partial correctness
- Data Refinement
- Computer-aided development of a real-time program
- Unifying Semantics for Concurrent Programming
- The algebra of multirelations
- A Multi-level Refinement Approach for Structural Synthesis of Optimal Probabilistic Models
- Building Specifications in the Event-B Institution
- Automated Algebraic Reasoning for Collections and Local Variables with Lenses
- Verifying the Correctness of Disjoint-Set Forests with Kleene Relation Algebras
- Differential Hoare Logics and Refinement Calculi for Hybrid Systems with Isabelle/HOL
- An algebraic approach to multirelations and their properties
- Verified Compilation and the B Method: A Proposal and a First Appraisal
- Concurrent dynamic algebra
- Taming multirelations
- Algebra for quantitative information flow
- An algebraic approach to refinement with fair choice
- Algebraic separation logic
- Normal forms in total correctness for while programs and action systems
- Hidden-Markov program algebra with iteration
- Combining top-down and bottom-up techniques in program derivation
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)
