Case Studies

Our evaluations include the following cases:

Security

• Case #1.1-#1.4: Symmetry in the Bakery Algorithm

• Case #3.1-#3.2: Non-interference in Typed Multi-threaded Programs

• Case #4.1-#4.2: Fairness in Non-repudiation Protocols

• Case #6.1: Mutant Synthesis for Mutation Testing

• Case #7.1: Co-termination of multiple programs

• Case #8.1: Deniability

• Case #9.1 - #9.3: Intransitive Non-interference

• Case #10.1 - #10.2: TINI and TSNI

• Case #11.1: K-safety

• Case #14.1: Non-deterministic init

• Case #14.2: Non-deterministic trans

Concurrency

• Case #2.1-#2.2: Linearizability in SNARK Algorithm

Planning

• Case #5.1-#5.2: Privacy-Preserving Path Synthesis for Robots

Synthesis

• Case #12.1-#12.2: MapSynth

• Case #13.1-#13.2: TeamLTL

References

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