Reachability graph, deadlock and livelock detection, Karp-Miller tree (ω-acceleration) for boundedness, timed simulation with exponential transitions, DOT/PNG visualisation, unit tests.
Académique 2025 → 2026
Petri-net library
Proving a concurrent system never blocks — on a graph, not on a passing test.
- Role
- Pair project, Models & Specifications (Master's 2)
- Context
- Université Marie & Louis Pasteur
- Status
- Completed
- Python
- Tests automatisés