Verification and Synthesis of Counters based on Symbolic Techniques