The following pages link to SPIN (Q15987):
Displayed 50 items.
- A lazy approach to symmetry reduction (Q613132) (← links)
- A formal logic approach to constrained combinatorial testing (Q616856) (← links)
- Formal specification of MPI 2.0: case study in specifying a practical concurrent programming API (Q617917) (← links)
- Deadlock and starvation free reentrant readers-writers: a case study combining model checking with theorem proving (Q617922) (← links)
- A state/event-based model-checking approach for the analysis of abstract system properties (Q617925) (← links)
- An accessible verification environment for UML models of services (Q617979) (← links)
- Efficient approximate verification of B and Z models via symmetry markers (Q622591) (← links)
- Pointfree expression and calculation: From quantification to temporal logic (Q633283) (← links)
- Bisimulation conversion and verification procedure for goal-based control systems (Q633304) (← links)
- Completeness for flat modal fixpoint logics (Q638475) (← links)
- Information gain of black-box testing (Q640298) (← links)
- Extended beam search for non-exhaustive state space analysis (Q652163) (← links)
- Efficient verification of distributed real-time systems with broadcasting behaviors (Q656082) (← links)
- Verification of consensus algorithms using satisfiability solving (Q658669) (← links)
- Formal reliability analysis of redundancy architectures (Q667523) (← links)
- Formal verification of an executable LTL model checker with partial order reduction (Q682350) (← links)
- Visibly linear temporal logic (Q682377) (← links)
- Designing the automatic transformation of visual languages (Q701039) (← links)
- Linear reachability problems and minimal solutions to linear Diophantine equation systems (Q703515) (← links)
- Concurrency and refinement in the unified modeling language (Q706511) (← links)
- Abstract reduction in directed model checking CCS processes (Q715051) (← links)
- Optimising the ProB model checker for B using partial order reduction (Q736463) (← links)
- A formal semantics of extended hierarchical state transition matrices using CSP\# (Q736828) (← links)
- Analysing neurobiological models using communicating automata (Q736844) (← links)
- A formal proof of the deadline driven scheduler in PPTL axiomatic system (Q744103) (← links)
- Game-theoretic simulation checking tool (Q764005) (← links)
- Nonatomic dual bakery algorithm with bounded tokens (Q766163) (← links)
- Linearizability on hardware weak memory models (Q782494) (← links)
- Using formal verification to evaluate the execution time of Spark applications (Q782497) (← links)
- Verifying time partitioning in the DEOS scheduling kernel (Q816194) (← links)
- Translating Java for multiple model checkers: The Bandera back-end (Q816196) (← links)
- Automated analysis of fault-tolerance in distributed systems (Q816197) (← links)
- State space reduction for process algebra specifications (Q820124) (← links)
- Timed hyperproperties (Q821560) (← links)
- An Event-B based approach for cloud composite services verification (Q826351) (← links)
- Model-checking structured context-free languages (Q832277) (← links)
- Model checking \(\omega \)-regular properties with decoupled search (Q832281) (← links)
- Integrating Owicki-Gries for C11-style memory models into Isabelle/HOL (Q832723) (← links)
- Model checking dynamic memory allocation in operating systems (Q835783) (← links)
- Invariant-driven specifications in Maude (Q838161) (← links)
- Symmetry and partial order reduction techniques in model checking Rebeca (Q845239) (← links)
- Action language verifier: An infinite-state model checker for reactive software specifications (Q845244) (← links)
- Summarization for termination: No return! (Q845247) (← links)
- Beyond contracts for concurrency (Q846113) (← links)
- Verifying distributed real-time properties of embedded systems via graph transformations and model checking (Q853626) (← links)
- Feature interaction detection by pairwise analysis of LTL properties -- A case study (Q853722) (← links)
- Optimistic synchronization-based state-space reduction (Q853724) (← links)
- Experiments with deterministic \(\omega\)-automata for formulas of linear temporal logic (Q860862) (← links)
- Tableau-based automata construction for dynamic linear time temporal logic (Q862830) (← links)
- Question-guided stubborn set methods for state properties (Q862861) (← links)