The Design of a Multicore Extension of the SPIN Model Checker

No abstract is available for this paper.

• Publication year

  2007

• Venue

  IEEE Transactions on Software Engineering

• Publication date

  2007-10-01

• Fields of study

  Computer Science, Engineering

• Identifiers
  DOI 10.1109/TSE.2007.70724
• External record

  Open on Semantic Scholar

• Source metadata

  Semantic Scholar

• No claims are published for this paper.

• No concepts are published for this paper.

• Verification, Model Checking, and Abstract Interpretation

  2009cited by this paper
• A Stack-Slicing Algorithm for Multi-Core Model Checking

  2008cited by this paper
• A mini challenge: build a verifiable filesystem

  2007cited by this paper
• How to Order Vertices for Distributed LTL Model-Checking Based on Accepting Predecessors

  2006cited by this paper
• Parallel External Directed Model Checking with Linear I/O

  2006influential reference
• Large-Scale Directed Model Checking LTL

  2006cited by this paper
• Improving Spin's Partial-Order Reduction for Breadth-First Search

  2005cited by this paper
• Verifying Time Partitioning in the DEOS Scheduling Kernel

  2005cited by this paper
• Load Balancing Parallel Explicit State Model Checking

  2005cited by this paper
• Distributed Partial Order Reduction of State Spaces

  2005cited by this paper
• CTL* model checking on a shared-memory architecture

  2005influential reference
• Using Autonomy Flight Software to Improve Science Return on Earth Observing One

  2005cited by this paper
• Accepting Predecessors Are Better than Back Edges in Distributed LTL Model-Checking

  2004cited by this paper
• Typical Structural Properties of State Spaces

  2004cited by this paper
• Model-Driven Software Verification

  2004cited by this paper
• Parallel breadth-first search LTL model-checking

  2003cited by this paper
• Design and Validation of Computer Protocols

  2003cited by this paper
• Distributed Explicit Fair Cycle Detection

  2003cited by this paper
• Distributed Explicit Fair Cycle Detection (Set Based Approach)

  2003cited by this paper
• The SPIN Model Checker - primer and reference manual

  2003cited by this paper
• Using SPIN model checking for flight software verification

  2002cited by this paper
• Effective State Exploration for Model Checking on a Shared Memory Architecture

  2002cited by this paper
• Partial-Order Reduction in Symbolic State-Space Exploration

  2001cited by this paper
• Distributed LTL model-checking in SPIN

  2001cited by this paper
• Automating software feature verification

  2000cited by this paper
• Distributing Timed Model Checking - How the Search Order Matters

  2000cited by this paper
• Distributed-Memory Model Checking with SPIN

  1999influential reference
• Static Partial Order Reduct ion

  1998cited by this paper
• Cramming More Components Onto Integrated Circuits

  1998cited by this paper
• Partial-Order Reduction in Symbolic State Space Exploration

  1997cited by this paper
• Parallelizing the Murphi Verifier

  1997cited by this paper
• Lectures on Petri Nets I: Basic Models

  1996cited by this paper
• The State Explosion Problem

  1996cited by this paper
• Partial-Order Methods for the Verification of Concurrent Systems

  1996cited by this paper
• On nested depth first search

  1996influential reference
• An improvement in formal verification

  1994cited by this paper
• Combining partial order reductions with on-the-fly model-checking

  1994cited by this paper
• Coverage Preserving Reduction Strategies for Reachability Analysis

  1992cited by this paper
• Depth-First Search is Inherently Sequential

  1985cited by this paper
• Myths About the Mutual Exclusion Problem

  1981cited by this paper
• Parallelizing the Mur ’ Verifier (cid:3)

  year unknowninfluential reference

• Parallel Maude-NPA for Cryptographic Protocol Analysis

  2025influential citation
• The fast and the capacious: memory-efficient multi-GPU accelerated explicit state space exploration with GPUexplore 3.0

  2024cites this paper
• Leveraging Cache Coherence to Detect and Repair False Sharing On-the-fly

  2024cites this paper
• Metis: File System Model Checking via Versatile Input and State Exploration

  2024cites this paper
