Contents Menu Expand Light mode Dark mode Auto light/dark, in light mode Auto light/dark, in dark mode Skip to content
HyperQB
HyperQB

Contents:

  • Introduction
  • Background Theory
  • Case Studies
    • Security
      • Symmetry: Bakery Algorithm (NuSMV)
      • Non-interference: Multi-threaded Programs (NuSMV)
      • Fairness: Non-Repudiation Protocols (NuSMV)
      • Co-termination (NuSMV)
      • Deniability (NuSMV)
      • Intransitive Non-interference (NuSMV)
      • Termination-sensitive/-insensitive Non-interference (NuSMV)
      • Nondeterministic Inputs and Transitions (NuSMV)
      • Generalized Non-interference: Banking Audit Logs (NuSMV)
      • Concurrent Leakage Variants (NuSMV)
      • Access-Controlled Database: Observational Equivalence (NuSMV)
      • Declassification by Enforcement: Refinement Check (NuSMV)
      • Compiler Optimisations: Security-Preserving Refinement (NuSMV)
      • Cache Timing Attack: Observational Determinism (NuSMV)
      • Alternating Bit Protocol (NuSMV, w/loops)
      • Translation Validation: Matrix Multiplication (NuSMV, w/loops)
      • Compiler Optimization: Common Branch Factorization (NuSMV, w/loops)
      • LED Blinker Modules (Verilog)
      • Observational Determinism: SPI Bus Secondary (Verilog)
      • Constant-Time Execution: Floating Point Unit (Verilog)
    • Concurrency
      • Linearizability: SNARK (NuSMV)
      • Linearizability: Explicit Memory Management ABA (NuSMV)
      • Linearizability: Lazy List Set (NuSMV)
      • Linearizability: IQueue (NuSMV)
      • Linearizability: Simple Queue (NuSMV)
      • Speculative Execution Defenses (NuSMV)
    • Planning
      • Shortest Paths: Grid-World Planning (NuSMV)
      • Path Robustness: Grid-World Planning (NuSMV)
      • Robust Path Planning (NuSMV, w/loops)
      • Plan Synthesis: Wolf–Goat–Cabbage (NuSMV, w/loops)
    • Synthesis
      • Secrecy-preserving Refinement (NuSMV)
      • LTL with Team Semantics (NuSMV)
      • Synthesis for Mutation Testing (NuSMV)
  • Playground
  • Download
  • People
  • Publications
  • HyperQB Support
Back to top
View this page

Concurrency¶

  • Linearizability: SNARK (NuSMV)
  • Linearizability: Explicit Memory Management ABA (NuSMV)
  • Linearizability: Lazy List Set (NuSMV)
  • Linearizability: IQueue (NuSMV)
  • Linearizability: Simple Queue (NuSMV)
  • Speculative Execution Defenses (NuSMV)
Next
Linearizability: SNARK (NuSMV)
Previous
Constant-Time Execution: Floating Point Unit (Verilog)
Copyright © 2025, TART @ MSU
Made with Sphinx and @pradyunsg's Furo