Security

• Symmetry: Bakery Algorithm (NuSMV)
• Non-interference: Multi-threaded Programs (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)
• Declassification by Enforcement: Refinement Check (NuSMV)
• Compiler Optimisations: Security-Preserving Refinement (NuSMV)
• Cache Timing Attack: Observational Determinism (NuSMV)
• Alternating Bit Protocol (NuSMV, w/loops)
• Translation Validation: Matrix Multiplication (NuSMV, w/loops)
• Compiler Optimization: Common Branch Factorization (NuSMV, w/loops)

Verilog

• LED Blinker Modules (Verilog)
• Observational Determinism: SPI Bus Secondary (Verilog)
• Constant-Time Execution: Floating Point Unit (Verilog)