Difference between revisions of "Daejun Park"

From FSL
Jump to: navigation, search
Line 1: Line 1:
I am a PhD student working with Prof. [[Grigore Rosu]]. Recently, I defined a [https://github.com/kframework/javascript-semantics 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.
+
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.
 +
<!--
 +
Recently, I defined a [https://github.com/kframework/javascript-semantics 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 [http://web.engr.illinois.edu/~dpark69/cv.pdf CV] and my [http://web.engr.illinois.edu/~dpark69/ homepage].
+
Here is my [http://web.engr.illinois.edu/~dpark69/cv.pdf CV].
  
 
== Contact ==
 
== Contact ==

Revision as of 03:26, 1 May 2015

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.

Contact

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

Publications

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
PDF, KEVM, CSF 2018, BIB
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
Namespaces

Variants
Actions
Navigation