• A Layered and Parallelized Method of Eventual Model Checking

  2023cites this paper
• Optimization Techniques for Model Checking Leads-to Properties in a Stratified Way

  2023cites this paper
• Sequential and Parallel Tools for Model Checking Conditional Stable Properties in a Layered Way

  2022influential citation
• A Divide and Conquer Approach to Eventual Model Checking

  2021influential citation
• Parallel Graph-Based Stateless Model Checking

  2020cites this paper
• Pipelining Bottom-up Data Flow Analysis

  2020cites this paper
• Swarm model checking on the GPU

  2020cites this paper
• Improving swarming using genetic algorithms

  2020cites this paper
• Parallel Refinement for Multi-Threaded Program Verification

  2019cites this paper
• Towards Parallel Verification of Concurrent Systems using the Symbolic Observation Graph

  2019cites this paper
• Chapter Two - Advances in Software Model Checking

  2018cites this paper
• Improving Parallel State-Space Exploration Using Genetic Algorithms

  2018cites this paper
• Parallel A* for State-Space Search

  2018cites this paper
• Featherlight on-the-fly false-sharing detection

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

  2018cites this paper
• Explicit-State Model Checking

  2018cites this paper
• Fast detection of concurrency errors by state space traversal with randomization and early backtracking

  2018cites this paper
• Scalable Parallel Model Checking via Monte-Carlo Tree Search

  2018cites this paper
• Parameter estimation of qualitative biological regulatory networks on high performance computing hardware

  2018cites this paper
• Lazy Parallel Kronecker Algebra-Operations on Heterogeneous Multicores

  2017cites this paper
• A Survey of Parallel A

  2017cites this paper
• On Hash-Based Work Distribution Methods for Parallel Best-First Search

  2017cites this paper
• SIMPAL: a compositional reasoning framework for imperative programs

  2017cites this paper
• Parallel bug-finding in concurrent programs via reduced interleaving instances

  2017cites this paper
• Parallelizing model checking algorithms using multi-core and many-core architectures

  2017cites this paper
• Recent advances in interactive and automated analysis

  2017cites this paper
• Helena: Handling massively distributed systems with ELaborate ENsemble Architectures

  2016cites this paper
• Some recent advances in automated analysis

  2016cites this paper
• A framework for rigorous development of distributed components: formalisation and tools. (Un environnement pour le développement rigoureux de composants répartis: formalisation et outils logiciels)

  2016cites this paper
• Partial-Order Reduction for GPU Model Checking

  2016influential citation
• Scalable Concurrent Hash Table in Java

  2016cites this paper
• GPU IMPLEMENTATION OF PARTIAL-ORDER REDUCTION

  2016cites this paper
• Towards the Exploration of Hash Tables

  2016cites this paper
• Model Counting Modulo Theories

  2015cites this paper
• Concurrent Bounded Model Checking

  2015cites this paper
• Partial Order Reduction and Symmetry with Multiple Representatives

  2015cites this paper
• Directed and Distributed Model Checking of B-Specifications

  2015cites this paper
• Distributed Assertion Checking Using Symbolic Execution

  2015cites this paper
• Using SPIN for automated debugging of infinite executions of Java programs

  2014cites this paper
• Enabling BYOD through secure meta-market

  2014cites this paper
• Towards a GPGPU-parallel SPIN model checker

  2014cites this paper
• An improvement of the piggyback algorithm for parallel model checking

  2014cites this paper
• Contribution aux tests de vacuité pour le model checking explicite. (Contribution to emptiness checks for explicit model checking)

  2014influential citation
• An Improvement on Acceleration of Distributed SMT Solving

  2014cites this paper
• GPU-aided Model Checking of Markov Decision Processes

  2014influential citation
• Scalable multi-core model checking

  2014cites this paper
• Formal Methods for Dynamical Systems

  2013cites this paper
• ABORDAGENS PARALELAS PARA MODEL CHECKING DE REDES DE AUTÔMATOS ESTOCÁSTICOS

  2013cites this paper
• Model Checking in Bits and Pieces

  2013cites this paper
• Model Checking of Biological Systems

  2013cites this paper
