scientific article; zbMATH DE number 605806
From MaRDI portal
Publication:4301161
Recommendations
- Laws of data refinement
- A theoretical basis for stepwise refinement and the programming calculus
- Designware: Software development by refinement
- scientific article; zbMATH DE number 1086636
- scientific article; zbMATH DE number 1390335
- Formal models of stepwise refinements of programs
- scientific article; zbMATH DE number 1497802
- scientific article; zbMATH DE number 3951983
- scientific article; zbMATH DE number 177527
- scientific article; zbMATH DE number 497680
Cited in
(only showing first 100 items - show all)- Refinement and verification in component-based model-driven design
- A UTP semantics for \textsf{Circus}
- Graph transformations for object-oriented refinement
- Trace-based derivation of a scalable lock-free stack algorithm
- Simply-typed underdeterminism
- Parallel composition and decomposition of specifications
- Soundness of data refinement for a higher-order imperative language
- Calculating sharp adaptation rules.
- Refinement to certify abstract interpretations: illustrated on linearization for polyhedra
- Angelic processes for CSP via the UTP
- Schedulers and finishers: on generating and filtering the behaviours of an event structure
- Data refinement, call by value and higher order programs
- In praise of algebra
- Unifying theories in ProofPower-Z
- Linking theories in probabilistic programming
- Ensuring liveness properties of distributed systems: open problems
- Abstractions of non-interference security: probabilistic versus possibilistic
- A wide-spectrum language for verification of programs on weak memory models
- Two-dimensional pattern matching against local and regular-like picture languages
- Traits: correctness-by-construction for free
- Sound refactorings
- Fifty years of Hoare's logic
- Laws of mission-based programming
- Proof-based verification approaches for dynamic properties: application to the information system domain
- Towards patterns for heaps and imperative lambdas
- A synchronous program algebra: a basis for reasoning about shared-memory and event-based concurrency
- Safety-critical Java programs from \textsf{Circus} models
- The weakest specifunction
- Compiling quantum programs
- A theory for execution-time derivation in real-time programs
- Specification and verification challenges for sequential object-oriented programs
- Modelling and analysing neural networks using a hybrid process algebra
- Angelicism in the theory of reactive processes
- Simulink timed models for program verification
- Refining specifications to programmable logic
- Using CafeOBJ to mechanise refactoring proofs and application
- On computing representatives
- Type checking \textsf{Circus} specifications
- The laws of programming unify process calculi
- Unifying theories of programming in Isabelle
- A stepwise approach to linking theories
- Proving Quicksort Correct in Event-B
- How to brew-up a refinement ordering
- A graph-based implementation for mechanized refinement calculus of OO programs
- Patterns for refinement automation
- A refinement methodology for object-oriented programs
- scientific article; zbMATH DE number 2130217 (Why is no real title available?)
- Generalised rely-guarantee concurrency: an algebraic foundation
- Safe Modification of Pointer Programs in Refinement Calculus
- On the Purpose of Event-B Proof Obligations
- Inferring Loop Invariants Using Postconditions
- CSP with Hierarchical State
- Incremental System Modelling in Event-B
- scientific article; zbMATH DE number 46740 (Why is no real title available?)
- scientific article; zbMATH DE number 497680 (Why is no real title available?)
- scientific article; zbMATH DE number 517333 (Why is no real title available?)
- Compositional refinement in agent-based security protocols
- Compositional noninterference from first principles
- Experiments in program verification using Event-B
- Emergence and refinement
- Combining decision procedures by (model-)equality propagation
- Refinement-oriented models of Stateflow charts
- Hoare semigroups
- Refinement modal logic
- Computer-aided development of a real-time program
- A generalisation of stationary distributions, and probabilistic program algebra
- A superposition operator for the refinement of algebraic models
- The algebra of multirelations
- Transformational programming and the derivation of algorithms
- Differential Hoare Logics and Refinement Calculi for Hybrid Systems with Isabelle/HOL
- Loop invariants: analysis, classification, and examples
- Stateflow diagrams in Circus
- Combining Decision Procedures by (Model-)Equality Propagation
- Algebra for quantitative information flow
- An algebraic approach to refinement with fair choice
- Linking event-B and concurrent object-oriented programs
- A tactic language for refinement of state-rich concurrent specifications
- A semantics for behavior trees using CSP with specification commands
- Hidden-Markov program algebra with iteration
- A formal software development approach using refinement calculus
- An algebraic approach to the design of compilers for object-oriented languages
- Information Flow Control-by-Construction for an Object-Oriented Language
- Flexible Correct-by-Construction Programming
- Modular verification for shared-variable concurrent programs
- Program semantics and verification technique for AI-centred programs
- Structural operational semantics through context-dependent behaviour
- From control law diagrams to Ada via \textsf{Circus}
- UTP, \textsf{\textit{Circus}}, and Isabelle
- Linking formal methods in software development. A reflection on the development of rCOS
- Specifying and reasoning about shared-variable concurrency
- Towards a model-checker for \textit{\textsf{Circus}}
- \textit{\textsf{Circus2CSP}}: a tool for model-checking \textit{\textsf{Circus}} using FDR
- Program derivation using the refinement calculator
- Relation-algebraic verification of disjoint-set forests
- Predicate transformers and higher-order programs
- Probabilistic datatypes
- Restructuring a concurrent refinement algebra
- An SMT-based approach to the verification of knowledge-based programs
- A theory of software product line refinement
- Program Construction and Verification Components Based on Kleene Algebra
This page was built for publication:
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4301161)
