Rodin
From MaRDI portal
Cited in
(only showing first 100 items - show all)- ProofPeer
- ViSiDiA
- Pliant modalities in hybrid Event-B
- Modeling in Event B. System and software engineering.
- scientific article; zbMATH DE number 7453194 (Why is no real title available?)
- Efficient approximate verification of B and Z models via symmetry markers
- Foundations for using linear temporal logic in Event-B refinement
- FeatherTrait
- Traits: correctness-by-construction for free
- The subject-oriented approach to software design and the abstract state machines method
- Verifiable Code Generation from Scheduled Event-B Models
- The behavioural semantics of Event-B refinement
- BGSL
- RUN-ONCO
- TraitCbC
- Stepwise refinement of heap-manipulating code in Chalice
- Proof-based verification approaches for dynamic properties: application to the information system domain
- External and internal choice with event groups in Event-B
- Abstractions of non-interference security: probabilistic versus possibilistic
- Developing topology discovery in Event-B
- A refinement-based development of a distributed signalling system
- Hybrid dynamic logic institutions for event/data-based systems
- Proving Quicksort Correct in Event-B
- Simulation relations for fault-tolerance
- A formal framework for Hybrid Event B
- BTestBox
- EventB2Java
- Moded and continuous abstract state machines
- On labeled birooted tree languages: algebras, automata and logic
- Fundamentals of software engineering. 6th international conference, FSEN 2015, Tehran, Iran, April 22--24, 2015. Revised selected papers
- Generating counterexamples for quantitative safety specifications in probabilistic B
- Building Specifications in the Event-B Institution
- Semantics of Mizar as an Isabelle object logic
- Integration of SMT-solvers in B and Event-B development environments
- Changing System Interfaces Consistently: A New Refinement Strategy for CSP||B
- Consistency-preserving refactoring of refinement structures in Event-B models
- Set-theoretic models of computations
- Automating Event-B invariant proofs by rippling and proof patching
- Manifest domains: analysis and description
- Refining autonomous agents with declarative beliefs and desires
- Refinement of Timing Constraints for Concurrent Tasks with Scheduling
- Relating trace refinement and linearizability
- scientific article; zbMATH DE number 7178367 (Why is no real title available?)
- Domain science and engineering from computer science to the sciences of informatics. I: Engineering
- BMotionWeb
- JeB
- VisB
- WebASM
- TraitRecordJ
- Translating controlled graph grammars to ordinary graph grammars
- Incremental System Modelling in Event-B
- Developing Topology Discovery in Event-B
- An Event-B based approach for cloud composite services verification
- Knowledge representation analysis of graph mining
- Presentation and manipulation of Mizar properties in an Isabelle object logic
- Verification by construction of distributed algorithms
- Alcove
- A formal verification technique for behavioural model-to-model transformations
- Sound verification procedures for temporal properties of infinite-state systems
- Refinement of structured interactive systems
- Event-B refinement for continuous behaviours approximation
- Practical theory extension in Event-B
- The refinement calculus of reactive systems
- On the purpose of Event-B proof obligations
- Retrenchment for Event-B: UseCase-wise development and Rodin integration
- Relational differential dynamic logic
- A behavioural theory of recursive algorithms
- rCOS: defining meanings of component-based software architectures
- Checking the Conformance of a Promela Design to its Formal Specification in Event-B
- Towards leveraging domain knowledge in state-based formal methods
- Flashix: modular verification of a concurrent and crash-safe flash file system
- Spot the difference: a detailed comparison between B and Event-B
- A verification and deployment approach for elastic component-based applications
- Specification and verification of concurrent programs through refinements
- Verification of \(\mathrm{EB}^3\) specifications using CADP
- Changing system interfaces consistently: a new refinement strategy for CSP\(\|\)B
- Monitorability for the Hennessy-Milner logic with recursion
- Elucidating concurrent algorithms via layers of abstraction and reification
- Modelling the embedded control system using iUML-B pattern state machine
- A new roadmap for linking theories of programming
- Experiments in program verification using Event-B
- Proof-Based Approach to Hybrid Systems Development: Dynamic Logic and Event-B
- A concurrent constraint programming interpretation of access permissions
- scientific article; zbMATH DE number 7533347 (Why is no real title available?)
- Putting logic-based distributed systems on stable grounds
- Theorem proving graph grammars with attributes and negative application conditions
- Modelling resilient collaborative multi-agent systems
- Provably correct derivation of algorithms using FermaT
- Formal verification of cP systems using Coq
- Optimising the ProB model checker for B using partial order reduction
- Continuous KAOS, ASM, and formal control system design across the continuous/discrete modeling interface: a simple train stopping application
- Derivation of concurrent programs by stepwise scheduling of Event-B models
- Kaisa Sere: in memoriam
- Combining refinement and signal-temporal logic for biological systems
- Behavioural models for FMI co-simulations
- The techniques of formalization of OS Astra Linux Special Edition access control model using Event-B formal method for verification using Rodin and ProB
- Systematic Refinement of Abstract State Machines with Higher-Order Logic
- Specification of a localization component driven by a goal-based approach: some lessons we learned
- Rule-based transformation of graph rewriting rules: towards higher-order graph grammars
- Integrating formal specifications into applications: the ProB Java API
This page was built for software: Rodin
