SPIN

swMATH3455MaRDI QIDQ15987

No author found.

Related Items (only showing first 100 items - show all)

A geometric view of partial order reduction ⋮ State space reduction for process algebra specifications ⋮ Timed hyperproperties ⋮ Formal analysis of oscillatory behaviors in biological regulatory networks: an alternative approach ⋮ An Event-B based approach for cloud composite services verification ⋮ Verification of \(\mathrm{EB}^3\) specifications using CADP ⋮ Bounded situation calculus action theories ⋮ Model-checking structured context-free languages ⋮ Model checking \(\omega \)-regular properties with decoupled search ⋮ Integrating Owicki-Gries for C11-style memory models into Isabelle/HOL ⋮ Model checking dynamic memory allocation in operating systems ⋮ Invariant-driven specifications in Maude ⋮ Projecting transition systems: overcoming state explosion in concurrent system verification ⋮ Symmetry and partial order reduction techniques in model checking Rebeca ⋮ Action language verifier: An infinite-state model checker for reactive software specifications ⋮ Summarization for termination: No return! ⋮ Beyond contracts for concurrency ⋮ ASM-based formal design of an adaptivity component for a cloud system ⋮ Formal modelling and verification of GALS systems using GRL and CADP ⋮ Formalising concurrent UML state machines using coloured Petri nets ⋮ On the diversity of asynchronous communication ⋮ Degeneralization algorithm for generation of Büchi automata based on contented situation ⋮ Verifying distributed real-time properties of embedded systems via graph transformations and model checking ⋮ Feature interaction detection by pairwise analysis of LTL properties -- A case study ⋮ Optimistic synchronization-based state-space reduction ⋮ Model checking learning agent systems using Promela with embedded C code and abstraction ⋮ Experiments with deterministic \(\omega\)-automata for formulas of linear temporal logic ⋮ On deciding synchronizability for asynchronously communicating systems ⋮ Tableau-based automata construction for dynamic linear time temporal logic ⋮ Question-guided stubborn set methods for state properties ⋮ Formal modeling and verification for MVB ⋮ Context-aware counter abstraction ⋮ An invariant-based approach to the verification of asynchronous parameterized networks ⋮ A distributed resource allocation algorithm for many processes ⋮ Robust synthesis for real-time systems ⋮ A complete proof system for propositional projection temporal logic ⋮ MR4UM: a framework for adding fault tolerance to UML state diagrams ⋮ Facilitating the design of fault tolerance in transaction level SystemC programs ⋮ A lazy approach to symmetry reduction ⋮ A formal logic approach to constrained combinatorial testing ⋮ Formal specification of MPI 2.0: case study in specifying a practical concurrent programming API ⋮ Deadlock and starvation free reentrant readers-writers: a case study combining model checking with theorem proving ⋮ A state/event-based model-checking approach for the analysis of abstract system properties ⋮ An accessible verification environment for UML models of services ⋮ Efficient approximate verification of B and Z models via symmetry markers ⋮ An action-based approach to the formal specification and automatic analysis of business processes under authorization constraints ⋮ The sweep-line state space exploration method ⋮ Pointfree expression and calculation: From quantification to temporal logic ⋮ Bisimulation conversion and verification procedure for goal-based control systems ⋮ Complexity results for weighted timed event graphs ⋮ 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 ⋮ Verification of graph grammars using a logical approach ⋮ A formal model for service-oriented interactions ⋮ Sequential and distributed on-the-fly computation of weak tau-confluence ⋮ Exploiting step semantics for efficient bounded model checking of asynchronous systems ⋮ Completeness for flat modal fixpoint logics ⋮ A novel logic-based automatic approach to constructing compliant security policies ⋮ Information gain of black-box testing ⋮ Verification of STM on relaxed memory models ⋮ An analytic tableau calculus for a temporalised belief logic ⋮ Establishing flight software reliability: testing, model checking, constraint-solving, monitoring and learning ⋮ Extended beam search for non-exhaustive state space analysis ⋮ Linear temporal logic symbolic model checking ⋮ A Hoare logic for linear systems ⋮ Model checking RAISE applicative specifications ⋮ Efficient verification of distributed real-time systems with broadcasting behaviors ⋮ Constraint LTL satisfiability checking without automata ⋮ Verification of consensus algorithms using satisfiability solving ⋮ An architectural approach to the analysis, verification and validation of software intensive embedded systems ⋮ Formal reliability analysis of redundancy architectures ⋮ State space search nogood learning: online refinement of critical-path dead-end detectors in planning ⋮ Formal verification of an executable LTL model checker with partial order reduction ⋮ Visibly linear temporal logic ⋮ Automatic distributed code generation from formal models of asynchronous processes interacting by multiway rendezvous ⋮ SMT-based model checking for recursive programs ⋮ Combining fault injection and model checking to verify fault tolerance, recoverability, and diagnosability in multi-agent systems ⋮ Enabling synchronous and asynchronous communications in CSP for SOC ⋮ Z2SAL: a translation-based model checker for Z ⋮ A data-flow approach to test multi-agent ASMs ⋮ Model checking with bounded context switching ⋮ The right tools for the job: correctness of cone of influence reduction proved using ACL2 and HOL4 ⋮ Designing the automatic transformation of visual languages ⋮ CTRL: extension of CTL with regular expressions and fairness operators to verify genetic regulatory networks ⋮ Linear reachability problems and minimal solutions to linear Diophantine equation systems ⋮ Concurrency and refinement in the unified modeling language ⋮ Abstract reduction in directed model checking CCS processes ⋮ Optimising the ProB model checker for B using partial order reduction ⋮ A formal semantics of extended hierarchical state transition matrices using CSP\# ⋮ Analysing neurobiological models using communicating automata ⋮ A formal proof of the deadline driven scheduler in PPTL axiomatic system ⋮ Game-theoretic simulation checking tool ⋮ Nonatomic dual bakery algorithm with bounded tokens ⋮ Linearizability on hardware weak memory models ⋮ Using formal verification to evaluate the execution time of Spark applications ⋮ Verifying time partitioning in the DEOS scheduling kernel ⋮ Translating Java for multiple model checkers: The Bandera back-end ⋮ Automated analysis of fault-tolerance in distributed systems ⋮ \texttt{VeriSIMPL 2}: an open-source software for the verification of max-plus-linear systems

This page was built for software: SPIN