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.


Advisor(s):
Kuncak, Viktor
Piskac, Ruzica
Jobstmann, Barbara
Year:
2010
Keywords:
Laboratories:




 Record created 2010-01-19, last modified 2018-01-28

External link:
Download fulltext
n/a
Rate this document:

Rate this document:
1
2
3
 
(Not yet reviewed)