Deprecated: $wgMWOAuthSharedUserIDs=false is deprecated, set $wgMWOAuthSharedUserIDs=true, $wgMWOAuthSharedUserSource='local' instead [Called from MediaWiki\HookContainer\HookContainer::run in /var/www/html/w/includes/HookContainer/HookContainer.php at line 135] in /var/www/html/w/includes/Debug/MWDebug.php on line 372
ProB - MaRDI portal

ProB

From MaRDI portal
Software:19142



swMATH7084MaRDI QIDQ19142


No author found.





Related Items (56)

Sound reasoning in \textit{tock}-CSPA set solver for finite set relation algebraAn Event-B based approach for cloud composite services verificationVerification of \(\mathrm{EB}^3\) specifications using CADPTracking CSP computationsIntegrating formal specifications into applications: the ProB Java APIChecking the Conformance of a Promela Design to its Formal Specification in Event-BModel Checking under Fairness in ProB and Its Application to Fair Exchange ProtocolsFormal verification of cP systems using CoqTrust ManagementFoundations for using linear temporal logic in Event-B refinementUnnamed ItemA decision procedure for restricted intensional setsAutomated reasoning with restricted intensional setsObject oriented concepts identification from formal \(B\) specificationsConsistency-preserving refactoring of refinement structures in Event-B modelsA verification and deployment approach for elastic component-based applicationsEfficient approximate verification of B and Z models via symmetry markersStatic slicing of explicitly synchronized languagesStepwise refinement of heap-manipulating code in ChaliceSecurity invariants in discrete transition systemsUnnamed ItemCSP theorems for communicating B machinesExperiments in program verification using Event-BValidation of formal models by refinement animationOn the analysis of compensation correctnessUnnamed ItemGenerating counterexamples for quantitative safety specifications in probabilistic BModel checking RAISE applicative specificationsDirected Model Checking for B: An Evaluation and New TechniquesSpecification of a Localization Component Driven by a Goal-Based Approach: Some Lessons We LearnedZB 2005: Formal Specification and Development in Z and BGraph Generation to Statically Represent CSP ProcessesFast and Accurate Strong Termination Analysis with an Application to Partial EvaluationFormal verification of cP systems using PAT3 and ProBLinking Event-B and Concurrent Object-Oriented ProgramsProgram Development in Computational LogicFM 2005: Formal MethodsModel checking approach to automated planningLifting General Correctness into Partial Correctness is okThe MEB and CEB Static Analysis for CSP SpecificationsOptimising the ProB model checker for B using partial order reductionSolving quantifier-free first-order constraints over finite sets and binary relationsIncomplete SMT Techniques for Solving Non-Linear Formulas over the IntegersModel checking action system refinementsIncremental System Modelling in Event-BA refinement-based development of a distributed signalling systemKnowledge representation analysis of graph miningOurs Is to Reason WhyAutomatic Generation of CSP || B Skeletons from xUML ModelsThe techniques of formalization of OS Astra Linux Special Edition access control model using Event-B formal method for verification using Rodin and ProBRemoving algebraic data types from constrained Horn clauses using difference predicatesPardinus: a temporal relational model finderTowards leveraging domain knowledge in state-based formal methodsProof-based verification approaches for dynamic properties: application to the information system domainSpot the difference: a detailed comparison between B and Event-B


This page was built for software: ProB