A Formal Framework for Trace Abstraction
and Correlation