default search action
Google
Google Scholar
Semantic Scholar
Internet Archive Scholar
CiteSeerX
ORCIDDavid Sanán
Person information
Refine list
refinements active!
zoomed in on ?? of ?? records
view refined list in
export refined list as
2020 – today
- 2024
[c27]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: 363-382- [i17]Yufan Cai, Zhe Hou, Xiaokun Luan, David Sanán, Yun Lin, Jun Sun, Jin Song Dong:
Towards Large Language Model Aided Program Refinement. CoRR abs/2406.18616 (2024) - 2023
- [i16]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 abs/2308.03344 (2023) - [i15]Yongwang Zhao, David Sanán, Fuyuan Zhang, Yang Liu:
Event-based Compositional Reasoning of Information-Flow Security for Concurrent Systems. CoRR abs/2309.09141 (2023) - [i14]Yongwang Zhao, David Sanán:
Rely-guarantee Reasoning about Concurrent Reactive Systems: The PiCore Framework, Languages Integration and Applications. CoRR abs/2309.09148 (2023) - [i13]Yongwang Zhao, David Sanán:
Rely-guarantee Reasoning about Concurrent Memory Management: Correctness, Safety and Security. CoRR abs/2309.09997 (2023) - 2022
- [j13]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): 1-27 (2022) - [c26]Ke Jiang, Tianwei Zhang, David Sanán, Yongwang Zhao, Yang Liu:
A Formal Methodology for Verifying Side-Channel Vulnerabilities in Cache Architectures. ICFEM 2022: 190-208 - [i12]Wilayat Khan, Zhe Hou, David Sanán, Jamel Nebhen, Yang Liu, Alwen Tiu:
An Executable Formal Model of the VHDL in Isabelle/HOL. CoRR abs/2202.04192 (2022) - 2021
- [j12]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): 569-598 (2021) - [j11]David Sanán, Yongwang Zhao, Shang-Wei Lin, Yang Liu:
CSim2: Compositional Top-down Verification of Concurrent Systems using Rely-Guarantee. ACM Trans. Program. Lang. Syst. 43(1): 2:1-2:46 (2021) - 2020
- [j10]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): 7116-7130 (2020) - [c25]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: 43-52 - [c24]Jiao Jiao, Shuanglong Kan, Shang-Wei Lin, David Sanán, Yang Liu, Jun Sun:
Semantic Understanding of Smart Contracts: Executable Operational Semantics of Solidity. SP 2020: 1695-1712
2010 – 2019
- 2019
- [j9]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): 123-151 (2019) - [j8]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): 127-141 (2019) - [c23]Yongwang Zhao, David Sanán:
Rely-Guarantee Reasoning About Concurrent Memory Management in Zephyr RTOS. CAV (2) 2019: 515-533 - [c22]Yongwang Zhao, David Sanán, Fuyuan Zhang, Yang Liu:
A Parametric Rely-Guarantee Reasoning Framework for Concurrent Reactive Systems. FM 2019: 161-178 - [c21]Ke Jiang, David Sanán, Yongwang Zhao, Shuanglong Kan, Yang Liu:
A Formally Verified Buddy Memory Allocation Model. ICECCS 2019: 144-153 - [c20]Yu Zhang, Yongwang Zhao, David Sanán, Lei Qiao, Jinkun Zhang:
A Verified Specification of TLSF Memory Management Allocator Using State Monads. SETTA 2019: 122-138 - [i11]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 abs/1906.11203 (2019) - 2018
- [c19]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: 523-541 - [i10]Jiao Jiao, Shuanglong Kan, Shang-Wei Lin, David Sanán, Yang Liu, Jun Sun:
Executable Operational Semantics of Solidity. CoRR abs/1804.01295 (2018) - [i9]Shuanglong Kan, David Sanán, Shang-Wei Lin, Yang Liu:
K-Rust: An Executable Formal Semantics for Rust. CoRR abs/1804.07608 (2018) - [i8]Yongwang Zhao, David Sanán, Fuyuan Zhang, Yang Liu:
An Event-based Compositional Reasoning Approach for Concurrent Reactive Systems. CoRR abs/1810.07855 (2018) - [i7]Yu Zhang, Yongwang Zhao, David Sanán:
A Verified Timsort C Implementation in Isabelle/HOL. CoRR abs/1812.03318 (2018) - 2017
- [c18]Zhe Hou, David Sanán, Alwen Tiu, Yang Liu:
Proof Tactics for Assertions in Separation Logic. ITP 2017: 285-303 - [c17]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: 793-803 - [c16]Wilayat Khan, Alwen Tiu, David Sanán:
VeriFormal: An Executable Formal Model of a Hardware Description Language. SG-CRC 2017: 19-36 - [c15]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: 481-498 - [i6]Yongwang Zhao, David Sanán, Fuyuan Zhang, Yang Liu:
High-Assurance Separation Kernels: A Survey on Formal Methods. CoRR abs/1701.01535 (2017) - [i5]Yongwang Zhao, David Sanán, Fuyuan Zhang, Yang Liu:
Refinement-based Specification and Security Analysis of Separation Kernels. CoRR abs/1702.05997 (2017) - 2016
- [j7]Zhe Hou, David Sanán, Alwen Tiu, Rajeev Goré, Ranald Clouston:
Separata: Isabelle tactics for Separation Algebra. Arch. Formal Proofs 2016 (2016) - [j6]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) - [j5]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): 1321-1331 (2016) - [c14]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: 388-405 - [c13]Yongwang Zhao, David Sanán, Fuyuan Zhang, Yang Liu:
Reasoning About Information Flow Security of Separation Kernels with Channel-Based Communication. TACAS 2016: 791-810 - [i4]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 abs/1611.00574 (2016) - 2015
- [c12]David Sanán, Yang Liu, Yongwang Zhao, Zhenchang Xing, Mike Hinchey:
Verifying FreeRTOS' Cyclic Doubly Linked List Implementation: From Abstract Specification to Machine Code. ICECCS 2015: 120-129 - [c11]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: 281-292 - [i3]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 abs/1508.06479 (2015) - [i2]Yongwang Zhao, David Sanán, Fuyuan Zhang, Yang Liu:
Reasoning About Information Flow Security of Separation Kernels with Channel-based Communication. CoRR abs/1510.05091 (2015) - 2014
- [c10]David Sanán, Andrew Butterfield, Mike Hinchey:
Separation Kernel Verification: The Xtratum Case Study. VSTTE 2014: 133-149 - 2013
- [j4]María-del-Mar Gallardo, David Sanán:
Verification of complex dynamic data tree with mu-calculus. Autom. Softw. Eng. 20(4): 569-612 (2013) - [c9]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: 515-535 - 2012
- [j3]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): 375-392 (2012) - 2011
- [c8]Manchun Zheng, Jun Sun, David Sanán, Yang Liu, Jin Song Dong, Yu Gu:
Towards bug-free implementation for wireless sensor networks. SenSys 2011: 407-408 - 2010
- [c7]María-del-Mar Gallardo, David Sanán:
Verification of Dynamic Data Tree with mu-calculus Extended with Separation. SEFM 2010: 211-221
2000 – 2009
- 2009
- [j2]María-del-Mar Gallardo, Pedro Merino, David Sanán:
Model Checking Dynamic Memory Allocation in Operating Systems. J. Autom. Reason. 42(2-4): 229-264 (2009) - [j1]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): 359-374 (2009) - 2008
- [c6]María-del-Mar Gallardo, Pedro Merino, David Sanán:
Model Checking C Programs with Dynamic Memory Allocation. COMPSAC 2008: 219-226 - [i1]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) - 2007
- [c5]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: 321-329 - [c4]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: 268-273 - [c3]María-del-Mar Gallardo, Pedro Merino, David Sanán:
Extending CADP for Analyzing C Code. MSVVEIS 2007: 104-113 - 2006
- [c2]María-del-Mar Gallardo, Pedro Merino, David Sanán:
Towards Model Checking C Code with OPEN/CÆSAR. MSVVEIS 2006: 198-201 - 2005
- [c1]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: 17-26
Coauthor Index
manage site settings
To protect your privacy, all features that rely on external API calls from your browser are turned off by default. You need to opt-in for them to become active. All settings here will be stored as cookies with your web browser. For more information see our F.A.Q.
Unpaywalled article links
Add open access links from 
to the list of external document links (if available).
Privacy notice: By enabling the option above, your browser will contact the API of unpaywall.org to load hyperlinks to open access articles. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Unpaywall privacy policy.
Archived links via Wayback Machine
For web page which are no longer available, try to retrieve content from the 
of the Internet Archive (if available).
Privacy notice: By enabling the option above, your browser will contact the API of archive.org to check for archived content of web pages that are no longer available. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Internet Archive privacy policy.
Reference lists
Add a list of references from 
, 
, and 
to record detail pages.
load references from crossref.org and opencitations.net
Privacy notice: By enabling the option above, your browser will contact the APIs of crossref.org, opencitations.net, and semanticscholar.org to load article reference information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Crossref privacy policy and the OpenCitations privacy policy, as well as the AI2 Privacy Policy covering Semantic Scholar.
Citation data
Add a list of citing articles from and to record detail pages.
load citations from opencitations.net
Privacy notice: By enabling the option above, your browser will contact the API of opencitations.net and semanticscholar.org to load citation information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the OpenCitations privacy policy as well as the AI2 Privacy Policy covering Semantic Scholar.
OpenAlex data
Load additional information about publications from 
.
Privacy notice: By enabling the option above, your browser will contact the API of openalex.org to load additional information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the information given by OpenAlex.
last updated on 2024-08-05 20:22 CEST by the dblp team
all metadata released as open data under CC0 1.0 license
see also: Terms of Use | Privacy Policy | Imprint
dblp was originally created in 1993 at:
since 2018, dblp has been operated and maintained by:
the dblp computer science bibliography is funded and supported by:
