CONCURRENT ON-THE-FLY SCC-BASED LTL MODEL CHECKING
- Mentors
- Markus Kuppe, tla+guru
- Organization
- TLA+
Project aims at implementation and proof of concurrent on-the-fly SCC detection algorithm to aid in liveness checking of TLC model checker. The goal is to allow TLC's liveness checking to scale on large state space as opposed to Tarjan's sequential solution to this problem.