Daejun Park

From FSL
Revision as of 03:27, 1 May 2015 by Dpark69 (Talk | contribs)

Jump to: navigation, search

I am a PhD student working with Prof. Grigore Rosu. I am interested in helping to develop reliable software. Currently, I am working on JavaScript program verification.

Here is my CV.


  • 2107 Thomas M. Siebel Center for Computer Science, 201 North Goodwin Avenue, Urbana, IL 61801-2302
  • Email: dpark69 AT illinois DOT edu


A Complete Formal Semantics of x86-64 User-Level Instruction Set Architecture 
Sandeep Dasgupta and Daejun Park and Theodoros Kasampalis and Vikram S. Adve and Grigore Rosu
PLDI'19, ACM, pp 1133-1148. 2019
PDF, Slides(PDF), Semantics, DOI, PLDI'19, BIB
A Language-Independent Approach to Smart Contract Verification 
Xiaohong Chen and Daejun Park and Grigore Rosu
ISoLA'18, Springer, pp 405-413. 2018
PDF, Slides(PPTX), Formally Verified Smart Contracts, DOI, ISoLA'18, BIB
A Formal Verification Tool for Ethereum VM Bytecode 
Daejun Park and Yi Zhang and Manasvi Saxena and Philip Daian and Grigore Rosu
ESEC/FSE'18, ACM, pp 912-915. 2018
PDF, Slides(PDF), Formally Verified Smart Contracts, DOI, ESEC/FSE'18, BIB
KEVM: A Complete Semantics of the Ethereum Virtual Machine 
Everett Hildenbrandt and Manasvi Saxena and Xiaoran Zhu and Nishant Rodrigues and Philip Daian and Dwight Guth and Brandon Moore and Yi Zhang and Daejun Park and Andrei Stefanescu and Grigore Rosu
CSF 2018, IEEE, pp 204-217. 2018
Semantics-Based Program Verifiers for All Languages 
Andrei Stefanescu and Daejun Park and Shijiao Yuwen and Yilong Li and Grigore Rosu
OOPSLA'16, ACM, pp 74-91. 2016
PDF, Slides(PDF), Matching Logic, DOI, OOPSLA'16, BIB
KJS: A Complete Formal Semantics of JavaScript 
Daejun Park and Andrei Stefanescu and Grigore Rosu
PLDI'15, ACM, pp 346-356. 2015
PDF, Slides(PDF), Semantics, DOI, PLDI'15, BIB

Personal tools