- Referenced in 261 articles
- Information Technology at FBK-IRST The Model Checking group at Carnegie Mellon University , the Mechanized ... open architecture for model checking, which can be reliably used for the verification of industrial ... research areas. NuSMV2, combines BDD-based model checking component that exploits the CUDD library developed ... Colorado University and SAT-based model checking component that includes an RBC-based Bounded Model...
- Referenced in 330 articles
- Markov chains. Analysis is performed through model checking such systems against specifications written ... tool features three model checking engines: one symbolic, using BDDs (binary decision diagrams) and MTBDDs...
- Referenced in 285 articles
- temporal requirements are verified by symbolic model checking. If the verification fails, then HyTech generates...
- Referenced in 128 articles
- Using the Bandera tool set to model-check properties of concurrent Java software. The Bandera ... components designed to facilitate experimentation with model-checking Java source code. Bandera takes as input ... language of one of several existing model-checking tools (including Spin, dSpin ... model to the property being checked. When a model-checker produces an error trail, Bandera...
- Referenced in 109 articles
- Model checking JAVA programs using JAVA PathFinder. The paper describes a translator called JAVA PATHFINDER ... which translates from JAVA to PROMELA, the modeling language of the SPIN model checker ... PROMELA model, which then can be model checked using SPIN. The JAVA program may contain ... translated into similar assertions in the PROMELA model. The PSIN model checker will then look...
- Referenced in 100 articles
- abstracting PEPA models, and for model checking properties in the Continuous Stochastic Logic (CSL). Download...
- Referenced in 65 articles
- models. It supports PCTL and CSL model checking, and their reward extensions. Distinguishing features ... Markov decision processes (CTMDPs) and CSL model checking by discrete-event simulation. This paper presents...
- Referenced in 62 articles
- SLMC: A tool for model checking concurrent systems against dynamical spatial logic specifications. The Spatial ... concurrency of Caires and Cardelli. Model-checking is one of the most widely used techniques ... check temporal properties of software systems. However, when the analysis focuses on properties related ... outperforms other tools for verifying systems modeled in π-calculus...
- Referenced in 79 articles
- MOCHA: Modularity in Model Checking. MOCHA is a growing interactive software environment for system specification...
- Referenced in 36 articles
- model checker using the Bogor extensible model checking framework Model checking has proven ... developed suggest that domain-specific model checking engines may be more effective than general purpose ... model checking tools. To overcome limitations of existing tools which tend to be monolithic ... have developed an extensible and customizable model checking framework called Bogor. In this tool paper...
- Referenced in 67 articles
- variable scoping, Bebop is able to model check boolean programs with several thousand lines...
- Referenced in 28 articles
- Types as models, model checking message-passing programs. Abstraction and composition are the fundamental issues ... making model checking viable for software. This paper proposes new techniques for automating abstraction ... proof rule for carrying out compositional model checking on the types. Open simulation between ... abstraction relation for compositional model checking. We have implemented these ideas in a tool – PIPER...
- Referenced in 33 articles
- with the state of the art model checking techniques. Web services are loosely coupled distributed ... several challenges in the application of model checking: (1) Numerous competing web service standards, most ... based manipulation are not supported by current model checkers...
- Referenced in 31 articles
- Tool for Compositional Model-Checking of Real-Time Systems. In this paper we present ... tool (CMC) for compositional model-checking of real-time systems. CMC is based...
- Referenced in 26 articles
- simulator. Most importantly, PAT implements various model checking techniques catering for different properties such ... fairness assumptions, refinement checking and probabilistic model checking. To achieve good performance, advanced optimization techniques ... symmetry reduction, process counter abstraction, parallel model checking...
- Referenced in 26 articles
- Cadence SMV is a symbolic model checking tool that allows you to formally verify temporal ... verification is often equated with equivalence checking, model checking is substantially more general. It allows ... design process by building abstract system level models. Its use continues through the design refinement...
- Referenced in 22 articles
- Model checking knowledge. MCK is a model checker for the logic of knowledge, developed ... variety of approaches to model checking the logic of knowledge. The novelty of this model ... were based primarily on BDD-based model checking algorithms, but MCK now also supports bounded ... model checking as well as explicit state model checking...
- Referenced in 40 articles
- graph transformation systems, for instance using model checking...
- Referenced in 24 articles
- Approximate probabilistic model checking. Symbolic model checking methods have been extended recently to the verification ... induce a prohibitive cost for the model checking algorithm. In this paper, we propose...
- Referenced in 37 articles
- Zing is a software model checking project at Microsoft Research. Our goal is to build...