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
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%)
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%)
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. More details can be found 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.