Global Sparse Analysis Framework. - Hakjoo Oh; Kihong Heo; Wonchan Lee; Woosuk Lee; Daejun Park 001; Jeehoon Kang; Kwangkeun Yi (ACM Trans. Program. Lang. Syst., 2014)

KJS: a complete formal semantics of JavaScript. - Daejun Park 001; Andrei Stefanescu; Grigore Rosu (PLDI, 2015)

Semantics-based program verifiers for all languages. - Andrei Stefanescu; Daejun Park 001; Shijiao Yuwen; Yilong Li; Grigore Rosu (OOPSLA, 2016)

KEVM: A Complete Formal Semantics of the Ethereum Virtual Machine. - Everett Hildenbrandt; Manasvi Saxena; Nishant Rodrigues; Xiaoran Zhu; Philip Daian; Dwight Guth; Brandon M. Moore; Daejun Park 001; Yi Zhang; Andrei Stefanescu; Grigore Rosu (CSF, 2018)

A Language-Independent Approach to Smart Contract Verification. - Xiaohong Chen 002; Daejun Park 001; Grigore Rosu (ISoLA (4), 2018)

A formal verification tool for Ethereum VM bytecode. - Daejun Park 001; Yi Zhang; Manasvi Saxena; Philip Daian; Grigore Rosu (ESEC/SIGSOFT FSE, 2018)

Invariant Synthesis for Incomplete Verification Engines. - Daniel Neider; Pranav Garg 001; P. Madhusudan; Shambwaditya Saha; Daejun Park 001 (TACAS (1), 2018)

Efficient Logistic Regression on Large Encrypted Data. - Kyoohyung Han; Seungwan Hong 001; Jung Hee Cheon; Daejun Park 001 (IACR Cryptol. ePrint Arch., 2018)

Logistic Regression on Homomorphic Encrypted Data at Scale. - Kyoohyung Han; Seungwan Hong 001; Jung Hee Cheon; Daejun Park 001 (AAAI, 2019)

A complete formal semantics of x86-64 user-level instruction set architecture. - Sandeep Dasgupta; Daejun Park 001; Theodoros Kasampalis; Vikram S. Adve; Grigore Rosu (PLDI, 2019)

Verifiable Computing for Approximate Computation. - Shuo Chen; Jung Hee Cheon; Dongwoo Kim 003; Daejun Park 001 (IACR Cryptol. ePrint Arch., 2019)

Semantics-based program verification - Daejun Park 001 (2019)

End-to-End Formal Verification of Ethereum 2.0 Deposit Smart Contract. - Daejun Park 001; Yi Zhang; Grigore Rosu (CAV (1), 2020)

A Learning-Based Approach to Synthesizing Invariants for Incomplete Verification Engines. - Daniel Neider; P. Madhusudan; Shambwaditya Saha; Pranav Garg 001; Daejun Park 001 (J. Autom. Reason., 2020)

Language-parametric compiler validation with application to LLVM. - Theodoros Kasampalis; Daejun Park 001; Zhengyao Lin; Vikram S. Adve; Grigore Rosu (ASPLOS, 2021)

Interactive Proofs for Rounding Arithmetic. - Shuo Chen; Jung Hee Cheon; Dongwoo Kim 003; Daejun Park 001 (IEEE Access, 2022)