Xiaokang Qiu

Postdoctoral Associate

I am a postdoc sponsored by ExCAPE, 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. I studied logic, automated deduction and program verification with 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.

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

Professional Activities

Program Committee
PLDI 2015 (ERC), VMCAI 2015
Journal Reviewer
ACM TOPLAS, Software: Practice and Experience
Conference Reviewer
PLDI 2014, ESOP 2013, ATVA 2012, CAV 2011


Strand: A logic combining heap structures and data
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.
Dryad: Recursive proofs for inductive tree data-structures
Dryad is a dialect of separation logic with recursive definitions. Dryad provides natural proofs for general properties of structure, data, and separation. More details can be found here.
Pasket: a PAttern SKETcher
Pasket is a tool for synthesizing models of the observer pattern for event-driven frameworks. More details can be found in this draft.


My Erdös number is at most 4.
Valid XHTML 1.0! Valid CSS!