Daejun Park

From FSL
Revision as of 04:35, 22 January 2015 by Dpark69 (Talk | contribs)

Jump to: navigation, search

I am a PhD student working with Prof. Grigore Rosu. Recently, I defined a complete formal semantics of JavaScript language, based on the latest standard ECMAScript 5.1. Currently, I am working on using the semantics to formally verify JavaScript applications, particularly against security properties.

Here is my CV and my old homepage.


  • 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