Partial model checking via abstract interpretation