Hyunjoon Kim

I like the many ways a program can be run. An abstract interpreter runs it over sound approximations; a symbolic executor runs it on symbols and collects path conditions; a runtime monitor runs it on concrete inputs and carries along information that the program itself never exposes. I see these techniques as different expressions of a common idea, interpretation, and find their connections beautiful.

This fascination with methods first drew me to research. Through research, however, I have come to appreciate something equally important: finding problems worth solving. I still love studying the foundations of these techniques, but I also want to understand real problems and find elegant, principled ways to solve them.

So far, my research has focused on ECMA-262, the JavaScript language specification. I have worked on making static type analysis of the specification precise and using that analysis to synthesize conformance tests. I am currently developing test oracles from a runtime verification perspective: using the mechanized specification as a reference, they propagate differences that existing tests overlook until those differences become observable, revealing more bugs.