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

Time: 13:00

Venue: room 3248, Faculty of Mathematics and Mechanics, Saint Petersburg State University, Stary Peterhof, Universitetski pr., 28