Complete Program Synthesis for Linear Arithmetic

Synthesis of programs or their fragments is a way to write programs by providing only their meaning without worrying about the implementation details. It avoids the drawback of writing sequential code, which might be difficult 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 algorithms for Linear Rational Arithmetic, Linear Integer Arithmetic and Parametrized Linear Integer Arithmetic. Our implementation and the associated Scala compiler plug-in have been used to implement Boolean Algebra for Presburger Arithmetic synthesis.