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. Please apply to Purdue's strong Computer Engineering Programs. 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

Recent News

March 2018:

Invited to give a talk at GCASR 2018.
Invited to serve on SATE 2018 Program Committee. Consider submitting a paper!

February 2018:

Invited to serve on APLAS 2018 Program Committee. Consider submitting a paper!

January 2018:

Invited to serve on ATVA 2018 Program Committee. Consider submitting a paper!
Ph.D. student Yanjun Wang wins the runner-up prize in the ACM Student Research Competition (SRC) held at POPL 2018. Congrats, Yanjun!

December 2017:

Invited to serve on NASAC 2018 Program Committee. Consider submitting a paper!

August 2017:

Invited to serve on PLDI 2018 External Review Committee. Consider submitting a paper!
Our paper on "Natural Synthesis" accepted to OOPSLA 2017.
Invited to participate Shonan Meeting on Analysis and Verification of Pointer Programs.

July 2017:

Our SyGuS solver DryadSynth got a runner-up place in the Invariant track of SyGuS-COMP 2017.

May 2017:

Invited to serve on VMCAI 2018 Program Committee. Consider submitting a paper!

April 2017:

Invited to serve on APLAS 2017 Program Committee. Consider submitting a paper or a tool!

February 2017:

Our paper on "Adaptive Concretization" accepted to Formal Methods in System Design.

Selected Publications

• Natural Synthesis of Provably-Correct Data-Structure Manipulations
  Xiaokang Qiu, Armando Solar-Lezama
  In Proc. 2017 ACM SIGPLAN International Conference on Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA '17), 2017. (Acc rate: 29%)
  (PDF via ACM Author-izer © ACM) (ACM DL via DOI) (Slides)
• An Empirical Study of Adaptive Concretization for Parallel Program Synthesis
  Jinseong Jeon, Xiaokang Qiu, Armando Solar-Lezama, Jeffrey S. Foster
  Formal Methods in System Design, 50(1):75-95, 2017.
  (PDF (preprint) © Springer) (SpringerLink via DOI)
• Synthesis of Recursive ADT Transformers from Reusable Templates
  Jeevana Priya Inala, Nadia Polikarpova, Xiaokang Qiu, Benjamin S. Lerner, Armando Solar-Lezama
  In Proc. 23rd International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS '17), LNCS 10205, 2017. (Acc rate: 27%)
  (PDF (preprint) © Springer) (SpringerLink via DOI)
