|
Research Interests
- Program analysis, abstract interpretation, program verification
- Program Synthesis
- Programming Languages, compiler construction, software engineering
Current Projects
- Saint: Synthesis using Abstract Interpretation (TACAS'09) (EC2 '09) (SPIN '09) (POPL'10) (PODC'10)
- Fender: Preserving Correctness under Weak Memory Models (FMCAD'10)(PLDI'11)(PLDI'12)
- Dojo: Ensuring Determinism of Concurrent Systems
(SAS '10) (RV'10
)(PLDI'12)
- PET: Parallelism-Enabling Toolset (OOPSLA'11-a)(OOPSLA'11-b)
Completed Projects
- QVM: The quality virtual machine (OOPSLA'08) (PLDI'09) (ISMM'10) (OOPSLA'11)
- Paraglide: Search-Based Synthesis of Concurrent Programs (PLDI'06) (PLDI'07) (PLDI'08) (EC2 '08)
- SAFE: scalable verification for heap-manipulating programs
(ISSTA'06
)
(ISSTA'07
) (POPL'08) (ISMM'08) (ISSTA'08) (TSE'08) (TOSEM'08) (Mining'11) (Exp'11) - 3VMC: shape analysis for concurrent programs (POPL'01) (SOFTMC'03) (ESOP'03) (PLDI'04) (IGPL'08) (TOPLAS'10)