Starting implementation for definite reachability analysis