David Sanán

Publication Activity (10 Years)

Years Active: 2005-2024
Publications (10 Years): 42

Top Topics

Memory Management

Reactive Systems

Top Venues

Arch. Formal Proofs

Publications

Shang-Wei Lin, Tzu-Fan Wang, Yean-Ru Chen, Zhe Hou, David Sanán, Yon Shin Teo
A Parallel and Distributed Quantum SAT Solver Based on Entanglement and Teleportation. TACAS (2) (2024)
Yufan Cai, Zhe Hou, Xiaokun Luan, David Sanán, Yun Lin, Jun Sun, Jin Song Dong
Towards Large Language Model Aided Program Refinement. CoRR (2024)
Shang-Wei Lin, Tzu-Fan Wang, Yean-Ru Chen, Zhe Hou, David Sanán, Yon Shin Teo
A Parallel and Distributed Quantum SAT Solver Based on Entanglement and Quantum Teleportation. CoRR (2023)
Yongwang Zhao, David Sanán
Rely-guarantee Reasoning about Concurrent Memory Management: Correctness, Safety and Security. CoRR (2023)
Yongwang Zhao, David Sanán
Rely-guarantee Reasoning about Concurrent Reactive Systems: The PiCore Framework, Languages Integration and Applications. CoRR (2023)
Yongwang Zhao, David Sanán, Fuyuan Zhang, Yang Liu
Event-based Compositional Reasoning of Information-Flow Security for Concurrent Systems. CoRR (2023)
Wilayat Khan, Zhe Hou, David Sanán, Jamel Nebhen, Yang Liu, Alwen Tiu
An Executable Formal Model of the VHDL in Isabelle/HOL. CoRR (2022)
Xuan-Bach Le, Shang-Wei Lin, Jun Sun, David Sanán
A Quantum interpretation of separating conjunction for local reasoning of Quantum programs based on separation logic. Proc. ACM Program. Lang. 6 (POPL) (2022)
Ke Jiang, Tianwei Zhang, David Sanán, Yongwang Zhao, Yang Liu
A Formal Methodology for Verifying Side-Channel Vulnerabilities in Cache Architectures. ICFEM (2022)
Zhé Hóu, David Sanán, Alwen Tiu, Yang Liu, Koh Chuen Hoa, Jin Song Dong
An Isabelle/HOL Formalisation of the SPARC Instruction Set Architecture and the TSO Memory Model. J. Autom. Reason. 65 (4) (2021)
David Sanán, Yongwang Zhao, Shang-Wei Lin, Yang Liu
: Compositional Top-down Verification of Concurrent Systems using Rely-Guarantee. ACM Trans. Program. Lang. Syst. 43 (1) (2021)
Kun Cheng, Yuebin Bai, Yuan Zhou, Yun Tang, David Sanán, Yang Liu
CANeleon: Protecting CAN Bus With Frame ID Chameleon. IEEE Trans. Veh. Technol. 69 (7) (2020)
Jiao Jiao, Shuanglong Kan, Shang-Wei Lin, David Sanán, Yang Liu, Jun Sun
Semantic Understanding of Smart Contracts: Executable Operational Semantics of Solidity. IEEE Symposium on Security and Privacy (2020)
Xuan-Bach Le, David Sanán, Jun Sun, Shang-Wei Lin
Automatic Verification of Multi-threaded Programs by Inference of Rely-Guarantee Specifications. ICECCS (2020)
Yongwang Zhao, David Sanán, Fuyuan Zhang, Yang Liu
Refinement-Based Specification and Security Analysis of Separation Kernels. IEEE Trans. Dependable Secur. Comput. 16 (1) (2019)
Zhe Hou, David Sanán, Alwen Tiu, Yang Liu, Jin Song Dong
A formalisation of the SPARC TSO memory model for multi-core machine code. CoRR (2019)
Wilayat Khan, David Sanán, Zhe Hou, Yang Liu
On embedding a hardware description language in Isabelle/HOL. Des. Autom. Embed. Syst. 23 (3-4) (2019)
Yongwang Zhao, David Sanán, Fuyuan Zhang, Yang Liu
A Parametric Rely-Guarantee Reasoning Framework for Concurrent Reactive Systems. FM (2019)
Yu Zhang, Yongwang Zhao, David Sanán, Lei Qiao, Jinkun Zhang
A Verified Specification of TLSF Memory Management Allocator Using State Monads. SETTA (2019)
Ke Jiang, David Sanán, Yongwang Zhao, Shuanglong Kan, Yang Liu
A Formally Verified Buddy Memory Allocation Model. ICECCS (2019)
Yongwang Zhao, David Sanán
Rely-Guarantee Reasoning About Concurrent Memory Management in Zephyr RTOS. CAV (2) (2019)
Yu Zhang, Yongwang Zhao, David Sanán
A Verified Timsort C Implementation in Isabelle/HOL. CoRR (2018)
Fuyuan Zhang, Yongwang Zhao, David Sanán, Yang Liu, Alwen Tiu, Shang-Wei Lin, Jun Sun
Compositional Reasoning for Shared-Variable Concurrent Programs. FM (2018)
Yongwang Zhao, David Sanán, Fuyuan Zhang, Yang Liu
An Event-based Compositional Reasoning Approach for Concurrent Reactive Systems. CoRR (2018)
Jiao Jiao, Shuanglong Kan, Shang-Wei Lin, David Sanán, Yang Liu, Jun Sun
Executable Operational Semantics of Solidity. CoRR (2018)
Shuanglong Kan, David Sanán, Shang-Wei Lin, Yang Liu
K-Rust: An Executable Formal Semantics for Rust. CoRR (2018)
Zhe Hou, David Sanán, Alwen Tiu, Yang Liu
Proof Tactics for Assertions in Separation Logic. ITP (2017)
Shang-Wei Lin, Jun Sun, Hao Xiao, Yang Liu, David Sanán, Henri Hansen
FiB: squeezing loop invariants by interpolation between Forward/Backward predicate transformers. ASE (2017)
Yongwang Zhao, David Sanán, Fuyuan Zhang, Yang Liu
Refinement-based Specification and Security Analysis of Separation Kernels. CoRR (2017)
David Sanán, Yongwang Zhao, Zhe Hou, Fuyuan Zhang, Alwen Tiu, Yang Liu
CSimpl: A Rely-Guarantee-Based Framework for Verifying Concurrent Programs. TACAS (1) (2017)
Yongwang Zhao, David Sanán, Fuyuan Zhang, Yang Liu
High-Assurance Separation Kernels: A Survey on Formal Methods. CoRR (2017)
Wilayat Khan, Alwen Tiu, David Sanán
VeriFormal: An Executable Formal Model of a Hardware Description Language. SG-CRC (2017)
Zhe Hou, David Sanán, Alwen Tiu, Rajeev Goré, Ranald Clouston
Separata: Isabelle tactics for Separation Algebra. Arch. Formal Proofs 2016 (2016)
Fuyuan Zhang, Yongwang Zhao, David Sanán, Yang Liu, Alwen Tiu, Shang-Wei Lin, Zhimin Wu, Jun Sun
Compositional Reasoning for Shared-variable Concurrent Programs. CoRR (2016)
Zhe Hou, David Sanán, Alwen Tiu, Yang Liu
A formal model for the SPARCv8 ISA and a proof of non-interference for the LEON3 processor. Arch. Formal Proofs 2016 (2016)
Yongwang Zhao, David Sanán, Fuyuan Zhang, Yang Liu
Reasoning About Information Flow Security of Separation Kernels with Channel-Based Communication. TACAS (2016)
Yongwang Zhao, David Sanán, Fuyuan Zhang, Yang Liu
Formal Specification and Analysis of Partitioning Operating Systems by Integrating Ontology and Refinement. IEEE Trans. Ind. Informatics 12 (4) (2016)
Zhe Hou, David Sanán, Alwen Tiu, Yang Liu, Koh Chuen Hoa
An Executable Formalisation of the SPARCv8 Instruction Set Architecture: A Case Study for the LEON3 Processor. FM (2016)
Yongwang Zhao, David Sanán, Fuyuan Zhang, Yang Liu
Reasoning About Information Flow Security of Separation Kernels with Channel-based Communication. CoRR (2015)
David Sanán, Liu Yang, Yongwang Zhao, Zhenchang Xing, Mike Hinchey
Verifying FreeRTOS' Cyclic Doubly Linked List Implementation: From Abstract Specification to Machine Code. ICECCS (2015)
Yongwang Zhao, Zhibin Yang, David Sanán
Event-based Formalization of Safety-critical Operating System Standards: An Experience Report on ARINC 653 using Event-B. CoRR (2015)
Yongwang Zhao, Zhibin Yang, David Sanán, Yang Liu
Event-based formalization of safety-critical operating system standards: An experience report on ARINC 653 using Event-B. ISSRE (2015)
David Sanán, Andrew Butterfield, Mike Hinchey
Separation Kernel Verification: The Xtratum Case Study. VSTTE (2014)
Manchun Zheng, David Sanán, Jun Sun, Yang Liu, Jin Song Dong, Yu Gu
State Space Reduction for Sensor Networks Using Two-Level Partial Order Reduction. VMCAI (2013)
María-del-Mar Gallardo, David Sanán
Verification of complex dynamic data tree with mu-calculus. Autom. Softw. Eng. 20 (4) (2013)
María-del-Mar Gallardo, Christophe Joubert, Pedro Merino, David Sanán
A model-extraction approach to verifying concurrent C programs with CADP. Sci. Comput. Program. 77 (3) (2012)
Manchun Zheng, Jun Sun, David Sanán, Yang Liu, Jin Song Dong, Yu Gu
Towards bug-free implementation for wireless sensor networks. SenSys (2011)
María-del-Mar Gallardo, David Sanán
Verification of Dynamic Data Tree with mu-calculus Extended with Separation. SEFM (2010)
María-del-Mar Gallardo, Pedro Merino, David Sanán
Model Checking Dynamic Memory Allocation in Operating Systems. J. Autom. Reason. 42 (2-4) (2009)
Pedro de la Cámara, María-del-Mar Gallardo, Pedro Merino, David Sanán
Checking the reliability of socket based communication software. Int. J. Softw. Tools Technol. Transf. 11 (5) (2009)
María-del-Mar Gallardo, Christophe Joubert, Pedro Merino, David Sanán
Web Services for Accessing Explicit State Space Verification Tools. ERCIM News 2008 (73) (2008)
María-del-Mar Gallardo, Pedro Merino, David Sanán
Model Checking C Programs with Dynamic Memory Allocation. COMPSAC (2008)
María-del-Mar Gallardo, Christophe Joubert, Pedro Merino, David Sanán
C.OPEN and ANNOTATOR: Tools for On-the-Fly Model Checking C Programs. SPIN (2007)
María-del-Mar Gallardo, Pedro Merino, David Sanán
Extending CADP for Analyzing C Code. MSVVEIS (2007)
María-del-Mar Gallardo, Pedro Merino, Christophe Joubert, David Sanán
On-the-fly model checking for C programs with extended CADP in FMICS-jETI. ICECCS (2007)
María-del-Mar Gallardo, Pedro Merino, David Sanán
Towards Model Checking C Code with OPEN/CÆSAR. MSVVEIS (2006)
Pedro de la Cámara, María-del-Mar Gallardo, Pedro Merino, David Sanán
Model checking software with well-defined APIs: the socket case. FMICS (2005)