Case Studies
==========
Our evaluations include the following cases:

Security
^^^^^^^^
- :doc:`Case #1.1-#1.4: Symmetry in the Bakery Algorithm<case-studies/symmetry>`
- :doc:`Case #3.1-#3.2: Non-interference in Typed Multi-threaded Programs</case-studies/non-interference>`
- :doc:`Case #4.1-#4.2: Fairness in Non-repudiation Protocols</case-studies/fairness>`
- :doc:`Case #6.1: Mutant Synthesis for Mutation Testing<case-studies/mutation>`
- :doc:`Case #7.1: Co-termination of multiple programs<case-studies/co-termination>`
- :doc:`Case #8.1: Deniability<case-studies/deniability>`
- :doc:`Case #9.1 - #9.3: Intransitive Non-interference<case-studies/intransitive-non-interference>`
- :doc:`Case #10.1 - #10.2: TINI and TSNI<case-studies/termination-non-interference>`
- :doc:`Case #11.1: K-safety<case-studies/termination-non-interference>`
- :doc:`Case #14.1: Non-deterministic init<case-studies/nondeterministic>`
- :doc:`Case #14.2: Non-deterministic trans<case-studies/nondeterministic>`

Concurrency
^^^^^^^^^^^
- :doc:`Case #2.1-#2.2: Linearizability in SNARK Algorithm<case-studies/linearizability>`

Planning
^^^^^^^^
- :doc:`Case #5.1-#5.2: Privacy-Preserving Path Synthesis for Robots<case-studies/path-planning>`

Synthesis
^^^^^^^^^
- :doc:`Case #12.1-#12.2: MapSynth<case-studies/secrecy>`
- :doc:`Case #13.1-#13.2: TeamLTL<case-studies/teamltl>`

References
^^^^^^^^^^

1. `HyperQB: A QBF-Based Bounded Model Checker for Hyperproperties <https://arxiv.org/pdf/2109.12989>`_ *Tzu-Han Hsu, Borzoo Bonakdarpour, and César Sánchez*