| 2025 | CCS | Generalized Security-Preserving Refinement for Concurrent Systems. | Huan Sun, David Sann, Jingyi Wang, Yongwang Zhao, Jun Sun, Wenhai Wang |
| 2025 | ICFEM | Modeling and Verifying Concurrent Reactive Systems Using Separation Logic. | Huan Sun, David Sann, Jun Sun, Wenhai Wang |
| 2024 | SETTA | Formalizing x86-64 ISA in Isabelle/HOL: A Binary Semantics for eBPF JIT Correctness. | Jiayi Lu, Shenghao Yuan, David Sann, Yongwang Zhao |
| 2024 | TACAS | A Parallel and Distributed Quantum SAT Solver Based on Entanglement and Teleportation. | Shang-Wei Lin, Tzu-Fan Wang, Yean-Ru Chen, Zhe Hou, David Sann, Yon Shin Teo |
| 2022 | ICFEM | A Formal Methodology for Verifying Side-Channel Vulnerabilities in Cache Architectures. | Ke Jiang, Tianwei Zhang, David Sann, Yongwang Zhao, Yang Liu |
| 2020 | ICECCS | Automatic Verification of Multi-threaded Programs by Inference of Rely-Guarantee Specifications. | Xuan-Bach Le, David Sann, Jun Sun, Shang-Wei Lin |
| 2020 | SP | Semantic Understanding of Smart Contracts: Executable Operational Semantics of Solidity. | Jiao Jiao, Shuanglong Kan, Shang-Wei Lin, David Sann, Yang Liu, Jun Sun |
| 2019 | CAV | Rely-Guarantee Reasoning About Concurrent Memory Management in Zephyr RTOS. | Yongwang Zhao, David Sann |
| 2019 | FM | A Parametric Rely-Guarantee Reasoning Framework for Concurrent Reactive Systems. | Yongwang Zhao, David Sann, Fuyuan Zhang, Yang Liu |
| 2019 | ICECCS | A Formally Verified Buddy Memory Allocation Model. | Ke Jiang, David Sann, Yongwang Zhao, Shuanglong Kan, Yang Liu |
| 2019 | SETTA | A Verified Specification of TLSF Memory Management Allocator Using State Monads. | Yu Zhang, Yongwang Zhao, David Sann, Lei Qiao, Jinkun Zhang |
| 2018 | FM | Compositional Reasoning for Shared-Variable Concurrent Programs. | Fuyuan Zhang, Yongwang Zhao, David Sann, Yang Liu, Alwen Tiu, Shang-Wei Lin, Jun Sun |
| 2017 | ITP | Proof Tactics for Assertions in Separation Logic. | Zhe Hou, David Sann, Alwen Tiu, Yang Liu |
| 2017 | TACAS | CSimpl: A Rely-Guarantee-Based Framework for Verifying Concurrent Programs. | David Sann, Yongwang Zhao, Zhe Hou, Fuyuan Zhang, Alwen Tiu, Yang Liu |
| 2016 | FM | An Executable Formalisation of the SPARCv8 Instruction Set Architecture: A Case Study for the LEON3 Processor. | Zhe Hou, David Sann, Alwen Tiu, Yang Liu, Koh Chuen Hoa |
| 2016 | TACAS | Reasoning About Information Flow Security of Separation Kernels with Channel-Based Communication. | Yongwang Zhao, David Sann, Fuyuan Zhang, Yang Liu |
| 2015 | ICECCS | Verifying FreeRTOS' Cyclic Doubly Linked List Implementation: From Abstract Specification to Machine Code. | David Sann, Yang Liu, Yongwang Zhao, Zhenchang Xing, Mike Hinchey |
| 2015 | ISSRE | Event-based formalization of safety-critical operating system standards: An experience report on ARINC 653 using Event-B. | Yongwang Zhao, Zhibin Yang, David Sann, Yang Liu |
| 2013 | VMCAI | State Space Reduction for Sensor Networks Using Two-Level Partial Order Reduction. | Manchun Zheng, David Sann, Jun Sun, Yang Liu, Jin Song Dong, Yu Gu |
| 2011 | SENSYS | Towards bug-free implementation for wireless sensor networks. | Manchun Zheng, Jun Sun, David Sann, Yang Liu, Jin Song Dong, Yu Gu |
| 2010 | SEFM | Verification of Dynamic Data Tree with mu-calculus Extended with Separation. | Mara-del-Mar Gallardo, David Sann |
| 2008 | COMPSAC | Model Checking C Programs with Dynamic Memory Allocation. | Mara-del-Mar Gallardo, Pedro Merino, David Sann |
| 2007 | ICECCS | On-the-fly model checking for C programs with extended CADP in FMICS-jETI. | Mara-del-Mar Gallardo, Pedro Merino, Christophe Joubert, David Sann |
| 2005 | FMICS | Model checking software with well-defined APIs: the socket case. | Pedro de la Cmara, Mara-del-Mar Gallardo, Pedro Merino, David Sann |