Model checking software with well-defined APIs: the socket case. - Pedro de la Cámara; María-del-Mar Gallardo; Pedro Merino 001; David Sanán (FMICS, 2005)

Towards Model Checking C Code with OPEN/CÆSAR. - María-del-Mar Gallardo; Pedro Merino 001; David Sanán (MSVVEIS, 2006)

On-the-fly model checking for C programs with extended CADP in FMICS-jETI. - María-del-Mar Gallardo; Pedro Merino 001; Christophe Joubert; David Sanán (ICECCS, 2007)

C.OPEN and ANNOTATOR: Tools for On-the-Fly Model Checking C Programs. - María-del-Mar Gallardo; Christophe Joubert; Pedro Merino 001; David Sanán (SPIN, 2007)

Extending CADP for Analyzing C Code. - María-del-Mar Gallardo; Pedro Merino 001; David Sanán (MSVVEIS, 2007)

Model Checking C Programs with Dynamic Memory Allocation. - María-del-Mar Gallardo; Pedro Merino 001; David Sanán (COMPSAC, 2008)

Web Services for Accessing Explicit State Space Verification Tools. - María-del-Mar Gallardo; Christophe Joubert; Pedro Merino 001; David Sanán (ERCIM News, 2008)

Model Checking Dynamic Memory Allocation in Operating Systems. - María-del-Mar Gallardo; Pedro Merino 001; David Sanán (J. Autom. Reason., 2009)

Checking the reliability of socket based communication software. - Pedro de la Cámara; María-del-Mar Gallardo; Pedro Merino 001; David Sanán (Int. J. Softw. Tools Technol. Transf., 2009)

Verification of Dynamic Data Tree with mu-calculus Extended with Separation. - María-del-Mar Gallardo; David Sanán (SEFM, 2010)

Towards bug-free implementation for wireless sensor networks. - Manchun Zheng; Jun Sun 001; David Sanán; Yang Liu 003; Jin Song Dong; Yu Gu 001 (SenSys, 2011)

A model-extraction approach to verifying concurrent C programs with CADP. - María-del-Mar Gallardo; Christophe Joubert; Pedro Merino 001; David Sanán (Sci. Comput. Program., 2012)

State Space Reduction for Sensor Networks Using Two-Level Partial Order Reduction. - Manchun Zheng; David Sanán; Jun Sun 001; Yang Liu 003; Jin Song Dong; Yu Gu 001 (VMCAI, 2013)

Verification of complex dynamic data tree with mu-calculus. - María-del-Mar Gallardo; David Sanán (Autom. Softw. Eng., 2013)

Separation Kernel Verification: The Xtratum Case Study. - David Sanán; Andrew Butterfield; Mike Hinchey (VSTTE, 2014)

Verifying FreeRTOS' Cyclic Doubly Linked List Implementation: From Abstract Specification to Machine Code. - David Sanán; Yang Liu 003; Yongwang Zhao; Zhenchang Xing; Mike Hinchey (ICECCS, 2015)

Event-based formalization of safety-critical operating system standards: An experience report on ARINC 653 using Event-B. - Yongwang Zhao; Zhibin Yang; David Sanán; Yang Liu 003 (ISSRE, 2015)

Event-based Formalization of Safety-critical Operating System Standards: An Experience Report on ARINC 653 using Event-B. - Yongwang Zhao; Zhibin Yang; David Sanán (CoRR, 2015)

An Executable Formalisation of the SPARCv8 Instruction Set Architecture: A Case Study for the LEON3 Processor. - Zhe Hou; David Sanán; Alwen Tiu; Yang Liu 003; Koh Chuen Hoa (FM, 2016)

Reasoning About Information Flow Security of Separation Kernels with Channel-Based Communication. - Yongwang Zhao; David Sanán; Fuyuan Zhang; Yang Liu 003 (TACAS, 2016)

Separata: Isabelle tactics for Separation Algebra. - Zhe Hou; David Sanán; Alwen Tiu; Rajeev Goré; Ranald Clouston (Arch. Formal Proofs, 2016)

A formal model for the SPARCv8 ISA and a proof of non-interference for the LEON3 processor. - Zhe Hou; David Sanán; Alwen Tiu; Yang Liu 003 (Arch. Formal Proofs, 2016)

Compositional Reasoning for Shared-variable Concurrent Programs. - Fuyuan Zhang; Yongwang Zhao; David Sanán; Yang Liu 003; Alwen Tiu; Shang-Wei Lin 001; Zhimin Wu; Jun Sun 001 (CoRR, 2016)

