ProB

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