Follow
Daejun Park
Daejun Park
Unknown affiliation
No verified email - Homepage
Title
Cited by
Cited by
Year
Kevm: A complete formal semantics of the ethereum virtual machine
E Hildenbrandt, M Saxena, N Rodrigues, X Zhu, P Daian, D Guth, ...
2018 IEEE 31st Computer Security Foundations Symposium (CSF), 204-217, 2018
4282018
KJS: A complete formal semantics of JavaScript
D Park, A Stefănescu, G Roşu
PLDI'15, 346-356, 2015
1732015
Logistic regression on homomorphic encrypted data at scale
K Han, S Hong, JH Cheon, D Park
Proceedings of the AAAI Conference on Artificial Intelligence 33, 9466-9471, 2019
142*2019
Semantics-based program verifiers for all languages
A Stefănescu, D Park, S Yuwen, Y Li, G Roşu
OOPSLA'16, 74-91, 2016
1302016
A formal verification tool for Ethereum VM bytecode
D Park, Y Zhang, M Saxena, P Daian, G Roşu
Proceedings of the 2018 26th ACM joint meeting on european software …, 2018
1172018
A complete formal semantics of x86-64 user-level instruction set architecture
S Dasgupta, D Park, T Kasampalis, VS Adve, G Roşu
Proceedings of the 40th ACM SIGPLAN Conference on Programming Language …, 2019
862019
End-to-end formal verification of ethereum 2.0 deposit smart contract
D Park, Y Zhang, G Rosu
Computer Aided Verification: 32nd International Conference, CAV 2020, Los …, 2020
312020
Global sparse analysis framework
H Oh, K Heo, W Lee, W Lee, D Park, J Kang, K Yi
ACM Transactions on Programming Languages and Systems (TOPLAS) 36 (3), 1-44, 2014
292014
A language-independent approach to smart contract verification
X Chen, D Park, G Roşu
Leveraging Applications of Formal Methods, Verification and Validation …, 2018
202018
Verifiable computing for approximate computation
S Chen, JH Cheon, D Kim, D Park
Cryptology ePrint Archive, 2019
162019
Language-parametric compiler validation with application to LLVM
T Kasampalis, D Park, Z Lin, VS Adve, G Roşu
Proceedings of the 26th ACM International Conference on Architectural …, 2021
152021
Invariant synthesis for incomplete verification engines
D Neider, P Garg, P Madhusudan, S Saha, D Park
Tools and Algorithms for the Construction and Analysis of Systems: 24th …, 2018
132018
A learning-based approach to synthesizing invariants for incomplete verification engines
D Neider, P Madhusudan, S Saha, P Garg, D Park
Journal of Automated Reasoning 64, 1523-1552, 2020
72020
Unstaging Translation of Cross-Stage Persistent Multi-Staged Programs
J Choi, J Kang, D Park, K Yi
3*2012
Calculation verification for approximate calculation
JH Cheon, D Kim, D Park
US Patent App. 17/422,278, 2022
22022
Encrypted Execution
D Park, J Kang, K Heo, S Cho, Y Yoon, K Yi
22012
Interactive Proofs for Rounding Arithmetic
S Chen, JH Cheon, D Kim, D Park
IEEE Access 10, 122706-122725, 2022
12022
Cut-Bisimulation and Program Equivalence
D Park, G Rosu, VS Adve, T Kasampalis
Unpublished manuscript, University of Illinois at Urbana-Champaign, 2020
12020
Semantics-based program verification
D Park
University of Illinois at Urbana-Champaign, 2019
12019
Parameterized Procedural Summaries: How to Achieve Scalable and Context-sensitive Buffer-overrun Static Detection for C Programs
D Park
Seoul National University, 2008
2008
The system can't perform the operation now. Try again later.
Articles 1–20