This paper presents a method for automatically constructing an abstract state graph of an arbitrary system using the PVS theorem prover. The method involves partitioning the state space into an abstract state space defined by predicates on program variables, and then computing the successors of each state using PVS to verify if a predicate or its negation is a postcondition of the transition. This allows for the exploration of the abstract state space for any program. The paper discusses the construction of abstract states, abstract transitions, and methods for exploring the abstract state space. It also describes an implementation of the method in a tool that integrates with PVS and the ALDÉBARAN state space analysis tool. The tool has been used to verify a bounded retransmission protocol, demonstrating its effectiveness in automatic verification without significant user intervention. The paper concludes by highlighting the incremental and compositional nature of the method, as well as its potential for debugging and invariant generation.This paper presents a method for automatically constructing an abstract state graph of an arbitrary system using the PVS theorem prover. The method involves partitioning the state space into an abstract state space defined by predicates on program variables, and then computing the successors of each state using PVS to verify if a predicate or its negation is a postcondition of the transition. This allows for the exploration of the abstract state space for any program. The paper discusses the construction of abstract states, abstract transitions, and methods for exploring the abstract state space. It also describes an implementation of the method in a tool that integrates with PVS and the ALDÉBARAN state space analysis tool. The tool has been used to verify a bounded retransmission protocol, demonstrating its effectiveness in automatic verification without significant user intervention. The paper concludes by highlighting the incremental and compositional nature of the method, as well as its potential for debugging and invariant generation.