Formal Specification and Analysis of Partitioning Operating Systems by Integrating Ontology and Refinement. - Yongwang Zhao; David Sanán; Fuyuan Zhang; Yang Liu 003 (IEEE Trans. Ind. Informatics, 2016)

Proof Tactics for Assertions in Separation Logic. - Zhe Hou; David Sanán; Alwen Tiu; Yang Liu 003 (ITP, 2017)

FiB: squeezing loop invariants by interpolation between Forward/Backward predicate transformers. - Shang-Wei Lin 001; Jun Sun 001; Hao Xiao; Yang Liu 003; David Sanán; Henri Hansen (ASE, 2017)

VeriFormal: An Executable Formal Model of a Hardware Description Language. - Wilayat Khan; Alwen Tiu; David Sanán (SG-CRC, 2017)

CSimpl: A Rely-Guarantee-Based Framework for Verifying Concurrent Programs. - David Sanán; Yongwang Zhao; Zhe Hou; Fuyuan Zhang; Alwen Tiu; Yang Liu 003 (TACAS (1), 2017)

High-Assurance Separation Kernels: A Survey on Formal Methods. - Yongwang Zhao; David Sanán; Fuyuan Zhang; Yang Liu 003 (CoRR, 2017)

Compositional Reasoning for Shared-Variable Concurrent Programs. - Fuyuan Zhang; Yongwang Zhao; David Sanán; Yang Liu 003; Alwen Tiu; Shang-Wei Lin 001; Jun Sun 001 (FM, 2018)

Executable Operational Semantics of Solidity. - Jiao Jiao 002; Shuanglong Kan; Shang-Wei Lin 001; David Sanán; Yang Liu 003; Jun Sun 001 (CoRR, 2018)

K-Rust: An Executable Formal Semantics for Rust. - Shuanglong Kan; David Sanán; Shang-Wei Lin 001; Yang Liu 003 (CoRR, 2018)

An Event-based Compositional Reasoning Approach for Concurrent Reactive Systems. - Yongwang Zhao; David Sanán; Fuyuan Zhang; Yang Liu 003 (CoRR, 2018)

A Verified Timsort C Implementation in Isabelle/HOL. - Yu Zhang; Yongwang Zhao; David Sanán (CoRR, 2018)

Rely-Guarantee Reasoning About Concurrent Memory Management in Zephyr RTOS. - Yongwang Zhao; David Sanán (CAV (2), 2019)

A Parametric Rely-Guarantee Reasoning Framework for Concurrent Reactive Systems. - Yongwang Zhao; David Sanán; Fuyuan Zhang; Yang Liu 003 (FM, 2019)

A Formally Verified Buddy Memory Allocation Model. - Ke Jiang; David Sanán; Yongwang Zhao; Shuanglong Kan; Yang Liu 003 (ICECCS, 2019)

A Verified Specification of TLSF Memory Management Allocator Using State Monads. - Yu Zhang; Yongwang Zhao; David Sanán; Lei Qiao; Jinkun Zhang (SETTA, 2019)

A formalisation of the SPARC TSO memory model for multi-core machine code. - Zhe Hou; David Sanán; Alwen Tiu; Yang Liu 003; Jin Song Dong (CoRR, 2019)

On embedding a hardware description language in Isabelle/HOL. - Wilayat Khan; David Sanán; Zhe Hou; Yang Liu 003 (Des. Autom. Embed. Syst., 2019)

Refinement-Based Specification and Security Analysis of Separation Kernels. - Yongwang Zhao; David Sanán; Fuyuan Zhang; Yang Liu 003 (IEEE Trans. Dependable Secur. Comput., 2019)

Automatic Verification of Multi-threaded Programs by Inference of Rely-Guarantee Specifications. - Xuan-Bach Le; David Sanán; Jun Sun 001; Shang-Wei Lin 001 (ICECCS, 2020)

Semantic Understanding of Smart Contracts: Executable Operational Semantics of Solidity. - Jiao Jiao 002; Shuanglong Kan; Shang-Wei Lin 001; David Sanán; Yang Liu 003; Jun Sun 001 (SP, 2020)

CANeleon: Protecting CAN Bus With Frame ID Chameleon. - Kun Cheng; Yuebin Bai; Yuan Zhou 005; Yun Tang 003; David Sanán; Yang Liu 003 (IEEE Trans. Veh. Technol., 2020)

