This paper presents a method for automatically constructing abstract state graphs of arbitrary systems using the PVS theorem prover. The method uses a partition of the state space induced by predicates on program variables to define an abstract state space. Abstract state graphs are constructed starting from an abstract initial state, and the possible successors of a state are determined using the PVS theorem prover by verifying if each predicate or its negation is a postcondition of the state. This allows for abstract state space exploration for arbitrary programs. The method is based on abstract interpretation and is similar to the splitting method proposed in previous works. It uses a weaker abstract transition relation to automatically construct abstract state graphs with reasonable computational cost. The abstract state space is defined by a set of monomials on a set of state predicates. The successor of an abstract state for a transition is determined by checking if each predicate or its negation is a postcondition of the state. The PVS theorem prover is used to verify these conditions, and if the tactic used for verification is not powerful enough, an upper approximation of the abstract successor is constructed. The method allows for the computation of upper approximations of the set of reachable states, which is sufficient for verifying invariants. It also enables the construction of abstract state graphs with minimal computational cost, as the expensive part of the algorithm is the computation of an abstract successor. Abstract state graphs can be used for verifying properties expressible as temporal logic formulas without existential quantification over paths. They also represent a relatively precise global control graph of the system, which can be used for backward verification of invariants. The method has been implemented in a tool that constructs abstract state graphs for systems with a single process. It has been used to verify a bounded retransmission protocol developed by Philips, which was previously proven correct using theorem provers. The tool allows for the verification of the protocol without user intervention, as it automatically constructs the abstract state graph and verifies the required properties. The method is efficient and can be applied to systems with infinite state spaces. It uses a set of predicates to define the abstract state space and allows for the construction of abstract state graphs with minimal computational cost. The method is incremental, allowing for the refinement of the abstract state graph by adding more predicates to obtain a more precise abstraction. It is also compositional, allowing for the construction of separate abstract state graphs for each component of a system. The abstract state graphs can be used for debugging and for generating invariants and backward analysis. The method is complementary to other approaches, such as tableau construction, and integrates a reachability analysis.This paper presents a method for automatically constructing abstract state graphs of arbitrary systems using the PVS theorem prover. The method uses a partition of the state space induced by predicates on program variables to define an abstract state space. Abstract state graphs are constructed starting from an abstract initial state, and the possible successors of a state are determined using the PVS theorem prover by verifying if each predicate or its negation is a postcondition of the state. This allows for abstract state space exploration for arbitrary programs. The method is based on abstract interpretation and is similar to the splitting method proposed in previous works. It uses a weaker abstract transition relation to automatically construct abstract state graphs with reasonable computational cost. The abstract state space is defined by a set of monomials on a set of state predicates. The successor of an abstract state for a transition is determined by checking if each predicate or its negation is a postcondition of the state. The PVS theorem prover is used to verify these conditions, and if the tactic used for verification is not powerful enough, an upper approximation of the abstract successor is constructed. The method allows for the computation of upper approximations of the set of reachable states, which is sufficient for verifying invariants. It also enables the construction of abstract state graphs with minimal computational cost, as the expensive part of the algorithm is the computation of an abstract successor. Abstract state graphs can be used for verifying properties expressible as temporal logic formulas without existential quantification over paths. They also represent a relatively precise global control graph of the system, which can be used for backward verification of invariants. The method has been implemented in a tool that constructs abstract state graphs for systems with a single process. It has been used to verify a bounded retransmission protocol developed by Philips, which was previously proven correct using theorem provers. The tool allows for the verification of the protocol without user intervention, as it automatically constructs the abstract state graph and verifies the required properties. The method is efficient and can be applied to systems with infinite state spaces. It uses a set of predicates to define the abstract state space and allows for the construction of abstract state graphs with minimal computational cost. The method is incremental, allowing for the refinement of the abstract state graph by adding more predicates to obtain a more precise abstraction. It is also compositional, allowing for the construction of separate abstract state graphs for each component of a system. The abstract state graphs can be used for debugging and for generating invariants and backward analysis. The method is complementary to other approaches, such as tableau construction, and integrates a reachability analysis.