Daejun Park

daejunpark (at) gmail (dot) com

[LinkedIn] [Twitter] [Github]

[DBLP] [Google Scholar]

Language-Parametric Compiler Validation with Application to LLVM.
Theodoros Kasampalis, Daejun Park, Zhengyao Lin, Vikram Adve, and Grigore Rosu.
ASPLOS 2021.
[paper]
End-to-End Formal Verification of Ethereum 2.0 Deposit Smart Contract.
Daejun Park, Yi Zhang, and Grigore Rosu.
CAV (Industrial) 2020.
[paper] [slides] [code]
A Complete Formal Semantics of x86-64 User-Level Instruction Set Architecture.
Sandeep Dasgupta, Daejun Park, Theodoros Kasampalis, Vikram Adve, and Grigore Rosu.
PLDI 2019.
[paper]
A Formal Verification Tool for Ethereum VM Bytecode.
Daejun Park, Yi Zhang, Manasvi Saxena, Philip Daian, and Grigore Rosu.
ESEC/FSE (Tool) 2018.
[paper] [slides] [code]
KEVM: A Complete Formal Semantics of the Ethereum Virtual Machine.
Everett Hildenbrandt, Manasvi Saxena, Nishant Rodrigues, Xiaoran Zhu, Philip Daian, Dwight Guth, Brandon Moore, Daejun Park, Yi Zhang, Andrei Stefanescu, and Grigore Rosu.
CSF 2018.
[paper]
Invariant Synthesis for Incomplete Verification Engines.
Daniel Neider, Pranav Garg, P. Madhusudan, Shambwaditya Saha, and Daejun Park.
TACAS 2018. (Invited to JAR 2020.)
[paper (TACAS)] [paper (JAR)] [code]
Semantics-Based Program Verifiers for All Languages.
Andrei Stefanescu, Daejun Park, Shijiao Yuwen, Yilong Li, and Grigore Rosu.
OOPSLA 2016. Distinguished Paper Award.
[paper] [slides]
KJS: A Complete Formal Semantics of JavaScript.
Daejun Park, Andrei Stefanescu, and Grigore Rosu.
PLDI 2015.
[paper] [slides] [code]