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