Xiaokang Qiu

Postdoctoral Associate

I am a postdoc at MIT, sponsored by ExCAPE and working with Jeff Foster and Armando Solar-Lezama. I used to be a PhD student in computer science at the University of Illinois at Urbana-Champaign, where I was advised by Madhusudan Parthasarathy. I have graduated in the Summer of 2013. Before starting my studies at the University of Illinois I completed my Master studies at Nanjing University, China in the group of Xuandong Li.

My research interests span a range of areas in Programming Languages and Software Engineering, with focus on theories, algorithms and tools of Programming Systems, including program logics, decision procedures, automated deduction, program verification, and program synthesis.

If you need to contact me, the easiest way to do that is by email to "xkqiu" at the domain "csail.mit.edu". You can also visit me at my office:

MIT Computer Science & Artificial Intelligence Lab (CSAIL)
32 Vassar Street
Cambridge, MA 02139
phone: +1 617-253-0945

Selected Publications


MIT 6.885: Introduction to Principles and Practice of Software Synthesis (Spring 2015)
Head Teaching Assistant
UIUC CS373: Theory of Computation (Fall 2011, Fall 2010)
Teaching Assistant
UIUC CS373: Theory of Computation (Spring 2010)
UIUC CS105: Introduction to Computing with Application to Business and Commerce (Fall 2009)
NJU CS: Symbolic Logic (Fall 2004)

Professional Service

Program Committee
POPL 2016 (ERC), PLDI 2015 (ERC), VMCAI 2015
Conference Session Chair
VMCAI 2015
Journal Reviewer
ACM TOPLAS, Software: Practice and Experience
Conference Reviewer
CADE-25 (2015), CAV 2015, PLDI 2014, ESOP 2013, ATVA 2012, CAV 2011

Software Projects

STRAND Logic Solver
STRAND ("STRucture ANd Data") is a logic that allows reasoning with heap-manipulating programs using deductive verification and SMT solvers. More details can be found here.
VCDryad Program Verifier
VCDryad extends the VCC framework to provide an automated de- ductive framework against separation logic specifications for C programs based on natural proofs. More details can be found here.
ImpSketch Program Synthesizer
ImpSketch is a language that enables a novel verification-synthesis inte- gration, and produces provably-correct data-structure manipulations. More details can be found in this draft.
PASKET Model Synthesizer
PASKET ("PAttern SKETcher") is a tool for automatically generating models of event-driven Java frameworks by design pattern matching. More details can be found in this draft.


My Erdös number is at most 4.