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
  • Intermediate Representation
  • Case Studies
    • Security
      • Symmetry in the Bakery Algorithm (NuSMV)
      • Non-interference in multi-threaded programs (NuSMV)
      • Fairness in Non-Repudiation Protocols (NuSMV)
      • Co-termination (NuSMV)
      • Deniability (NuSMV)
      • Intransitive Non-interference (NuSMV)
      • Termination-sensitive/-insensitive Non-interference (NuSMV)
      • Nondeterministic Inputs and Transitions (NuSMV)
    • Concurrency
      • Linearizability (NuSMV)
    • Planning
      • Path planning for robots (NuSMV)
    • Synthesis
      • Secrecy-preserving Refinement
      • LTL with Team Semantics
    • Testing
      • Mutation Testing (NuSMV)
  • Playground
  • Download
  • People
  • Publications
Back to top
View this page

Publications¶

The following are HyperQB related papers by the HyperQB team:

  • HyperQB: A QBF-Based Bounded Model Checker for Hyperproperties Tzu-Han Hsu, Borzoo Bonakdarpour, and César Sánchez

  • Bounded Model Checking for Hyperproperties Tzu-Han Hsu, César Sánchez, and Borzoo Bonakdarpour

Previous
People
Copyright © 2025, TART @ MSU
Made with Sphinx and @pradyunsg's Furo