• Synthesizing Framework Models for Symbolic Execution
  Jinseong Jeon, Xiaokang Qiu, Jonathan Fetter-Degges, Jeffrey S. Foster, Armando Solar-Lezama
  In Proc. 38th International Conference on Software Engineering (ICSE '16), 2016. (Acc rate: 19%)
  Press: (MIT News) (MIT CSAIL Spotlight) (Computerworld) (ACM Technews)
  (PDF via ACM Author-izer © ACM) (ACM DL via DOI) (Slides) (Tool)
• JSketch: Sketching for Java
  Jinseong Jeon, Xiaokang Qiu, Jeffrey S. Foster, Armando Solar-Lezama
  In Proc. 10th Joint Meeting of the European Software Engineering Conference and the ACM SIGSOFT Symposium on the Foundations of Software Engineering (ESEC/FSE '15 Tool demonstrations), 2015. (Acc rate: 43%)
  (PDF via ACM Author-izer © ACM) (ACM DL via DOI) (Tool)
• Adaptive Concretization for Parallel Program Synthesis
  Jinseong Jeon, Xiaokang Qiu, Armando Solar-Lezama, Jeffrey S. Foster
  In Proc. 27th International Conference on Computer Aided Verification (CAV '15), LNCS 9207, 2015. (Acc rate: 27%)
  (PDF (preprint) © Springer) (SpringerLink via DOI)
• Natural Proofs for Data-Structure Manipulation in C using Separation Logic
  Edgar Pek, Xiaokang Qiu, P. Madhusudan
  In Proc. 35th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI '14), 2014. (Acc rate: 18%)
  (PDF via ACM Author-izer © ACM) (ACM DL via DOI)
• Automatic Techniques for Proving Correctness of Heap-Manipulating Programs
  Xiaokang Qiu
  PhD Thesis, University of Illinois at Urbana-Champaign, 2013.
  (PDF © Xiaokang Qiu) (University of Illinois IDEALS)
• Natural Proofs for Structure, Data, and Separation
  Xiaokang Qiu, Pranav Garg, Andrei Stefanescu, P. Madhusudan
  In Proc. 34th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI '13), 2013. (Acc rate: 17%)
  (PDF via ACM Author-izer © ACM) (ACM DL via DOI) (Slides)
• Recursive Proofs for Inductive Tree Data-Structures
  P. Madhusudan, Xiaokang Qiu, Andrei Stefanescu
  In Proc. 39th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL '12), 2012. (Acc rate for PC submissions: 18%)
  (PDF via ACM Author-izer © ACM) (ACM DL via DOI) (Slides)
• Efficient Decision Procedures for Heaps Using STRAND
  P. Madhusudan, Xiaokang Qiu
  In Proc. 18th International Static Analysis Symposium (SAS '11), LNCS 6887, 2011. (Acc rate: 33%)
  (PDF (preprint) © Springer) (SpringerLink via DOI) (Slides)
• Decidable Logics Combining Heap Structures and Data
  P. Madhusudan, Gennaro Parlato, Xiaokang Qiu
  In Proc. 38th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL '11), 2011. (Acc rate: 23%)
  (PDF via ACM Author-izer) (ACM DL via DOI) (Slides)
• UML Interaction Model-Driven Runtime Verification of Java Programs
  Xuandong Li, Xiaokang Qiu, Linzhang Wang, Xin Chen, Zhou Zhou, Liqian Yu, Jianhua Zhao
  IET Software, 5(2):142-156, 2011.
  (IET DL or IEEE Xplore via DOI)
• A Formal Architecture Pattern for Real-Time Distributed Systems
  Abdullah Al-Nayeem, Mu Sun, Xiaokang Qiu, Lui Sha, Steven P. Miller, Darren D. Cofer
  In Proc. 30th IEEE Real-Time System Symposium (RTSS '09), 2009. (Acc rate: 21%)
  (PDF (preprint) © IEEE) (IEEE Xplore via DOI)
• UML Activity Diagram-Based Automatic Test Case Generation for Java Programs
  Mingsong Chen, Xiaokang Qiu, Wei Xu, Linzhang Wang, Jianhua Zhao, Xuandong Li
  The Computer Journal, 52(5):545-556, 2009.
  (Oxford Journals via DOI)
• UML State Machine Diagram Driven Runtime Verification of Java Programs for Message Interaction Consistency
  Xuandong Li, Xiaokang Qiu, Linzhang Wang, Bin Lei, W. Eric Wong
  In Proc. 23rd ACM Symposium on Applied Computing (SAC '08), 2008. (Acc rate: 29%)
  (PDF via ACM Author-izer) (ACM DL via DOI)
• Runtime Verification of Java Programs for Scenario-Based Specifications
  Xuandong Li, Linzhang Wang, Xiaokang Qiu, Bin Lei, Jiesong Yuan, Jianhua Zhao, Guoliang Zheng
  In Proc. 11th Ada-Europe International Conference on Reliable Software Technologies (Ada-Europe '06), LNCS 4006, 2006.
  (SpringerLink via DOI)
• Automatic Test Case Generation for UML Activity Diagrams
  Mingsong Chen, Xiaokang Qiu, Xuandong Li
  In Proc. 1st International Workshop on Automation of Software Test (AST '06), 2006.
  (PDF via ACM Author-izer) (ACM DL via DOI)

Teaching

Professional Service

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 at

(Tool Website) (Paper)

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 at:

(Tool Website) (GitHub) (Paper)

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 at:

(GitHub) (Paper)

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 at:

(Tool Website) (GitHub) (Paper)

DryadSynth SyGuS Solver

DryadSynth is a Syntax-Guided Synthesis (SyGuS) solver that combines explicit search and symbolic search. DryadSynth got a runner-up place in the Invariant track of SyGuS-COMP 2017, the 4th Syntax-Guided Synthesis Competition. The solver was presented at SYNT 2017 and available at:

(GitHub) (Paper)

Misc

My Erdös number is at most 4.