Xiaokang Qiu

Assistant Professor

I am an assistant professor with the School of Electrical and Computer Engineering at Purdue University. I used to be a postdoc at MIT CSAIL, sponsored by ExCAPE and working with Jeff Foster and Armando Solar-Lezama. I received my Ph.D. in Computer Science in 2013 from the University of Illinois at Urbana-Champaign, where I was advised by Madhusudan Parthasarathy. 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.

I look for smart, motivated, hard-working students. If you are interested in working with me, I will be more than happy to talk with you!

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

EE 334C
Purdue University
School of Electrical and Computer Engineering
465 Northwestern Avenue
West Lafayette, IN 47907-2035
phone: +1 765 494 9987

Selected Publications


Purdue ECE573: Compilers and Translator Writing Systems (Spring 2017)
Purdue ECE468: Introduction to Compiler and Translation Systems Engineering (Fall 2016)
MIT 6.885: Introduction to Principles and Practice of Software Synthesis (Spring 2015)
Guest Instructor
MIT 6.820: Foundations of Program Analysis (Fall 2015)

Professional Service

Program Committee
VMCAI 2018, NASAC 2017, APLAS 2017, ATVA 2017, ICSE 2017 (Demonstrations), SATE 2016, TrustSoft 2016, POPL 2016 (ERC), PLDI 2015 (ERC), VMCAI 2015
Conference Session Chair
VMCAI 2015
Journal Reviewer
ACM TACO, 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 deductive framework against separation logic specifications for C programs based on natural proofs. The tool is available here.
ImpSynt Program Synthesizer
ImpSynt is a syntax-guided program synthesizer that can automatically synthesizes data-structure manipulations and their correctness proofs in tandem, from bare-bones control flow skeletons. Some examples can be found here.
PASKET Model Synthesizer
PASKET ("PAttern SKETcher") is a tool for automatically generating Java framework models for symbolic execution. The tool is available here.
JSketch Java Program Synthesizer
JSketch is a sketch-based Java program synthesizer built on top of Sketch. The tool was presented at ESEC/FSE 2015 and available here.


My Erdös number is at most 4.