IMFUFA Seminar: Program Inversion by Maja Kirkeby (RUC/IMT)
Given a specification of the known input and output arguments of a program, a program inverter creates a new program where the known arguments are input, and the rest is output. There are three kinds of program inversions, namely full inversion, partial inversion and semi-inversion, where semi-inversion is the most general one. If p is a program with two inputs (x,y) and two outputs (u,v), then the three forms of inversion can be illustrated as follows.
p(x,y) = <u,v> == full inversion ==> p'(u,v) = <x,y>
p(x,y) = <u,v> == partial inversion ==> p'(x,u,v) = <y>
p(x,y) = <u,v> == semi inversion ==> p('x,v) = <u,y>
Full inversion swaps the entire input and output, partial inversion swaps parts of the input and the entire output, and semi-inversion allows parts of the input and output to be swapped. Important applications include the full inversion of lossless encoders, e.g., encode(data) = code into decode(code) = data, the partial inversion of symmetric encrypters, inverting, e.g., encrypt(key; data) = code into decrypt(key; code) = data, and the semiinversion of equation systems to isolate the unknown variables.
Program inversion algorithms are often tightly connected to a particular programming language, and instead, we use conditional constructor term rewriting systems; these systems model reversible, functional and declarative languages. In this talk, we present and discuss inverters developed for these rewrite systems.
The seminar is open for everyone, no registration needed.