Daejun Park
daejunpark (at) gmail (dot) com
Software
Writings
-
Formal verification of Pectra system contracts with Halmos
[post]
(2025)
-
Symbolic testing with Halmos: Leveraging existing tests for formal verification
[post]
(2023)
-
Generalized property tests for ERC4626 vaults
[post]
(2022)
-
Formal Verification of ERC20 Contracts
[post]
(2018)
-
How Formal Verification of Smart Contracts Works
[post]
(2018)
Work
-
Formal Verification of Beacon Chain Specification
[artifact]
(2020)
-
Formal Verification of Beacon Chain Deposit Contract
[artifact]
(2020)
-
Formal Verification of Gnosis Safe V1
[report]
(2019)
-
Formal Verification of Uniswap V1
[artifact]
(2018)
-
Formal Verification of Ethereum Casper FFG
[artifact]
(2018)
Papers (2015-2021)
-
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]
