InVeSt is a tool for automatic generation of abstractions, given a concrete (infinite-state) model and a state abstraction relation. This tool is implemented on top of the theorem prover PVS which is used to build the abstract transition relation. When a property is not satisfied by the abstract model, the tool provides a counter-example which can be analyzed automatically to check if it corresponds to a counter-example in the concrete system, and if not, to refine the considered abstraction relation. Connections between IF and InVeSt are under constructions.