ProB

swMATH7084MaRDI QIDQ19142FDOQ19142

Author name not available (Why is that?)

Cited In (56)

• Linking Event-B and Concurrent Object-Oriented Programs
• The techniques of formalization of OS Astra Linux Special Edition access control model using Event-B formal method for verification using Rodin and ProB
• Automatic Generation of CSP || B Skeletons from xUML Models
• Title not available (Why is that?)
• Knowledge representation analysis of graph mining
• An Event-B based approach for cloud composite services verification
• Solving quantifier-free first-order constraints over finite sets and binary relations
• Pardinus: a temporal relational model finder
• Checking the Conformance of a Promela Design to its Formal Specification in Event-B
• Model Checking under Fairness in ProB and Its Application to Fair Exchange Protocols
• Towards leveraging domain knowledge in state-based formal methods
• Spot the difference: a detailed comparison between B and Event-B
• Static slicing of explicitly synchronized languages
• Title not available (Why is that?)
• A verification and deployment approach for elastic component-based applications
• Program Development in Computational Logic
• Verification of \(\mathrm{EB}^3\) specifications using CADP
• A set solver for finite set relation algebra
• FM 2005: Formal Methods
• Sound reasoning in \textit{tock}-CSP
• Title not available (Why is that?)
• Graph Generation to Statically Represent CSP Processes
• Experiments in program verification using Event-B
• Tracking CSP computations
• Model checking approach to automated planning
• Trust Management
• Fast and accurate strong termination analysis with an application to partial evaluation
• On the analysis of compensation correctness
• Formal verification of cP systems using Coq
• Object oriented concepts identification from formal \(B\) specifications
• Optimising the ProB model checker for B using partial order reduction
• Integrating formal specifications into applications: the ProB Java API
• Security invariants in discrete transition systems
• Model checking action system refinements
• A decision procedure for restricted intensional sets
• Model checking RAISE applicative specifications
• Efficient approximate verification of B and Z models via symmetry markers
• Formal verification of cP systems using PAT3 and ProB
• Foundations for using linear temporal logic in Event-B refinement
• ZB 2005: Formal Specification and Development in Z and B
• Stepwise refinement of heap-manipulating code in Chalice
• Proof-based verification approaches for dynamic properties: application to the information system domain
• CSP theorems for communicating B machines
• Specification of a Localization Component Driven by a Goal-Based Approach: Some Lessons We Learned
• A refinement-based development of a distributed signalling system
• Ours Is to Reason Why
• Generating counterexamples for quantitative safety specifications in probabilistic B
• The MEB and CEB Static Analysis for CSP Specifications
• Consistency-preserving refactoring of refinement structures in Event-B models
• Incomplete SMT Techniques for Solving Non-Linear Formulas over the Integers
• Automated reasoning with restricted intensional sets
• Validation of formal models by refinement animation
• Directed Model Checking for B: An Evaluation and New Techniques
• Removing algebraic data types from constrained Horn clauses using difference predicates
• Incremental System Modelling in Event-B
• Lifting General Correctness into Partial Correctness is ok

This page was built for software: ProB