swMATH7084MaRDI QIDQ19142FDOQ19142
Author name not available (Why is that?)
Official website: http://www.stups.uni-duesseldorf.de/ProB/index.php5/Main_Page
Cited In (89)
- 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
- 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
- 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
- Experiments in program verification using Event-B
- Incomplete SMT techniques for solving non-linear formulas over the integers
- Tracking CSP computations
- 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
- TopSpin
- GeneSyst
- CZT
- Cardinal
- Atelier B
- B4Free
- Kodkod
- Rodin
- MUNCH
- Spin-to-Grape
- SymmSpin
- Model checking RAISE applicative specifications
- csp2B
- jSpin
- PROMELA
- DPPD
- TLC
- BWare
- Z/EVES
- Z
- tptp2X
- FDR2
- FDR3
- SICStus
- ERA-PAT
- PAT
- 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
- Jaza
- EFSMT
- kPWorkbench
- ZRC
- mural
- Coccinelle
- JSetL
- FaCiLe
- 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
- A refinement-based development of a distributed signalling system
- Generating counterexamples for quantitative safety specifications in probabilistic B
- The MEB and CEB Static Analysis for CSP Specifications
- Model checking under fairness in ProB and its application to fair exchange protocols
- 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
- Knowledge representation analysis of graph mining
- Checking the Conformance of a Promela Design to its Formal Specification in Event-B
- Program Development in Computational Logic
- Title not available (Why is that?)
- Model checking approach to automated planning
- Trust Management
- The techniques of formalization of OS Astra Linux Special Edition access control model using Event-B formal method for verification using Rodin and ProB
- Linking event-B and concurrent object-oriented programs
- Specification of a localization component driven by a goal-based approach: some lessons we learned
- Ours Is to Reason Why
- Automatic Generation of CSP || B Skeletons from xUML Models
- Consistency-preserving refactoring of refinement structures in Event-B models
- Title not available (Why is that?)
- Graph generation to statically represent CSP processes
- Lifting General Correctness into Partial Correctness is ok
This page was built for software: ProB