• A Survey of Acceleration Techniques for SMT-Based Bounded Model Checking

  2013cites this paper
• Two complementary approaches to detecting vulnerabilities in C programs. (Deux approches complémentaires pour la détection de vulnérabilités dans les programmes C)

  2013cites this paper
• On the Use of Model Checking for the Bounded and Unbounded Verification of Nonblocking Concurrent Data Structures

  2013cites this paper
• Automated formal analysis and verification: an overview

  2013cites this paper
• Using Event-Based and Rule-Based Paradigms to Develop Context-Aware Reactive Applications. (Programmation événementielle et programmation à base de règles pour le développement d'applications réactives sensibles au contexte.)

  2013cites this paper
• Evaluation of a simple, scalable, parallel best-first search strategy

  2012influential citation
• Introduction into Model Checking An Approach for Parallelization Seminar Paper

  2012cites this paper
• Leveraging Formal Methods and Fuzzing to Verify Security and Reliability Properties of Large-Scale High-Consequence Systems

  2012cites this paper
• Targeting the Cell Broadband Engine for constraint‐based local search

  2012cites this paper
• Parallelizing the Spin Model Checker

  2012cites this paper
• Improving GPU Sparse Matrix-Vector Multiplication for Probabilistic Model Checking

  2012cites this paper
• Designing fast LTL model checking algorithms for many-core GPUs

  2012cites this paper
• Parallelizing top-down interprocedural analyses

  2012cites this paper
• Depth-first Versus Breadth-first Search

  2012cites this paper
• On-the-fly parallel model checking algorithm that is optimal for verification of weak LTL properties

  2012cites this paper
• Parallel Model Checking Using Abstraction

  2012cites this paper
• Planning Under Time Pressure

  2012cites this paper
• Large scale parallel state space search utilizing graphics processing units and solid state disks

  2012cites this paper
• Multi-Core LTSmin: Marrying Modularity and Scalability

  2011influential citation
• Mixed Shared-Distributed Hash Tables Approaches for Parallel State Space Construction

  2011cites this paper
• Design Patterns of Parallel Control Systems.

  2011cites this paper
• Model Checking Multitask Applications for OSEK Compliant Real-Time Operating Systems

  2011cites this paper
• Platform Dependent Verification: On Engineering Verification Tools for 21st Century

  2011cites this paper
• Roomy: a new approach to parallel disk-based computation

  2011influential citation
• Communication in Parallel Algorithms for Constraint-Based Local Search

  2011cites this paper
• Model checking timed properties of healthcare processes

  2011cites this paper
• Parallel Nested Depth-First Searches for LTL Model Checking

  2011cites this paper
• Verifying mediated service interactions considering expected behaviours

  2011cites this paper
• Towards Informed Swarm Verification

  2011cites this paper
• Multi-Core Model Checking

  2011cites this paper
• Verification support for ARINC‐653‐based avionics software

  2011cites this paper
• Multi-core Nested Depth-First Search

  2011cites this paper
• Model Checking Software

  2011cites this paper
• Parallel model checking for multiprocessor architecture. (Model Checking sur Architecture Multiprocesseur)

  2011cites this paper
• Experiments in Parallel Constraint-Based Local Search

  2011cites this paper
• Parallel Model Checking With Lazy Cycle Detection - MCLCD

  2011cites this paper
• Partial Order Reduction in Parallel Model Checking

  2010cites this paper
• DiVinE: Parallel Distributed Model Checker

  2010cites this paper
• Parallel symbolic execution for structural test generation

  2010influential citation
• Parallel probabilistic model checking on general purpose graphics processors

  2010cites this paper
• Model checking software: on some new waves and some evergreens

  2010cites this paper
• SMT-based bounded model checking for multi-threaded software in embedded systems

  2010cites this paper
• Concurrent Multi-browser Crawling of Ajax-based Web Applications

  2010influential citation
• Parallel Partial Order Reduction with Topological Sort Proviso

  2010cites this paper
• Model Checking in Bits and Pieces

  2010cites this paper
• Scalable shared memory LTL model checking

  2010cites this paper