Synthesis for Rational Linear Arithmetic

This is the title of my bachelor thesis, done at EPFL in the Laboratory for Automated Reasoning and Analysis. It was supervised by Viktor Kuncak.

The idea was to write a program that takes as input some specifications, like "choose x such that x < a, and ", for arbitrary parameters a and b. The program would then output code that given a and b returns x satisfying the specifications. For the example above, this would be of the form (in pseudocode):

def f(a,b):
    return min (a,b) - 1

If you are interested, read the final report, or have a look at the program's source code (as always, you should verify its PGP signature).