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

People¶

Tzu-Han Hsu photo
Tzu-Han Hsu
Ph.D. student
Borzoo Bonakdarpour photo
Borzoo Bonakdarpour
Associate Professor – Director
Kenneth Rogale photo
Kenneth Rogale
Ph.D. student
Milad Rabizadeh photo
Milad Rabizadeh
Ph.D. student
Fedor Filippov photo
Fedor Filippov
Undergraduate student
Marco photo
Marco A. de Oliveira Batista
Undergraduate student
Alisha photo
Alisha Brenholt
Master’s student
Next
Publications
Previous
Download
Copyright © 2025, TART @ MSU
Made with Sphinx and @pradyunsg's Furo