A. W. Appel. SSA is functional programming. SIGPLAN Not., 33(4):17-20, Apr. 1998.
 S. Bansal and A. Aiken. Automatic generation of peephole superoptimizers. In Proceedings of the 12th International Conference on Architectural Support for Programming Languages and Operating Systems, pages 394-403, 2006.
 C. Barrett, A. Stump, and C. Tinelli. The SMT-LIB Standard: Version 2.0. In A. Gupta and D. Kroening, editors, Proceedings of the 8th International Workshop on Satisfiability Modulo Theories, 2010.
 S. Buchwald. Optgen: A Generator for Local Optimizations, pages 171-189. London, UK, Apr. 2015. [OpenAIRE]
 C. Cadar, D. Dunbar, and D. Engler. KLEE: Unassisted and automatic generation of high-coverage tests for complex systems programs. In Proceedings of the 8th USENIX Conference on Operating Systems Design and Implementation, OSDI'08, pages 209-224, 2008.
 R. Cytron, J. Ferrante, B. K. Rosen, M. N. Wegman, and F. K. Zadeck. Efficiently computing static single assignment form and the control dependence graph. ACM Trans. Program. Lang. Syst., 13(4):451-490, Oct. 1991.
 W. Dietz, P. Li, J. Regehr, and V. Adve. Understanding integer overflow in C/C++. ACM Trans. Softw. Eng. Methodol., 25(1): 2:1-2:29, Dec. 2015. [OpenAIRE]
 C. W. Fraser. A compact, machine-independent peephole optimizer. In Proceedings of the 6th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages, POPL '79, pages 1-6, 1979.
 T. Granlund and R. Kenner. Eliminating branches using a superoptimizer and the GNU C Compiler. In Proceedings of the ACM SIGPLAN 1992 Conference on Programming Language Design and Implementation, pages 341-352, 1992. [OpenAIRE]
 S. Gulwani, S. Jha, A. Tiwari, and R. Venkatesan. Synthesis of loop-free programs. In Proceedings of the 32nd ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI '11, pages 62-73, 2011.
 R. R. Kessler. Peep: An architectural description driven peephole optimizer. In Proceedings of the 1984 SIGPLAN Symposium on Compiler Construction, pages 106-110, 1984.
 C. Lattner and V. Adve. LLVM: A compilation framework for lifelong program analysis & transformation. In Proceedings of the International Symposium on Code Generation and Optimization: Feedback-directed and Runtime Optimization, pages 75-88, 2004. [OpenAIRE]
 X. Leroy. Formal verification of a realistic compiler. Commun. ACM, 52(7):107-115, July 2009. [OpenAIRE]
 N. P. Lopes, D. Menendez, S. Nagarakatte, and J. Regehr. Provably correct peephole optimizations with Alive. In Proceedings of the 36th ACM SIGPLAN Conference on Programming Language Design and Implementation, pages 22-32, 2015.
 H. Massalin. Superoptimizer: A look at the smallest program. In Proceedings of the Second International Conference on Architectual Support for Programming Languages and Operating Systems, pages 122-126, 1987. [OpenAIRE]