N. Klarlund, M. Nielsen, and K. Sunesen, “A Case Study in Automated Verification Based on Trace Abstractions”, BRICS, vol. 2, no. 54, Nov. 1995.