[go: up one dir, main page]

Follow
David Sanán
David Sanán
Singapore Institute of Technologie
Verified email at singaporetech.edu.sg
Title
Cited by
Cited by
Year
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
1282020
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
402017
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
382025
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
362020
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
362016
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
322017
Model checking dynamic memory allocation in operating systems
MM Gallardo, P Merino, D Sanán
Journal of Automated Reasoning 42 (2), 229-264, 2009
312009
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
302005
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
292021
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
282017
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
282016
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
272019
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
242017
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
232022
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
222023
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
222016
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
212024
Rely-guarantee reasoning about concurrent memory management in Zephyr RTOS
Y Zhao, D Sanán
International Conference on Computer Aided Verification, 515-533, 2019
212019
Separation kernel verification: The xtratum case study
D Sanán, A Butterfield, M Hinchey
Working Conference on Verified Software: Theories, Tools, and Experiments …, 2014
202014
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
192022
The system can't perform the operation now. Try again later.
Articles 1–20