My Third PLDI

Hi all,

I am Xin Zhang, a third year Ph.D from Georgia Tech. I have been fortunate to attend PLDI since my first year with the generous support from my advisor Mayur Naik, SIGPLAN and NSF.

PLDI has always been a major festival of the year for me. Not only is it a chance to hear talks on top-quality publications of our field, but it is also a rare chance to meet people in the community. Every time after PLDI, I always got back with fresh ideas and energies to work on research. I am confident I will feel the same after this PLDI.

Our group has two papers accepted at PLDI this time, and I am one of the authors for both papers.

"On abstraction refinement for program analyses in Datalog" proposes a novel counterexample-guided refinement (CEGAR) based approach via partial MAXSAT which automatically searches efficient abstractions for a given program analysis in Datalog. For a given query like a aliasing check (v!=u), our approach will either find a cheapest abstraction which proves this query or conclude that there is no abstraction in the space that can prove the query. The key observation here is that there is a natural connection between Datalog and SAT formula. Each grounded Datalog rule is basically a Horn clause. By encoding the derivations in Datalog as the hard constraints in MAXSAT, our approach successfully avoids all the counterexamples. By encoding the cost of the abstractions as weights of soft constraints in MAXSAT, our approach effectively chooses the cheapest abstraction while avoiding all the unviable abstractions.

"Hybrid top-down and bottom-up interprocedural analysis" introduces a novel interprocedural analysis framework which combines conventional top-down analysis and bottom-up analysis, and outperforms both empirically.

I am looking forward to seeing you guys at PLDI!

-Xin