jMocha: a model checking tool that exploits design structure

No abstract is available for this paper.

• Publication year

  2001

• Venue

  Proceedings of the 23rd International Conference on Software Engineering. ICSE 2001

• Publication date

  2001-07-01

• Fields of study

  Computer Science, Engineering

• Identifiers
  DOI 10.1109/ICSE.2001.919196
• External record

  Open on Semantic Scholar

• Source metadata

  Semantic Scholar

• No claims are published for this paper.

• No concepts are published for this paper.

• Proceedings of the 23rd International Conference on Software Engineering

  2001cited by this paper
• A Classification of Symbolic Transition Systems

  2000cited by this paper
• Bandera: extracting finite-state models from Java source code

  2000cited by this paper
• Automated Refinement Checking for Asynchronous Processes

  2000cited by this paper
• "Next" Heuristic for On-the-Fly Model Checking

  1999cited by this paper
• You Assume, We Guarantee: Methodology and Case Studies

  1998cited by this paper
• MOCHA: Modularity in Model Checking

  1998cited by this paper
• Alternating-time temporal logic

  1997influential reference
• The Model Checker SPIN

  1997cited by this paper
• VIS: A System for Verification and Synthesis

  1996cited by this paper
• Reactive Modules

  1996influential reference
• Symbolic model checking

  1992cited by this paper

• Approximate Verification of Strategic Abilities under Imperfect Information Using Local Models

  2025cites this paper
• Efficient Model Checking for the Alternating-Time μ-Calculus via Effectivity Frames

  2025cites this paper
• Multi-Agent Reinforcement Learning for Alternating-Time Logic

  2024cites this paper
• SMT4SMTL: A Tool for SMT-Based Satisfiability Checking of SMTL

  2024cites this paper
• Generic Model Checking for Modal Fixpoint Logics in COOL-MC

  2023cites this paper
• Playing to Learn, or to Keep Secret: Alternating-Time Logic Meets Information Theory

  2023cites this paper
• Formal Modelling and Verification of Probabilistic Resource Bounded Agents

  2023cites this paper
• Strategic reasoning with a bounded number of resources: The quest for tractability

  2021cites this paper
• Satisfiability Checking of Strategy Logic with Simple Goals

  2021cites this paper
• STV+Reductions: Towards Practical Verification of Strategic Ability Using Model Reductions

  2021cites this paper
• Strategic Abilities of Asynchronous Agents: Semantic Side Effects

  2020cites this paper
• Strategic Abilities of Asynchronous Agents: Semantic Paradoxes and How to Tame Them

  2020cites this paper
• Timed ATL: Forget Memory, Just Count

  2019cites this paper
• Reasoning about Strategic Abilities

  2019cites this paper
• Strategic logics for collaborative embedded systems

  2019cites this paper
• Strategy Logic with Simple Goals: Tractable Reasoning about Strategies

  2019cites this paper
• Approximate verification of strategic abilities under imperfect information

  2019cites this paper
• Resource-bounded ATL: the Quest for Tractable Fragments

  2019cites this paper
• The role of model checking in software engineering

  2018cites this paper
• Towards Partial Order Reductions for Strategic Ability

  2018cites this paper
• Model Checking Multi-Agent Systems against LDLK Specifications on Finite Traces

  2018cites this paper
• Extended Automata for Temporal Planning of Interacting Agents

  2017cites this paper
• Practical verification of multi-agent systems against Slk specifications

  2017cites this paper
• Timed ATL: Forget Memory, Just Count

  2017cites this paper
• SMC: synthesis of uniform strategies and verification of strategic ability for multi-agent systems

  2017cites this paper
• Timed ATL: Forget Memory, Just Count (Extended Abstract)

  2017cites this paper
• Towards partial order reductions for fragments of alternating-time temporal logic

  2016cites this paper
• Abstraction-Based Verification of Infinite-State Reactive Modules

  2016cites this paper
• Parameterised Model Checking for Alternating-Time Temporal Logic

  2016cites this paper
• Temporal Planning with Extended Timed Automata

  2016cites this paper
• Conference and Workshop Papers

  2015cites this paper
• Bounded model checking of strategy ability with perfect recall

  2015cites this paper
• Verifying and Synthesising Multi-Agent Systems against One-Goal Strategy Logic Specifications

  2015cites this paper
• Applying Rely/Guarantee in Compositional Ontology Alignment

  2014cites this paper
• An Abstraction Technique for the Verification of Multi-Agent Systems Against ATL Specifications

  2014cites this paper
• On module checking and strategies

  2014cites this paper
• Synthesis and Veri cation of Uniform Strategies for Multi-Agent Systems

  2014cites this paper
