Viktor Kuncak, Philippe Paul Henri Suter, Ali Sinan Köksal
We present a semi-decision procedure for checking satisfiability of formulas in the language of algebraic data types and integer linear arithmetic extended with user-defined terminating recursive functions. Our procedure is designed to integrate into a DPL ...
2010