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 | 480 | 2018 |
KJS: A complete formal semantics of JavaScript D Park, A Stefănescu, G Roşu PLDI'15, 346-356, 2015 | 182 | 2015 |
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 | 165* | 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 | 133 | 2016 |
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 | 124 | 2018 |
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 | 92 | 2019 |
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 | 40 | 2020 |
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 | 29 | 2014 |
A language-independent approach to smart contract verification X Chen, D Park, G Roşu Leveraging Applications of Formal Methods, Verification and Validation …, 2018 | 22 | 2018 |
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 | 19 | 2021 |
Verifiable computing for approximate computation S Chen, JH Cheon, D Kim, D Park Cryptology ePrint Archive, 2019 | 18 | 2019 |
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 | 14 | 2018 |
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 | 8 | 2020 |
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 | 2 | 2022 |
Encrypted Execution D Park, J Kang, K Heo, S Cho, Y Yoon, K Yi | 2 | 2012 |
Interactive Proofs for Rounding Arithmetic S Chen, JH Cheon, D Kim, D Park IEEE Access 10, 122706-122725, 2022 | 1 | 2022 |
Cut-Bisimulation and Program Equivalence D Park, G Rosu, VS Adve, T Kasampalis Unpublished manuscript, University of Illinois at Urbana-Champaign, 2020 | 1 | 2020 |
Semantics-based program verification D Park University of Illinois at Urbana-Champaign, 2019 | 1 | 2019 |
Parameterized Procedural Summaries: How to Achieve Scalable and Context-sensitive Buffer-overrun Static Detection for C Programs D Park Seoul National University, 2008 | 1* | 2008 |