bib.bib

@inproceedings{braun13cc,
    title = {Simple and Efficient Construction of Static Single Assignment Form},
    booktitle = {Compiler Construction},
    year = {2013},
    publisher = {Springer},
    volume = {7791},
    pages = {102--122},
    author = {Matthias Braun and Sebastian Buchwald and Sebastian Hack and Roland Lei { \ss } a and Christoph Mallon and Andreas Zwinkau},
    editor = {Jhala, Ranjit and Bosschere, Koen},
    series = {Lecture Notes in Computer Science},
    url = {http://dx.doi.org/10.1007/978-3-642-37051-9\_6},
    doi = {10.1007/978-3-642-37051-9_6},
}
@article{cytron91,
    author = {Cytron, Ron and Ferrante, Jeanne and Rosen, Barry K. and Wegman, Mark N. and Zadeck, F. Kenneth},
    title = {Efficiently computing static single assignment form and the control dependence graph},
    journal = {ACM Transactions on Programming Languages and Systems},
    issue_date = {Oct. 1991},
    volume = {13},
    number = {4},
    month = oct,
    year = {1991},
    issn = {0164-0925},
    pages = {451--490},
    numpages = {40},
    url = {http://doi.acm.org/10.1145/115372.115320},
    doi = {10.1145/115372.115320},
    acmid = {115320},
    publisher = {ACM},
    address = {New York, NY, USA},
    keywords = {control dependence, control flow graph, def-use chain, dominator, optimizing compilers},
}
@misc{LLVM_LCSSA,
    title = {LCSSA.cpp},
    url = {http://web.mit.edu/freebsd/head/contrib/llvm/lib/Transforms/Utils/LCSSA.cpp},
    journal = {LLVM - Web MIT},
    publisher = {MIT},
    author = { University of Illinois at Urbana-Champaign and LLVM Team}
}
@InProceedings{LLVM,
    author = {Lattner, Chris and Adve, Vikram},
    title = {{ LLVM } : A Compilation Framework for Lifelong Program Analysis \& Transformation},
    booktitle = {Proceedings of the international symposium on Code generation and optimization: feedback-directed and runtime optimization},
    series = {CGO '04},
    year = {2004},
    isbn = {0-7695-2102-9},
    location = {Palo Alto, California},
    pages = {75--},
    url = {http://dl.acm.org/citation.cfm?id=977395.977673},
    acmid = {977673},
    publisher = {IEEE Computer Society},
}
@techreport{libfirm,
    title = {{ libFIRM } -- A Library for Compiler Optimization Research Implementing { FIRM }},
    year = {2002},
    month = sep,
    publisher = {Universit{\"a}t Karlsruhe, Fakult{\"a}t f{\"u}r Informatik},
    number = {2002-5},
    pages = {75},
    chapter = {9},
    author = {G{\"o}tz Lindenmaier},
    url = {http://www.info.uni-karlsruhe.de/papers/Lind\_02-firm\_tutorial.ps},
}
@inproceedings{alpern,
    author = {Alpern, B. and Wegman, M. N. and Zadeck, F. K.},
    title = {Detecting equality of variables in programs},
    booktitle = {Proceedings of the 15th ACM SIGPLAN-SIGACT symposium on Principles of programming languages},
    series = {POPL '88},
    year = {1988},
    isbn = {0-89791-252-7},
    location = {San Diego, California, USA},
    pages = {1--11},
    numpages = {11},
    url = {http://doi.acm.org/10.1145/73560.73561},
    doi = {10.1145/73560.73561},
    acmid = {73561},
    publisher = {ACM},
}
@article{locales,
    year = {2013},
    issn = {0168-7433},
    journal = {Journal of Automated Reasoning},
    doi = {10.1007/s10817-013-9284-7},
    title = {Locales: A Module System for Mathematical Theories},
    url = {http://dx.doi.org/10.1007/s10817-013-9284-7},
    publisher = {Springer},
    keywords = {Theorem prover; Module system; Theory hierarchy; Theory interpretation; Isabelle},
    author = {Ballarin, Clemens},
    pages = {1-31},
    language = {English}
}
@inproceedings{zhao2013formal,
    author = {Zhao, Jianzhou and Nagarakatte, Santosh and Martin, Milo M.K. and Zdancewic, Steve},
    title = {{ Formal verification of SSA-based optimizations for LLVM }},
    booktitle = {Proceedings of the 34th ACM SIGPLAN conference on Programming language design and implementation},
    series = {PLDI '13},
    year = {2013},
    isbn = {978-1-4503-2014-6},
    location = {Seattle, Washington, USA},
    pages = {175--186},
    numpages = {12},
    url = {http://doi.acm.org/10.1145/2491956.2462164},
    doi = {10.1145/2491956.2462164},
    acmid = {2462164},
    publisher = {ACM},
    keywords = {coq, llvm, single static assignment},
}
@incollection{aycock2000simple,
    year = {2000},
    isbn = {978-3-540-67263-0},
    booktitle = {Compiler Construction},
    volume = {1781},
    series = {Lecture Notes in Computer Science},
    doi = {10.1007/3-540-46423-9_8},
    title = {Simple Generation of Static Single-Assignment Form},
    url = {http://dx.doi.org/10.1007/3-540-46423-9_8},
    publisher = {Springer},
    author = {Aycock, John and Horspool, Nigel},
    pages = {110-125},
    language = {English}
}
@inproceedings{zhao2012formalizing,
    author = {Zhao, Jianzhou and Nagarakatte, Santosh and Martin, Milo M.K. and Zdancewic, Steve},
    title = {Formalizing the { LLVM } intermediate representation for verified program transformations},
    booktitle = {Proceedings of the 39th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages},
    series = {POPL '12},
    year = {2012},
    isbn = {978-1-4503-1083-3},
    location = {Philadelphia, PA, USA},
    pages = {427--440},
    numpages = {14},
    url = {http://doi.acm.org/10.1145/2103656.2103709},
    doi = {10.1145/2103656.2103709},
    acmid = {2103709},
    publisher = {ACM},
    keywords = {Coq, LLVM, memory safety},
}
@article{kalvala2009program,
    author = {Kalvala, Sara and Warburton, Richard and Lacey, David},
    title = {Program transformations using temporal logic side conditions},
    journal = {ACM Transactions on Programming Languages and Systems},
    issue_date = {May 2009},
    volume = {31},
    number = {4},
    month = may,
    year = {2009},
    issn = {0164-0925},
    pages = {14:1--14:48},
    articleno = {14},
    numpages = {48},
    url = {http://doi.acm.org/10.1145/1516507.1516509},
    doi = {10.1145/1516507.1516509},
    acmid = {1516509},
    publisher = {ACM},
    keywords = {Optimizing compilers, program transformation, rewriting, temporal logic},
}
@inproceedings{huffman2012lifting,
    title = {Lifting and Transfer: A Modular Design for Quotients in { Isabelle/HOL }},
    author = {Huffman, Brian and Kun { \v { c } } ar, Ond { \v { r } } ej}
}
@article{paulson2000foundation,
    author = {Paulson, L. C.},
    title = {The foundation of a generic theorem prover},
    journal = {Journal of Automated Reasoning},
    issue_date = {September 1989},
    volume = {5},
    number = {3},
    month = sep,
    year = {1989},
    issn = {0168-7433},
    pages = {363--397},
    numpages = {35},
    url = {http://dx.doi.org/10.1007/BF00248324},
    doi = {10.1007/BF00248324},
    acmid = {67178},
    publisher = {Springer},
    address = {Secaucus, NJ, USA},
}
@inproceedings{choi1991automatic,
    author = {Choi, Jong-Deok and Cytron, Ron and Ferrante, Jeanne},
    title = {Automatic construction of sparse data flow evaluation graphs},
    booktitle = {Proceedings of the 18th ACM SIGPLAN-SIGACT symposium on Principles of programming languages},
    series = {POPL '91},
    year = {1991},
    isbn = {0-89791-419-8},
    location = {Orlando, Florida, USA},
    pages = {55--66},
    numpages = {12},
    url = {http://doi.acm.org/10.1145/99583.99594},
    doi = {10.1145/99583.99594},
    acmid = {99594},
    publisher = {ACM},
}
@inproceedings{sreedhar1995linear,
    author = {Sreedhar, Vugranam C. and Gao, Guang R.},
    title = {A linear time algorithm for placing $\Phi$-nodes},
    booktitle = {Proceedings of the 22nd ACM SIGPLAN-SIGACT symposium on Principles of programming languages},
    series = {POPL '95},
    year = {1995},
    isbn = {0-89791-692-1},
    location = {San Francisco, California, USA},
    pages = {62--73},
    numpages = {12},
    url = {http://doi.acm.org/10.1145/199448.199464},
    doi = {10.1145/199448.199464},
    acmid = {199464},
    publisher = {ACM},
}
@article{bilardi2003algorithms,
    author = {Bilardi, Gianfranco and Pingali, Keshav},
    title = {Algorithms for computing the static single assignment form},
    journal = {ACM Transactions on Computational Logic},
    issue_date = {May 2003},
    volume = {50},
    number = {3},
    month = may,
    year = {2003},
    issn = {0004-5411},
    pages = {375--425},
    numpages = {51},
    url = {http://doi.acm.org/10.1145/765568.765573},
    doi = {10.1145/765568.765573},
    acmid = {765573},
    publisher = {ACM},
    address = {New York, NY, USA},
    keywords = {Control dependence, optimizing compilers, program optimization, program transformation, static single assignment form},
}
@misc{gcc-ssa,
    title = {The { GCC } Internals Documentation},
    howpublished = {\url { http://gcc.gnu.org/onlinedocs/gccint/SSA.html }},
    note = {Retrieved: 23 Oct. 2013}
}
@misc{llvm-sreedhar,
    title = {Source code of The { LLVM } Compiler Infrastructure},
    howpublished = {\url { http://llvm.org/viewvc/llvm-project/llvm/trunk/lib/Transforms/Utils/PromoteMemoryToRegister.cpp?revision=189169&view=markup }},
    note = {Revision 189169, 24 Aug.\ 2013}
}
@misc{aebi18bachelorarbeit,
    title = {Ausrollen von Schleifen f{\"u}r Zwischensprachen in LCSSA-Form},
    year = {2018},
    month = jun,
    author = {Elias Aebi},
    school = {Karlsruher Institut f{\"u}r Technologie (KIT)},
    institution = {IPD Snelting},
}
@book{aho_ullman_1979,
    place = {Amsterdam},
    title = {Principles of compiler design},
    publisher = {Addison-Wesley},
    author = {Aho, Alfred V. and Ullman, Jeffrey D.},
    year = {1979}
}
@ONLINE{fog_2018,
    title = {Optimizing subroutines in assembly language},
    url = {https://www.agner.org/optimize/optimizing_assembly.pdf},
    publisher = {Technical University of Denmark},
    author = {Fog, Agner},
    year = {2018},
    month = {Apr}
}

@Article{Sarkar2001,
    author="Sarkar, Vivek",
    title="Optimized Unrolling of Nested Loops",
    journal="International Journal of Parallel Programming",
    year="2001",
    month="Oct",
    day="01",
    volume="29",
    number="5",
    pages="545--581",
    abstract="Loop unrolling is a well known loop transformation that has been used in optimizing compilers for over three decades. In this paper, we address the problems of automatically selecting unroll factors for perfectly nested loops, and generating compact code for the selected unroll factors. Compared to past work, the contributions of our work include (i) a more detailed cost model that includes register locality, instruction-level parallelism and instruction-cache considerations; (ii) a new code generation algorithm that generates more compact code than the unroll-and-jam transformation; and (iii) a new algorithm for efficiently enumerating feasible unroll vectors. Our experimental results confirm the wide applicability of our approach by showing a 2.2{\texttimes} speedup on matrix multiply, and an average 1.08{\texttimes} speedup on seven of the SPEC95fp benchmarks (with a 1.2{\texttimes} speedup for two benchmarks). Larger performance improvements can be expected on processors that have larger numbers of registers and larger degrees of instruction-level parallelism than the processor used for our measurements (PowerPC 604).",
    issn="1573-7640",
    doi="10.1023/A:1012246031671",
    url="https://doi.org/10.1023/A:1012246031671"
}

@ONLINE{duff_1983,
    title={Tom Duff on Duff's Device},
    url={http://www.lysator.liu.se/c/duffs-device.html},
    journal={Tom Duff on Duff's Device},
    author={Duff, Tom},
    year={1983},
    month={Nov}
}

@ONLINE{gcc,
    title={loop-unroll.c},
    url={https://github.com/gcc-mirror/gcc/blob/2e966e2a603e7049a9ea24007f03af858407df93/gcc/loop-unroll.c},
    journal={GCC Source Code},
    publisher={GitHub},
    author={mult.}
}

@ONLINE{pmg_2009,
    title={How do I detect unsigned integer multiply overflow?},
    url={https://web.archive.org/web/20190821132916/https://stackoverflow.com/questions/199333/how-do-i-detect-unsigned-integer-multiply-overflow/1514309},
    journal={Stack Overflow},
    author={pmg},
    year={2009},
    month={Oct}
}

@ONLINE{gcc_lcssa,
    title={GCC Internals: LCSSA},
    url={https://gcc.gnu.org/onlinedocs/gccint/LCSSA.html},
    journal={GNU Compiler Collection (GCC)}
}

@ONLINE{cparser,
    url={https://pp.ipd.kit.edu/git/cparser/},
    title={cparser - a C99-Frontend},
    publisher={Karlsruhe Institute of Technology}
}

@ONLINE{libfirm-unroll-static,
    url={https://pp.ipd.kit.edu/git/libfirm/},
    title={cparser - Graph-Based Intermediate Representation},
    publisher={Karlsruhe Institute of Technology},
    note={Commit 2ba5f6e3246a1ae7905857f04b116dc880c2e040}
}

@misc{helmer10studienarbeit,
    title = {Entwicklung von Kriterien zur Anwendung von Schleifenoptimierungen
 im Kontext SSA-basierter Zwischensprachen},
    year = {2010},
    month = oct,
    author = {Christian Helmer},
    school = {Karlsruher Institut f{\"u}r Technologie (KIT)},
    institution = {IPD Snelting},
}

@INBOOK{aho_2014,
    place={Harlow}, 
    edition={2}, 
    title={Compilers: principles, techniques, and tools}, 
    publisher={Pearson}, 
    author={A.V. Aho and Monica S. Lam and R. Sethi and Jeffrey D. Ullman},
    pages = {632--637},
    isbn = "9781292024349",
    year={2014}
}