PhD thesis introducing a complete framework for Abstract Execution, as well a general framework for symbolic execution, model and dynamic trace logic based on the trace modality, and new safety preconditions for statement-based refactoring techniques for Java.