L. Kovacs: "Symbol Elimination in Program Analysis"; Technische Universität Wien/Fakultät für Informatik, 2012.