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 Ph.D. students and undergraduate interns. 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 329
Purdue University
School of Electrical and Computer Engineering
465 Northwestern Avenue
West Lafayette, IN 47907-2035
phone: +1 765 494 9987
Recent News
- May 2021:
- Invited to serve on PLDI 2022 Program Committee. Consider submitting a paper!
- March 2021:
- Invited to serve on APLAS 2021 Program Committee. Consider submitting a paper!
- February 2021:
- Received an NSF CAREER Award.
- November 2020:
- Our paper on reasoning about recursive tree traversals accepted to PPoPP 2021.
Received the Seed for Success Award from Purdue University.
- October 2020:
- Elevated to Senior Member of the ACM.
- June 2020:
- Our vision paper on grand challenges in resilience accepted to IEEE Open Journal of the Computer Society.
- February 2020:
- Our paper on Cooperative Synthesis (implemented as the DryadSynth solver) (conditionally) accepted to PLDI 2020.
- September 2019:
- Our paper on Comparative Synthesis accepted to HotNets 2019.
- August 2019:
- Received a seed grant (PI, ~$30K) from PurPL.
Invited to serve on CAV 2020 Program Committee. Consider submitting a paper!
- July 2019:
- Our paper on JLibSketch accepted to OOPSLA 2019.
Received an SPX award (co-PI, $1.25M) from the NSF.
Our SyGuS solver DryadSynth wins the CLIA track of SyGuS-COMP 2019!
Selected Publications
-
Reasoning About Recursive Tree Traversals
Yanjun Wang, Jinwei Liu, Dalin Zhang, Xiaokang Qiu
In Proc. 25th ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming (PPoPP '21), 2021. (Acc rate: 21%)
(
Postprint)
(
ACM DL via DOI)
(
GitHub)
-
Reconciling Enumerative and Deductive Program Synthesis
Kangjing Huang, Xiaokang Qiu, Peiyuan Shen, Yanjun Wang
In Proc. 41st ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI '20), 2020. (Acc rate: 22%)
(
PDF via ACM Author-izer © ACM)
(
ACM DL via DOI)
(
Postprint)
(
Slides)
(
GitHub)
-
Learning Network Design Objectives Using A Program Synthesis Approach
Yanjun Wang, Chuan Jiang, Xiaokang Qiu, Sanjay G. Rao
In Proc. 18th ACM Workshop on Hot Topics in Networks (HotNets '19), 2019. (Acc rate: 20%)
(
PDF via ACM Author-izer © ACM)
(
ACM DL via DOI)
(
Postprint)
(
Slides)
-
Program Synthesis with Algebraic Library Specifications
Benjamin Mariano, Josh Reese, Siyuan Xu, ThanhVu Nguyen, Xiaokang Qiu, Jeffrey S. Foster, Armando Solar-Lezama
In Proc. 2019 ACM SIGPLAN International Conference on Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA '19), 2019. (Acc rate: 35%)
(
PDF via ACM Author-izer © ACM)
(
ACM DL via DOI)
-
A Decidable Logic for Tree Data-Structures with Measurements
Xiaokang Qiu, Yanjun Wang
In Proc. 20th International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI '19), LNCS 11388, 2019. (Acc rate: 43%)
(
PDF (preprint) © Springer)
(
SpringerLink via DOI)
(
Slides)
-
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%)
(
PDF via ACM Author-izer © ACM)
(
ACM DL via DOI)
(
Slides)
(
GitHub)
-
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)
(
GitHub)
-
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%)
-
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.
-
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.
-
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%)
-
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.
-
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.
Teaching
- Instructor
- Purdue ECE663: Advanced Compilation and Automatic Programming (Spring 2018, Spring 2021)
Purdue ECE573: Compilers and Translator Writing Systems (Fall 2017, Spring 2017, Fall 2018, Fall 2019, Fall 2020)
Purdue ECE468: Introduction to Compiler and Translation Systems Engineering (Fall 2016, Fall 2018, Fall 2019, Fall 2020)
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
- CAV 2020, SATE 2019, PLDI 2019 SRC, APLAS 2018, ATVA 2018, SATE 2018, NASAC 2018 (Safety and Security of System Software track), PLDI 2018 (ERC), 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
- CAV 2020, VMCAI 2019, VMCAI 2015
- Journal Reviewer
- ACM TACO, ACM TOPLAS, Software: Practice and Experience
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 enumerative synthesis and deductive synthesis algorithms. DryadSynth won the CLIA track of SyGuS-COMP in 2018 and 2019. The solver was presented at PLDI 2020 and available at: