| Semantic understanding of smart contracts: Executable operational semantics of solidity J Jiao, S Kan, SW Lin, D Sanan, Y Liu, J Sun 2020 IEEE Symposium on Security and Privacy (SP), 1695-1712, 2020 | 128 | 2020 |
| Csimpl: A rely-guarantee-based framework for verifying concurrent programs D Sanán, Y Zhao, Z Hou, F Zhang, A Tiu, Y Liu International Conference on Tools and Algorithms for the Construction and …, 2017 | 40 | 2017 |
| Automated program refinement: Guide and verify code large language model with refinement calculus Y Cai, Z Hou, D Sanán, X Luan, Y Lin, J Sun, JS Dong Proceedings of the ACM on Programming Languages 9 (POPL), 2057-2089, 2025 | 38 | 2025 |
| CANeleon: Protecting CAN Bus With Frame ID Chameleon K Cheng, Y Bai, Y Zhou, Y Tang, D Sanan, Y Liu IEEE Transactions on Vehicular technology 69 (7), 7116-7130, 2020 | 36 | 2020 |
| An executable formalisation of the SPARCv8 instruction set architecture: a case study for the LEON3 processor Z Hou, D Sanán, A Tiu, Y Liu, KC Hoa International Symposium on Formal Methods, 388-405, 2016 | 36 | 2016 |
| Fib: Squeezing loop invariants by interpolation between forward/backward predicate transformers SW Lin, J Sun, H Xiao, Y Liu, D Sanán, H Hansen 2017 32nd IEEE/ACM International Conference on Automated Software …, 2017 | 32 | 2017 |
| Model checking dynamic memory allocation in operating systems MM Gallardo, P Merino, D Sanán Journal of Automated Reasoning 42 (2), 229-264, 2009 | 31 | 2009 |
| Model checking software with well-defined apis: the socket case P de la Cámara, MM Gallardo, P Merino, D Sanan Proceedings of the 10th international workshop on Formal methods for …, 2005 | 30 | 2005 |
| An isabelle/hol formalisation of the SPARC instruction set architecture and the TSO memory model Z Hóu, D Sanán, A Tiu, Y Liu, KC Hoa, JS Dong Journal of Automated Reasoning 65 (4), 569-598, 2021 | 29 | 2021 |
| Refinement-based specification and security analysis of separation kernels Y Zhao, D Sanán, F Zhang, Y Liu IEEE Transactions on Dependable and Secure Computing 16 (1), 127-141, 2017 | 28 | 2017 |
| Reasoning about information flow security of separation kernels with channel-based communication Y Zhao, D Sanán, F Zhang, Y Liu International Conference on Tools and Algorithms for the Construction and …, 2016 | 28 | 2016 |
| On embedding a hardware description language in Isabelle/HOL W Khan, D Sanán, Z Hou, L Yang Design Automation for Embedded Systems 23 (3), 123-151, 2019 | 27 | 2019 |
| Proof tactics for assertions in separation logic Z Hóu, D Sanán, A Tiu, Y Liu International Conference on Interactive Theorem Proving, 285-303, 2017 | 24 | 2017 |
| A quantum interpretation of separating conjunction for local reasoning of quantum programs based on separation logic XB Le, SW Lin, J Sun, D Sanan Proceedings of the ACM on Programming Languages 6 (POPL), 1-27, 2022 | 23 | 2022 |
| A parallel and distributed quantum SAT solver based on entanglement and quantum teleportation SW Lin, TF Wang, YR Chen, Z Hou, D Sanán, YS Teo arXiv preprint arXiv:2308.03344, 2023 | 22 | 2023 |
| Formal specification and analysis of partitioning operating systems by integrating ontology and refinement Y Zhao, D Sanán, F Zhang, Y Liu IEEE Transactions on Industrial Informatics 12 (4), 1321-1331, 2016 | 22 | 2016 |
| A parallel and distributed quantum SAT solver based on entanglement and teleportation SW Lin, TF Wang, YR Chen, Z Hou, D Sanán, YS Teo International Conference on Tools and Algorithms for the Construction and …, 2024 | 21 | 2024 |
| Rely-guarantee reasoning about concurrent memory management in Zephyr RTOS Y Zhao, D Sanán International Conference on Computer Aided Verification, 515-533, 2019 | 21 | 2019 |
| Separation kernel verification: The xtratum case study D Sanán, A Butterfield, M Hinchey Working Conference on Verified Software: Theories, Tools, and Experiments …, 2014 | 20 | 2014 |
| An executable formal model of the VHDL in isabelle/hol W Khan, Z Hou, D Sanán, J Nebhen, Y Liu, A Tiu arXiv preprint arXiv:2202.04192, 2022 | 19 | 2022 |