Constrained Monotonic Abstraction: A CEGAR for Parameterized Verification