A Practical Approach to Partial Functions in CVC Lite. - Sergey Berezin; Clark W. Barrett; Igor Shikanian; Marsha Chechik; Arie Gurfinkel; David L. Dill (D/PDPAR@IJCAR, 2004)

An Abstract Decision Procedure for Satisfiability in the Theory of Recursive Data Types. - Clark W. Barrett; Igor Shikanian; Cesare Tinelli (PDPAR/PaUL@FLoC, 2006)

An Abstract Decision Procedure for a Theory of Inductive Data Types. - Clark W. Barrett; Igor Shikanian; Cesare Tinelli (J. Satisf. Boolean Model. Comput., 2007)