Concurrent Protocol Verification with PRISM

I modeled mutual-exclusion protocols in PRISM and examined safety, progress, waiting rewards, and deliberately faulty variants.

My role

Concurrent-protocol modeling and verification within a capstone team

Outcome

Verified properties of two 5,738-state Bakery models and exposed a mutual-exclusion failure in a faulty variant.