Complete Program Synthesis for Linear Arithmetics

by Mikael Mayer Program synthesis, or their fragments, is a way to write programs by providing only its meaning, without worrying about the implementation details. It avoids the drawback of writing sequential code, which might be di cult to check, error-prone or tedious. Our contribution is to provide complete program synthesis algorithms with unbounded data types in decidable theories. We present synthesis examples and our synthesis algorithms for Linear Integer Arithmetic and Parametrized Linear Integer Arithmetic.