Kuat Yessenov

Kuat Yessenov

I was a Computer Science PhD student at MIT advised by Prof. Armando Solar-Lezama. My thesis was about automating tedious programming tasks using execution trace data and live demonstrations.

In the past, I have completed Master of Engineering degree at MIT under supervision of Prof. Daniel Jackson and had a great time working with Prof. Viktor Kuncak at EPFL and K. Rustan M. Leino at Microsoft Research.

I was a teaching assistant for Elements of Software Construction (known as 6.005, the main introductory software engineering course at MIT) twice in Spring 2009 and Fall 2008.



Publications [bib]

[1] Kuat Yessenov, Shubham Tulsiani, Aditya Krishna Menon, Robert C. Miller, Sumit Gulwani, Butler W. Lampson, and Adam Kalai, A colorful approach to text processing by example, UIST, 2013. [ full ]
[2] K. Rustan M. Leino and Kuat Yessenov, Stepwise refinement of heap-manipulating code in Chalice, Formal Aspects of Computing, 2012. [ talk | full ]
[3] Jean Yang, Kuat Yessenov, and Armando Solar-Lezama, A language for automatically enforcing privacy policies, POPL, 2012. [ full ]
[4] Kuat Yessenov, Zhilei Xu, and Armando Solar-Lezama, Data-driven synthesis for object-oriented frameworks, OOPSLA, 2011. [ talk | full ]
[5] Aleksandar Milicevic, Derek Rayside, Kuat Yessenov, and Daniel Jackson, Unifying execution of imperative and declarative code, ICSE, 2011. [ full ]
[6] Kuat Yessenov, Ruzica Piskac, and Viktor Kuncak, Collections, cardinalities, and relations, VMCAI, 2010. [ talk | full ]
[7] Derek Rayside, Aleksandar Milicevic, Kuat Yessenov, Greg Dennis, and Daniel Jackson, Agile specifications, OOPSLA Onward!, 2009. [ full ]
[8] Kuat Yessenov, A light-weight specification language for bounded program verification, Master's thesis, MIT, 2009. [ full ]
[9] Greg Dennis, Kuat Yessenov, and Daniel Jackson, Bounded verification of voting software, VSTTE, 2008. [ full ]


Using SMT solvers for deductive synthesis of cache-oblivious dynamic-programming algorithms
Data-Driven Program Synthesis
Using SMT solvers for constraint programming in Scala
Stepwise refinement of heap-manipulating code in Chalice
Unified execution of declarative and imperative code in Squander
General purpose SAT-powered bounded model checking of Java code in JForge Eclipse Plug-in
A JML front-end for Forge bounded verification called JMLForge
Course Projects


This GPG public key belongs to me. I enjoy cycling and have raced for MIT Cycling.
© Kuat Yessenov (also spelled as Kuat Esenov, Kuat Yesenov, Куат Есенов, Қуат Есенов)