Jinseong Jeon     

Software Engineer @ Google
Ph.D. / PLUM / CS / UMD (e-mail : jsjeon at (cs dot)? umd dot edu)

What excite me are programs that input and/or output programs. In particular, I am interested in developing tools and techniques that complete partial programs; analyze programs' behaviors; enhance the security of programs; and improve the performance of programs. My research has spanned:

Program Synthesis
creates a program that conforms to the given specification
Symbolic Execution
simulates a program with symbolic inputs
Binary Rewriting
parses; manipulates; and (re)generates a binary program
Compiler Optimization
outputs a faster program that utilizes the target machine

Projects

Pasket

  • Synthesizing Framework Models for Symbolic Execution   

    Researched and developed scalable synthesis of models for object-oriented, event-driven frameworks, such as Java Swing and Android, that enable symbolic execution tools to analyze real-world apps effectively and efficiently

  • Adaptive Concretization for Parallel Program Synthesis   

    Designed, implemented, and thoroughly evaluated a hybrid program synthesis algorithm that adaptively combines the best of symbolic and explicit search and can be naturally run in parallel

  • JSketch: Sketching for Java   

    Developed a Java front-end for Sketch synthesis tool, which inputs partial Java program, along with specification and/or input-output samples, then outputs a compilable, complete Java program that complies with the given specification

    • redexer

  • Dalvik Bytecode Instrumentation Framework   

    Developed a general-purpose bytecode rewriting framework for Android, which is composed of a rich set of utilities that let programmers parse, manipulate, and generate Dalvik bytecode from scratch

  • Driving Apps to Test the Security of Third-Party Components   

    Designed and implemented a static analysis that extracts program execution paths from app’s entry points to method calls of interest, e.g., authorization APIs in Facebook SDK, which are in turn used to steer apps so as to test security properties of third-party components in a large scale

    • SymDroid

  • Symbolic Execution for Dalvik Bytecode   

    Developed a symbolic execution engine for Android apps, which explores apps’ possible behaviors and discovers under what circumstance apps may disclose which sensitive user data

    • Troyd

  • Integration Testing Framework for Android   

    Developed a script-based testing framework for Android that allows testers to run Android apps via command-line interface; record testing scenarios; and replay recorded scenarios as regression tests

    • RTFA

  • Layout Transformation for Heap Objects   

    Developed a compiler optimization that infers data structure access patterns and transforms heap layouts to improve program performance by increasing cache hit ratios (won an Outstanding Master’s Thesis Award from the department)

    • Experience

    Google Feb 2016 ~ Current Software Engineer

    Android Compiler Toolchain:
  • Kotlin compiler (contributions)
  • D8 dexer and R8 shrinker (contributions)
    • Google Compute Engine:
  • Sole-tenant nodes
  • Committed use discounts

    • Google May ~ Aug 2015 Software Engineering Intern

    Espresso Test Recorder: Designed and prototyped an Android Studio plug-in that records user interactions via instrumentation and synthesizes repeatable Espresso test code from the logs

    Microsoft Research May ~ Aug 2014 Research Intern

    Researched automatic creation of platform-to-platform mappings (e.g., Android to Windows Phone) by logging example apps’ behaviors and summarizing them via template-based program synthesis

    Agency for Defense Development Feb 2007 ~ Jul 2010 Researcher

    • Worked with an ELINT (ELectric INTelligence) team to build a pod-style ELINT system,
    • Researched an adaptive way to test the system with a minimal number of input RF signals ,
    • Designed a compact, hard-to-decompose data format for ELINT system missions, and
    • Developed a passive geo-location algorithm for RF signals.