I am a graduate student in computer science at the University of Illinois at Urbana-Champaign. I started in Fall 2007 and I am studying logic, automated deduction and program verification with 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.

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

3240 Siebel Center
201 N Goodwin Ave
Urbana, IL 61801
phone: +1-(217)-333-5219

Selected Publications

• Natural Proofs for Structure, Data, and Separation
  Xiaokang Qiu, Pranav Garg, Andrei Stefanescu, P. Madhusudan
  To appear on 34th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI '13), 2013.
  (PDF (preprint) © ACM)
• 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-Verlag) (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)

Projects

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).

Misc

My Erdös number is at most 4.