Daejun Park

17 papers A* 4A 2Journal 6Unranked 4
YearRankTypeTitle / Venue / Authors
2022 J jnl
Interactive Proofs for Rounding Arithmetic.
IEEE Access
Shuo Chen, Jung Hee Cheon, Dongwoo Kim, Daejun Park
2021 A* conf
Language-parametric compiler validation with application to LLVM.
ASPLOS
Theodoros Kasampalis, Daejun Park, Zhengyao Lin, Vikram S. Adve, Grigore Rosu
2020 J jnl
A Learning-Based Approach to Synthesizing Invariants for Incomplete Verification Engines.
J. Autom. Reason.
Daniel Neider, P. Madhusudan, Shambwaditya Saha, Pranav Garg, Daejun Park
2020 — conf
End-to-End Formal Verification of Ethereum 2.0 Deposit Smart Contract.
CAV (1)
Daejun Park, Yi Zhang, Grigore Rosu
2019 A* conf
A complete formal semantics of x86-64 user-level instruction set architecture.
PLDI
Sandeep Dasgupta, Daejun Park, Theodoros Kasampalis, Vikram S. Adve, Grigore Rosu
2019 A* conf
Logistic Regression on Homomorphic Encrypted Data at Scale.
AAAI
Kyoohyung Han, Seungwan Hong, Jung Hee Cheon, Daejun Park
2019 — —
Semantics-based program verification
Daejun Park
2019 J jnl
Verifiable Computing for Approximate Computation.
IACR Cryptol. ePrint Arch.
Shuo Chen, Jung Hee Cheon, Dongwoo Kim, Daejun Park
2018 — conf
A Language-Independent Approach to Smart Contract Verification.
ISoLA (4)
Xiaohong Chen, Daejun Park, Grigore Rosu
2018 — conf
A formal verification tool for Ethereum VM bytecode.
ESEC/SIGSOFT FSE
Daejun Park, Yi Zhang, Manasvi Saxena, Philip Daian, Grigore Rosu
2018 J jnl
Efficient Logistic Regression on Large Encrypted Data.
IACR Cryptol. ePrint Arch.
Kyoohyung Han, Seungwan Hong, Jung Hee Cheon, Daejun Park
2018 — conf
Invariant Synthesis for Incomplete Verification Engines.
TACAS (1)
Daniel Neider, Pranav Garg, P. Madhusudan, Shambwaditya Saha, Daejun Park
2018 A conf
KEVM: A Complete Formal Semantics of the Ethereum Virtual Machine.
CSF
Everett Hildenbrandt, Manasvi Saxena, Nishant Rodrigues, Xiaoran Zhu, Philip Daian, Dwight Guth, Brandon M. Moore, Daejun Park, Yi Zhang, Andrei Stefanescu, Grigore Rosu
2017 J jnl
Invariant Synthesis for Incomplete Verification Engines.
CoRR
Daniel Neider, Pranav Garg, P. Madhusudan, Shambwaditya Saha, Daejun Park
2016 A conf
Semantics-based program verifiers for all languages.
OOPSLA
Andrei Stefanescu, Daejun Park, Shijiao Yuwen, Yilong Li, Grigore Rosu
2015 A* conf
KJS: a complete formal semantics of JavaScript.
PLDI
Daejun Park, Andrei Stefanescu, Grigore Rosu
2014 J jnl
Global Sparse Analysis Framework.
ACM Trans. Program. Lang. Syst.
Hakjoo Oh, Kihong Heo, Wonchan Lee, Woosuk Lee, Daejun Park, Jeehoon Kang, Kwangkeun Yi