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

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)
Next
Symmetry in the Bakery Algorithm (NuSMV)
Previous
Case Studies
Copyright © 2025, TART @ MSU
Made with Sphinx and @pradyunsg's Furo