Bounded Verification of Voting Software. - Greg Dennis; Kuat Yessenov; Daniel Jackson 001 (VSTTE, 2008)

Agile specifications. - Derek Rayside; Aleksandar Milicevic; Kuat Yessenov; Greg Dennis; Daniel Jackson 001 (OOPSLA Companion, 2009)

Collections, Cardinalities, and Relations. - Kuat Yessenov; Ruzica Piskac; Viktor Kuncak (VMCAI, 2010)

Unifying execution of imperative and declarative code. - Aleksandar Milicevic; Derek Rayside; Kuat Yessenov; Daniel Jackson 001 (ICSE, 2011)

Data-driven synthesis for object-oriented frameworks. - Kuat Yessenov; Zhilei Xu; Armando Solar-Lezama (OOPSLA, 2011)

A language for automatically enforcing privacy policies. - Jean Yang 001; Kuat Yessenov; Armando Solar-Lezama (POPL, 2012)

Stepwise refinement of heap-manipulating code in Chalice. - K. Rustan M. Leino; Kuat Yessenov (Formal Aspects Comput., 2012)

A colorful approach to text processing by example. - Kuat Yessenov; Shubham Tulsiani; Aditya Krishna Menon; Robert C. Miller; Sumit Gulwani; Butler W. Lampson; Adam Kalai (UIST, 2013)

Deriving divide-and-conquer dynamic programming algorithms using solver-aided transformations. - Shachar Itzhaky; Rohit Singh 002; Armando Solar-Lezama; Kuat Yessenov; Yongquan Lu; Charles E. Leiserson; Rezaul Alam Chowdhury (OOPSLA, 2016)

Program synthesis from execution traces and demonstrations. - Kuat Yessenov (2016)

DemoMatch: API discovery from demonstrations. - Kuat Yessenov; Ivan Kuraj; Armando Solar-Lezama (PLDI, 2017)