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)- Abstractions of non-interference security: probabilistic versus possibilistic
- Designing a semantic model for a wide-spectrum language with concurrency
- Effect polymorphism in higher-order logic (proof pearl)
- Types and invariants in the refinement calculus
- IsaVODEs: Interactive verification of cyber-physical systems at scale
- Computer-aided development of a real-time program
- Generic models of the laws of programming
- Algebra for quantitative information flow
- Multiple Viewpoint Contract-Based Specification and Design
- Building Specifications in the Event-B Institution
- A refinement methodology for object-oriented programs
- Intuitionistic Refinement Calculus
- The algebra of multirelations
- On hierarchically developing reactive systems
- Hybrid action systems
- Algebraic reasoning for probabilistic action systems and while-loops
- Modelling higher-order dual nondeterminacy
- 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
- UTP, \textsf{\textit{Circus}}, and Isabelle
- An algebraic approach to multirelations and their properties
- Synthesis of strategies using the Hoare logic of angelic and demonic nondeterminism
- Program algebra for quantitative information flow
- Differential Hoare Logics and Refinement Calculi for Hybrid Systems with Isabelle/HOL
- Formalizing the Edmonds-Karp algorithm
- Data refinement of invariant based programs
- Formalizing network flow algorithms: a refinement approach in Isabelle/HOL
- Automated verification of reactive and concurrent programs by calculation
- On the Purpose of Event-B Proof Obligations
- Unifying Semantics for Concurrent Programming
- 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
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)
