Under-approximation: Under-approximation occurs when behaviors are removed to create the abstract system. This approach corresponds to error-preserving abstractions (where the properties are safety or more general universal properties such as LTL). As mentioned, these abstractions are most useful for finding whether properties are false; hence, they can be used for debugging. Simple examples of under-approximation include: limiting the size of the data domains of a program (e.g., reduce the size of a communication channel) or using a model checker with a limited search depth or until it runs out of resources (memory or time). Program testing is another example: A test driver uses test cases to lead the system through a subset of the possible program executions. Testing is an error-preserving abstraction for these properties.