• Synthesis and Verification of Uniform Strategies for Multi-agent Systems

  2014cites this paper
• Comparison of Model Checking Tools

  2013cites this paper
• Group Synthesis for Alternating-Time Temporal Logic

  2013cites this paper
• Bounded planning for strategic goals with incomplete information and perfect recall

  2013cites this paper
• Verification of temporal-epistemic properties of access control systems

  2012cites this paper
• Hierarchical Modeling and Formal Verification. An Industrial Case Study Using Reo and Vereofy

  2011cites this paper
• A Method for Certifying Code in Trust-By-Policy-Adherence

  2011influential citation
• Digital System Verification: A Combined Formal Methods and Simulation Framework

  2010cites this paper
• Generalizing diagnosability definition and checking for open systems: a Game structure approach

  2010cites this paper
• Design and Verification of Systems with Exogenous Coordination Using Vereofy

  2010cites this paper
• Synthesis Lectures on Digital Circuits and Systems

  2009cites this paper
• INCREMENTAL VALIDATION OF FORMAL SPECIFICATIONS

  2009cites this paper
• Survey and evaluation of approaches for the adaptation reasoning framework

  2009cites this paper
• Incremental Validation of Formal Specifications

  2009cites this paper
• Efficient SAT-based bounded model checking for software verification

  2008cites this paper
• Formal Verification and Parameters Synthesis for Hybrid Real Systems

  2008cites this paper
• Model Checking Abilities of Agents: A Closer Look

  2008cites this paper
• A framework for compositional design and analysis of systems

  2007cites this paper
• Qualitative networks: a symbolic approach to analyze biological signaling networks

  2007cites this paper
• C. V.

  2007cites this paper
• Disk Based Software Verification via Bounded Model Checking

  2007cites this paper
• Integrated Design Validation : Combining Simulation and Formal Verification for Digital Integrated Circuits

  2006cites this paper
• Uniform random sampling of traces in very large models

  2006cites this paper
• A framework for checking behavioral compatibility for component selection

  2006influential citation
• A Collaboration Framework of Selecting Software Components Based on Behavioural Compatibility with User Requirements

  2006cites this paper
• An Introduction to the Tool Ticc

  2006cites this paper
• An environment for compositional specification verification of complex embedded systems

  2005cites this paper
• Monte Carlo Model Checking

  2005influential citation
• Model checking C programs using F-Soft

  2005cites this paper
• Model Checking Strategic Abilities of Agents Under Incomplete Information

  2005cites this paper
• Monte Carlo Analysis of Security Protocols: Needham-Schroeder Revisited∗

  2005cites this paper
• Combining Simulation and Formal Verification for Integrated Circuit Design Validation

  2005cites this paper
• Modular refinement of hierarchic reactive machines

  2004influential citation
• Quantitative Model checking

  2004influential citation
• Formal verification of timed systems: a survey and perspective

  2004cites this paper
• Verifying Invariants of Component-Based Systems through Refinement

  2004cites this paper
• Visuelle Modellierung agentenbasierter Systeme

  2004cites this paper
• Modelling and Analysis of Agents' Goal-Driven Behavior

  2003cites this paper
• Automating formal modular verification of asynchronous real-time embedded systems

  2003cites this paper
• Hierarchical modeling and analysis of embedded systems

  2003cites this paper
• Formal verification of dependable distributed protocols

  2003cites this paper
• Automated environment generation for software model checking

  2003cites this paper
• Synchronous and Bidirectional Component Interfaces

  2002cites this paper
• Visual Specifications for Modular Reasoning about Asynchronous Systems

  2002cites this paper
• Structure and Hierarchy in Real-Time Systems

  2002cites this paper
• Interface Compatibility Checking for Software Modules

  2002cites this paper
• Shared variables interaction diagrams

  2001cites this paper
• Hierarchical Hybrid Modeling of Embedded Systems

  2001cites this paper
• Embedded Software

  2001cites this paper
• Verifying Network Protocol Implementations by Symbolic Refinement Checking

  2001influential citation
• Heuristics for Hierarchical Partitioning with Application to Model Checking

  2000cites this paper
• Modular refinement of hierarchic reactive machines

  2000cites this paper
• 1 EHA : Efficient Modeling and Analysis of Excitable Cell Networks using Hybrid Automata

  year unknowncites this paper
• Summary of Research Efficient Modeling and Analysis of Excitable Cell Networks Using Hybrid Automata 3

  year unknowncites this paper
• Author's Personal Copy Information and Computation Solving Games via Three-valued Abstraction Refinement <

  year unknowncites this paper