Case Studies

Explore the collection of HyperQB case studies organized by thematic area. Jump directly to an overview or one of the featured benchmarks using the cards below.

Security

• Overview

• Symmetry: Bakery Algorithm (NuSMV)

• Non-interference: Multi-threaded Programs (NuSMV)

• Non-Interference Until Close: Secure Winner Disclosure in Fixed-Bid Auctions (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)

• Compiler Optimisations: Security-Preserving Refinement (NuSMV)

• Cache Timing Attack: Observational Determinism (NuSMV)

• LED Blinker Modules (Verilog)

• Observational Determinism: SPI Bus Secondary (Verilog)

• Constant-Time Execution: Floating Point Unit (Verilog)

• Alternating Bit Protocol (NuSMV, w/loops)

• Translation Validation: Matrix Multiplication (NuSMV, w/loops)

• Compiler Optimization: Common Branch Factorization (NuSMV, w/loops)

Concurrency

• Overview

• Linearizability: SNARK (NuSMV)

• Linearizability of Construction-Then-Read: Eliminating Partial Initialization (NuSMV)

• Linearizability: Explicit Memory Management ABA (NuSMV)

• Linearizability: Lazy List Set (NuSMV)

• Linearizability: IQueue (NuSMV)

• Linearizability: Simple Queue (NuSMV)

• Speculative Execution Defenses (NuSMV)

Planning

• Overview

• 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

• Overview

• Secrecy-preserving Refinement (NuSMV)

• LTL with Team Semantics (NuSMV)

• Synthesis for Mutation Testing (NuSMV)