SPIN - MaRDI portal

swMATH3455MaRDI QIDQ15987FDOQ15987

Author name not available (Why is that?)

Cited In (only showing first 100 items - show all)

Models and formal verification of multiprocessor system-on-chips
Title not available (Why is that?)
Title not available (Why is that?)
Ant colony optimization with partial order reduction for discovering safety property violations in concurrent models
Title not available (Why is that?)
Title not available (Why is that?)
Title not available (Why is that?)
Title not available (Why is that?)
Model checking dynamic memory allocation in operating systems
Verifying a signature architecture: a comparative case study
Title not available (Why is that?)
Action language verifier: An infinite-state model checker for reactive software specifications
Beyond contracts for concurrency
Symmetry and partial order reduction techniques in model checking Rebeca
Summarization for termination: No return!
Type inference and strong static type checking for Promela
Optimistic synchronization-based state-space reduction
Verifying distributed real-time properties of embedded systems via graph transformations and model checking
Model Checking Quantified Computation Tree Logic
Temporal Verification of Fault-Tolerant Protocols
A note on stutter-invariant PLTL
Tableau-based automata construction for dynamic linear time temporal logic
CONCUR 2004 - Concurrency Theory
Refinement and verification in component-based model-driven design
Title not available (Why is that?)
Title not available (Why is that?)
An efficient partial order reduction algorithm with an alternative proviso implementation
Designing communicating transaction processes by supervisory control theory
Representing the MSR cryptoprotocol specification language in an extension of rewriting logic with dependent types
From NuSMV to SPIN: Experiences with model checking flight guidance systems
Search algorithms for automated validation
On the unusual effectiveness of logic in computer science
Dynamic analysis of Petri net-based discrete systems
Hybrid automata-based CEGAR for rectangular hybrid systems
A canonical form based decision procedure and model checking approach for propositional projection temporal logic
A complete axiom system for propositional projection temporal logic with cylinder computation model
Synthesizing distributed protocol specifications from a UML state machine modeled service specification
Model checking the observational determinism security property using PROMELA and SPIN
Synchronizing relations on words
The verified software repository: a step towards the verifying compiler
Highly-fair bakery algorithm using symmetric tokens
Model-checking iterated games
Formal Approaches to Software Testing
Computer Aided Verification
Title not available (Why is that?)
Random walk based heuristic algorithms for distributed memory model checking
CTL Model-Checking with Graded Quantifiers
Tools and Algorithms for the Construction and Analysis of Systems
Title not available (Why is that?)
Bounded model checking of traffic light control system
Principles of Distributed Systems
Title not available (Why is that?)
Title not available (Why is that?)
A complete proof system for propositional projection temporal logic
Facilitating the design of fault tolerance in transaction level SystemC programs
MR4UM: a framework for adding fault tolerance to UML state diagrams
Theoretical Aspects of Computing – ICTAC 2005
Hybrid Systems: Computation and Control
Best-first heuristic search for multicore machines
Selective Approaches for Solving Weak Games
Efficient on-the-fly model-checking for regular alternation-free \(\mu\)-calculus
Semantics and pragmatics of real-time maude
A formal model for service-oriented interactions
Title not available (Why is that?)
Title not available (Why is that?)
Title not available (Why is that?)
Title not available (Why is that?)
Quantitative Analysis of UML Statechart Models of Dependable Systems
Unconditional secure communication: a Russian cards protocol
Experiments with deterministic \(\omega\)-automata for formulas of linear temporal logic
Modeling Routing Protocols in Adhoc Networks
Model checking multi-agent systems with logic based Petri nets
Bounded LTL model checking with stable models
An action-based approach to the formal specification and automatic analysis of business processes under authorization constraints
The sweep-line state space exploration method
Completeness for flat modal fixpoint logics
Complexity results for weighted timed event graphs
Title not available (Why is that?)
Title not available (Why is that?)
The Maude LTL model checker
Graph Transformations
Translation from Adapted UML to Promela for CORBA-Based Applications
A model checking-based approach for security policy verification of mobile systems
Kripke modelling and verification of temporal specifications of a multiple UAV system
Correct transformation: from object-based graph grammars to PROMELA
Exploiting step semantics for efficient bounded model checking of asynchronous systems
Sequential and distributed on-the-fly computation of weak tau-confluence
Verification of graph grammars using a logical approach
Title not available (Why is that?)
An automata-theoretic approach to infinite-state systems
A state/event-based model-checking approach for the analysis of abstract system properties
A novel logic-based automatic approach to constructing compliant security policies
Formal verification of a railway interlocking system using model checking
Automated Technology for Verification and Analysis
Modular strategies for recursive game graphs
Verification of STM on relaxed memory models
``More deterministic vs. ``smaller Büchi automata for efficient LTL model checking
Types as models: model checking message-passing programs
An analytic tableau calculus for a temporalised belief logic
Establishing flight software reliability: testing, model checking, constraint-solving, monitoring and learning

This page was built for software: SPIN