Trace Abstraction Framework and Techniques