An Isabelle/HOL Formalisation of the SPARC Instruction Set Architecture and the TSO Memory Model. - Zhé Hóu; David Sanán; Alwen Tiu; Yang Liu 003; Koh Chuen Hoa; Jin Song Dong (J. Autom. Reason., 2021)

CSim2: Compositional Top-down Verification of Concurrent Systems using Rely-Guarantee. - David Sanán; Yongwang Zhao; Shang-Wei Lin 001; Yang Liu 003 (ACM Trans. Program. Lang. Syst., 2021)

A Formal Methodology for Verifying Side-Channel Vulnerabilities in Cache Architectures. - Ke Jiang; Tianwei Zhang 004; David Sanán; Yongwang Zhao; Yang Liu 003 (ICFEM, 2022)

An Executable Formal Model of the VHDL in Isabelle/HOL. - Wilayat Khan; Zhe Hou; David Sanán; Jamel Nebhen; Yang Liu 003; Alwen Tiu (CoRR, 2022)

A Quantum interpretation of separating conjunction for local reasoning of Quantum programs based on separation logic. - Xuan-Bach Le; Shang-Wei Lin 001; Jun Sun 001; David Sanán (Proc. ACM Program. Lang., 2022)

A Parallel and Distributed Quantum SAT Solver Based on Entanglement and Quantum Teleportation. - Shang-Wei Lin 001; Tzu-Fan Wang; Yean-Ru Chen; Zhe Hou; David Sanán; Yon Shin Teo (CoRR, 2023)

Event-based Compositional Reasoning of Information-Flow Security for Concurrent Systems. - Yongwang Zhao; David Sanán; Fuyuan Zhang; Yang Liu 003 (CoRR, 2023)

Rely-guarantee Reasoning about Concurrent Reactive Systems: The PiCore Framework, Languages Integration and Applications. - Yongwang Zhao; David Sanán (CoRR, 2023)

Rely-guarantee Reasoning about Concurrent Memory Management: Correctness, Safety and Security. - Yongwang Zhao; David Sanán (CoRR, 2023)

Formalizing x86-64 ISA in Isabelle/HOL: A Binary Semantics for eBPF JIT Correctness. - Jiayi Lu; Shenghao Yuan; David Sanán; Yongwang Zhao (SETTA, 2024)

A Parallel and Distributed Quantum SAT Solver Based on Entanglement and Teleportation. - Shang-Wei Lin 001; Tzu-Fan Wang; Yean-Ru Chen; Zhe Hou; David Sanán; Yon Shin Teo (TACAS (2), 2024)

Towards Large Language Model Aided Program Refinement. - Yufan Cai; Zhe Hou; Xiaokun Luan; David Sanán; Yun Lin 001; Jun Sun 001; Jin Song Dong 001 (CoRR, 2024)

Formally understanding Rust's ownership and borrowing system at the memory level. - Shuanglong Kan; Zhe Chen 011; David Sanán; Yang Liu 003 (Formal Methods Syst. Des., 2024)

Automated Program Refinement: Guide and Verify Code Large Language Model with Refinement Calculus. - Yufan Cai; Zhe Hou; David Sanán; Xiaokun Luan; Yun Lin 001; Jun Sun 001; Jin Song Dong 001 (Proc. ACM Program. Lang., 2025)

Generically Automating Separation Logic by Functors, Homomorphisms, and Modules. - Qiyuan Xu; David Sanán; Zhe Hou; Xiaokun Luan; Conrad Watt; Yang Liu 003 (Proc. ACM Program. Lang., 2025)

A Complete Formal Semantics of eBPF Instruction Set Architecture for Solana. - Shenghao Yuan; Zhuoruo Zhang; Jiayi Lu; David Sanán; Rui Chang; Yongwang Zhao (Proc. ACM Program. Lang., 2025)

Why the Proof Fails in Different Versions of Theorem Provers: An Empirical Study of Compatibility Issues in Isabelle. - Xiaokun Luan; David Sanán; Zhe Hou; Qiyuan Xu; Chengwei Liu; Yufan Cai; Yang Liu 003; Meng Sun 002 (Proc. ACM Softw. Eng., 2025)

IsaMini: Redesigned Isabelle Proof Lanugage for Machine Learning. - Qiyuan Xu; Renxi Wang; Haonan Li; David Sanán; Conrad Watt (CoRR, 2025)