I am a PhD student in CSAIL working in Computer Aided Programming group. I am interested in programming languages, light-weight formal methods, verification, decision procedures, and program synthesis. I am advised by Prof. Armando Solar-Lezama.
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.
Publications
- [1]
- Jean Yang, Kuat Yessenov, and Armando Solar-Lezama, A language for automatically enforcing privacy policies, POPL, 2012. [ PDF ]
- [2]
- Kuat Yessenov, Zhilei Xu, and Armando Solar-Lezama, Data-driven synthesis for object-oriented frameworks, OOPSLA, 2011. [ slides | PDF ]
- [3]
- Aleksandar Milicevic, Derek Rayside, Kuat Yessenov, and Daniel Jackson, Unifying execution of imperative and declarative code, ICSE, 2011. [ PDF ]
- [4]
- K. Rustan M. Leino and Kuat Yessenov, Automated stepwise refinement of heap-manipulating code, 2010. [ PDF ]
- [5]
- Kuat Yessenov, Ruzica Piskac, and Viktor Kuncak, Collections, cardinalities, and relations, VMCAI, 2010. [ slides | PDF ]
- [6]
- Derek Rayside, Aleksandar Milicevic, Kuat Yessenov, Greg Dennis, and Daniel Jackson, Agile specifications, OOPSLA Onward!, 2009. [ PDF ]
- [7]
- Kuat Yessenov, A light-weight specification language for bounded program verification, Master's thesis, MIT, 2009. [ PDF ]
- [8]
- Greg Dennis, Kuat Yessenov, and Daniel Jackson, Bounded verification of voting software, VSTTE, 2008. [ PDF ]
[bib]
Teaching
I was a teaching assistant for Elements of Software Construction (known as 6.005) in Spring 2009 and Fall 2008.
Projects
I contributed to the following projects:
- 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.
Stuff
I have a GPG public key.
I enjoy travelling and so far have visited these countries.
Last modified: Monday, 23-Apr-2012 11:21:59 EDT