Rodin

swMATH7083MaRDI QIDQ19141

No author found.

Related Items (90)

Theorem proving graph grammars with attributes and negative application conditions ⋮ Proof-Based Approach to Hybrid Systems Development: Dynamic Logic and Event-B ⋮ Systematic Refinement of Abstract State Machines with Higher-Order Logic ⋮ Refinement of Timing Constraints for Concurrent Tasks with Scheduling ⋮ Verifiable Code Generation from Scheduled Event-B Models ⋮ An Event-B based approach for cloud composite services verification ⋮ Relational Differential Dynamic Logic ⋮ Presentation and manipulation of Mizar properties in an Isabelle object logic ⋮ Combining refinement and signal-temporal logic for biological systems ⋮ Verification of \(\mathrm{EB}^3\) specifications using CADP ⋮ Sound verification procedures for temporal properties of infinite-state systems ⋮ Modelling the embedded control system using iUML-B pattern state machine ⋮ Behavioural Models for FMI Co-simulations ⋮ Building Specifications in the Event-B Institution ⋮ Event-B refinement for continuous behaviours approximation ⋮ Integrating formal specifications into applications: the ProB Java API ⋮ Checking the Conformance of a Promela Design to its Formal Specification in Event-B ⋮ Unnamed Item ⋮ Formal verification of cP systems using Coq ⋮ Foundations for using linear temporal logic in Event-B refinement ⋮ Unnamed Item ⋮ Event algebra for transition systems composition application to timed automata ⋮ Traits: correctness-by-construction for free ⋮ Monitorability for the Hennessy-Milner logic with recursion ⋮ Refinement of Structured Interactive Systems ⋮ The refinement calculus of reactive systems ⋮ rCOS: Defining Meanings of Component-Based Software Architectures ⋮ The Subject-Oriented Approach to Software Design and the Abstract State Machines Method ⋮ Consistency-preserving refactoring of refinement structures in Event-B models ⋮ Relating trace refinement and linearizability ⋮ A verification and deployment approach for elastic component-based applications ⋮ Simulation relations for fault-tolerance ⋮ Putting logic-based distributed systems on stable grounds ⋮ Efficient approximate verification of B and Z models via symmetry markers ⋮ Stepwise refinement of heap-manipulating code in Chalice ⋮ External and internal choice with event groups in Event-B ⋮ Security invariants in discrete transition systems ⋮ Experiments in program verification using Event-B ⋮ A New Roadmap for Linking Theories of Programming ⋮ Integration of SMT-solvers in B and Event-B development environments ⋮ Unnamed Item ⋮ Generating counterexamples for quantitative safety specifications in probabilistic B ⋮ Domain science and engineering from computer science to the sciences of informatics. II: Science ⋮ Domain science and engineering from computer science to the sciences of informatics. I: Engineering ⋮ Proving Quicksort Correct in Event-B ⋮ Specification of a Localization Component Driven by a Goal-Based Approach: Some Lessons We Learned ⋮ Automating Event-B invariant proofs by rippling and proof patching ⋮ Fundamentals of software engineering. 6th international conference, FSEN 2015, Tehran, Iran, April 22--24, 2015. Revised selected papers ⋮ Linking Event-B and Concurrent Object-Oriented Programs ⋮ A concurrent constraint programming interpretation of access permissions ⋮ A formal verification technique for behavioural model-to-model transformations ⋮ Manifest domains: analysis and description ⋮ Refining autonomous agents with declarative beliefs and desires ⋮ Translating controlled graph grammars to ordinary graph grammars ⋮ On the purpose of Event-B proof obligations ⋮ Retrenchment for Event-B: UseCase-wise development and Rodin integration ⋮ Elucidating concurrent algorithms via layers of abstraction and reification ⋮ Changing system interfaces consistently: a new refinement strategy for CSP\(\|\)B ⋮ Unnamed Item ⋮ Abstractions of non-interference security: probabilistic versus possibilistic ⋮ Verification by construction of distributed algorithms ⋮ Developing Topology Discovery in Event-B ⋮ Changing System Interfaces Consistently: A New Refinement Strategy for CSP||B ⋮ Modelling resilient collaborative multi-agent systems ⋮ Optimising the ProB model checker for B using partial order reduction ⋮ Provably correct derivation of algorithms using FermaT ⋮ Kaisa Sere: in memoriam ⋮ The behavioural semantics of Event-B refinement ⋮ Derivation of concurrent programs by stepwise scheduling of Event-B models ⋮ Continuous KAOS, ASM, and formal control system design across the continuous/discrete modeling interface: a simple train stopping application ⋮ A formal framework for Hybrid Event B ⋮ Incremental System Modelling in Event-B ⋮ A refinement-based development of a distributed signalling system ⋮ Hybrid dynamic logic institutions for event/data-based systems ⋮ Knowledge representation analysis of graph mining ⋮ A Behavioural Theory of Recursive Algorithms ⋮ Semantics of Mizar as an Isabelle object logic ⋮ Set-Theoretic Models of Computations ⋮ Pliant Modalities in Hybrid Event-B ⋮ Practical Theory Extension in Event-B ⋮ Developing topology discovery in Event-B ⋮ The techniques of formalization of OS Astra Linux Special Edition access control model using Event-B formal method for verification using Rodin and ProB ⋮ On labeled birooted tree languages: algebras, automata and logic ⋮ Specification and verification of concurrent programs through refinements ⋮ Towards leveraging domain knowledge in state-based formal methods ⋮ Moded and continuous abstract state machines ⋮ Proof-based verification approaches for dynamic properties: application to the information system domain ⋮ Rule-based transformation of graph rewriting rules: towards higher-order graph grammars ⋮ Spot the difference: a detailed comparison between B and Event-B ⋮ Flashix: modular verification of a concurrent and crash-safe flash file system

This page was built for software: Rodin