P
pacman
The tool PACMAN derives counting invariants for parameterized concurrent programs and incrementally predicate abstracts them, leveraging on a nested constrained monotonic abstraction CEGAR loop which is implemented by its sister project zaama.