Supercompilation is a method for program transformation, which can be used both for program optimization and discovering and proving program properties. The main counterparts of supercompilation are driving, generalization and folding. Driving is a symbolic execution of a program, which generates (generally speaking infinite) tree, describing all possible states of the program. Generalization is a replacement of a set of states by some more general. Folding --- reduction of a set of sates to early encountered one. Generalization and folding allow to reduce infinite tree into finite graph, which then can be converted into residual program.
As a result of supercompilation, some useful transformations can be carried out:
1. elimination of useless program parts;
2. execution of operations, if their operands are known well enough;
3. turning multi-pass algorithms into single-pass;
4. elimination of intermediate data structures.
Experimental implementations of supercompiler are available online, which makes it possible to investigate their both strong and weak points.
Presenter: Sergey Romamenko, Keldysh Institute for Applied Mathematics, Russian Academy of Science, Moscow.
Date: March 30, 2018
Venue: room 3248, Faculty of Mathematics and Mechanics, Saint Petersburg State University, Stary Peterhof, Universitetski pr., 28