ABSTRACT. We present a method of abstracting parameterized or infinite-state symbolic model checking problems to finite-state problems, based on propositional skeletons and eager theory explication. The method is extensible in the sense that users can add abstractions (or refine existing abstractions) by providing axiom schemata. We evaluate the method on a collection of parameterized and infinite-state case studies, including FLASH cache coherence protocol and the Virtually Synchronous Paxos distributed consensus protocol. The approach is seen to substantially reduce the complexity of the required auxiliary invariants in comparison to invariant checking using an SMT solver.