David Sanán

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