Refinement Calculus
From MaRDI portal
Publication:4396958
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)
Recommendations
Cited in
(only showing first 100 items - show all)- Specification and refinement of mobile systems in MTLA and mobile UML
- Hidden-Markov program algebra with iteration
- An axiomatic approach to existence and liveness for differential equations
- A wide-spectrum language for verification of programs on weak memory models
- Formal verification of an executable LTL model checker with partial order reduction
- Investigating the limits of rely/guarantee relations based on a concurrent garbage collector example
- Modelling and analysing neural networks using a hybrid process algebra
- Predicate transformer semantics for hybrid systems. Verification components for Isabelle/HOL
- Flexible Correct-by-Construction Programming
- Annotation inference for modular checkers
- Calculating sharp adaptation rules.
- Bunch theory: axioms, logic, applications and model
- Splitting atoms safely
- Multirelations with infinite computations
- The laws of programming unify process calculi
- The refinement calculus of reactive systems
- Kleisli, Parikh and Peleg compositions and liftings for multirelations
- Dual choice and iteration in an abstract algebra of action
- scientific article; zbMATH DE number 194642 (Why is no real title available?)
- 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
- Automating Induction with an SMT Solver
- A theory for execution-time derivation in real-time programs
- Refinement to imperative HOL
- Alternating states for dual nondeterminism in imperative programming
- Continuous functions on final coalgebras
- On the relation between concurrent separation logic and concurrent Kleene algebra
- Kleene under a modal demonic star
- Normal forms in total correctness for while programs and action systems
- Evolution of rule-based programs
- Balancing expressiveness in formal approaches to concurrency
- Algebra of monotonic Boolean transformers
- Laws of programming for references
- Soundness of data refinement for a higher-order imperative language
- A relation-algebraic approach to multirelations and predicate transformers
- Conditions of contracts for separating responsibilities in heterogeneous systems
- Unifying theories of reactive design contracts
- Frame rule for mutually recursive procedures manipulating pointers
- The specification logic \(\nu \)Z
- Verification conditions are code
- Concurrent dynamic algebra
- Taming multirelations
- scientific article; zbMATH DE number 1512629 (Why is no real title available?)
- Efficient verified (UN)SAT certificate checking
- Compositional noninterference from first principles
- Invariant diagrams with data refinement
- Connectors as designs: modeling, refinement and test case generation
- Assumption propagation through annotated programs
- A Multi-level Refinement Approach for Structural Synthesis of Optimal Probabilistic Models
- Developments in concurrent Kleene algebra
- Refinement and verification in component-based model-driven design
- Angelicism in the theory of reactive processes
- An algebraic approach to refinement with fair choice
- Angelic processes for CSP via the UTP
- Don't care non-determinism in logic program refinement
- Algebraic separation logic
- Mechanical synthesis of sorting algorithms for binary trees by logic and combinatorial techniques
- Combining top-down and bottom-up techniques in program derivation
- 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
- The weakest specifunction
- Integrating formal specifications into applications: the ProB Java API
- A synchronous program algebra: a basis for reasoning about shared-memory and event-based concurrency
- Enabledness and termination in refinement algebra
- Bridging arrays and ADTs in recursive proofs
- An analysis of refinement in an abortive paradigm
- Towards an algebra for real-time programs
- Relation-algebraic verification of disjoint-set forests
- A verified ODE solver and the Lorenz attractor
- A Practical Single Refinement Method for B
- Formal communication elimination and sequentialization equivalence proofs for distributed system models
- Reasoning about orchestrations of web services using partial correctness
- Information Flow Control-by-Construction for an Object-Oriented Language
- On the design of correct and optimal dynamical systems and games
- Deriving Real-Time Action Systems Controllers from Multiscale System Specifications
- Contracts, games, and refinement.
- Generalised rely-guarantee concurrency: an algebraic foundation
- Structured calculational proof
- Refinement algebra for probabilistic programs
- Patterns for refinement automation
- scientific article; zbMATH DE number 517333 (Why is no real title available?)
- Verification-Led Smart Contracts
- Knowledge and Games in Modal Semirings
- Full abstraction at package boundaries of object-oriented languages
- Traits: correctness-by-construction for free
- Integrating stochastic reasoning into Event-B development
- A formal model of real-time program compilation
- Unifying theories of programming in Isabelle
- Programming interfaces and basic topology
- Exploring an interface model for CKA
- A program construction and verification tool for separation logic
- The behavioural semantics of Event-B refinement
- Safe Modification of Pointer Programs in Refinement Calculus
- A programming model for BSP with partitioned synchronisation
- Relating computer systems to sequence diagrams: the impact of underspecification and inherent nondeterminism
- rCOS: a refinement calculus of object systems
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)
