David Sanán

Orcid: 0000-0003-2755-3089

According to our database1, David Sanán authored at least 56 papers between 2005 and 2024.

Collaborative distances:

Timeline

Legend:

Book 
In proceedings 
Article 
PhD thesis 
Dataset
Other 

Links

Online presence:

On csauthors.net:

Bibliography

2024
Towards Large Language Model Aided Program Refinement.
CoRR, 2024

A Parallel and Distributed Quantum SAT Solver Based on Entanglement and Teleportation.
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2024

Formalizing x86-64 ISA in Isabelle/HOL: A Binary Semantics for eBPF JIT Correctness.
Proceedings of the Dependable Software Engineering. Theories, Tools, and Applications, 2024

2023
Rely-guarantee Reasoning about Concurrent Memory Management: Correctness, Safety and Security.
CoRR, 2023

Rely-guarantee Reasoning about Concurrent Reactive Systems: The PiCore Framework, Languages Integration and Applications.
CoRR, 2023

Event-based Compositional Reasoning of Information-Flow Security for Concurrent Systems.
CoRR, 2023

A Parallel and Distributed Quantum SAT Solver Based on Entanglement and Quantum Teleportation.
CoRR, 2023

2022
A Quantum interpretation of separating conjunction for local reasoning of Quantum programs based on separation logic.
Proc. ACM Program. Lang., 2022

An Executable Formal Model of the VHDL in Isabelle/HOL.
CoRR, 2022

A Formal Methodology for Verifying Side-Channel Vulnerabilities in Cache Architectures.
Proceedings of the Formal Methods and Software Engineering, 2022

2021
CSim<sup><i>2</i></sup>: Compositional Top-down Verification of Concurrent Systems using Rely-Guarantee.
ACM Trans. Program. Lang. Syst., 2021

An Isabelle/HOL Formalisation of the SPARC Instruction Set Architecture and the TSO Memory Model.
J. Autom. Reason., 2021

2020
CANeleon: Protecting CAN Bus With Frame ID Chameleon.
IEEE Trans. Veh. Technol., 2020

Semantic Understanding of Smart Contracts: Executable Operational Semantics of Solidity.
Proceedings of the 2020 IEEE Symposium on Security and Privacy, 2020

Automatic Verification of Multi-threaded Programs by Inference of Rely-Guarantee Specifications.
Proceedings of the 25th International Conference on Engineering of Complex Computer Systems, 2020

2019
Refinement-Based Specification and Security Analysis of Separation Kernels.
IEEE Trans. Dependable Secur. Comput., 2019

On embedding a hardware description language in Isabelle/HOL.
Des. Autom. Embed. Syst., 2019

A formalisation of the SPARC TSO memory model for multi-core machine code.
CoRR, 2019

A Verified Specification of TLSF Memory Management Allocator Using State Monads.
Proceedings of the Dependable Software Engineering. Theories, Tools, and Applications, 2019

A Formally Verified Buddy Memory Allocation Model.
Proceedings of the 24th International Conference on Engineering of Complex Computer Systems, 2019

A Parametric Rely-Guarantee Reasoning Framework for Concurrent Reactive Systems.
Proceedings of the Formal Methods - The Next 30 Years - Third World Congress, 2019

Rely-Guarantee Reasoning About Concurrent Memory Management in Zephyr RTOS.
Proceedings of the Computer Aided Verification - 31st International Conference, 2019

2018
A Verified Timsort C Implementation in Isabelle/HOL.
CoRR, 2018

An Event-based Compositional Reasoning Approach for Concurrent Reactive Systems.
CoRR, 2018

K-Rust: An Executable Formal Semantics for Rust.
CoRR, 2018

Executable Operational Semantics of Solidity.
CoRR, 2018

Compositional Reasoning for Shared-Variable Concurrent Programs.
Proceedings of the Formal Methods - 22nd International Symposium, 2018

2017
High-Assurance Separation Kernels: A Survey on Formal Methods.
CoRR, 2017

CSimpl: A Rely-Guarantee-Based Framework for Verifying Concurrent Programs.
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2017

VeriFormal: An Executable Formal Model of a Hardware Description Language.
Proceedings of the A Systems Approach to Cyber Security, 2017

FiB: squeezing loop invariants by interpolation between Forward/Backward predicate transformers.
Proceedings of the 32nd IEEE/ACM International Conference on Automated Software Engineering, 2017

Proof Tactics for Assertions in Separation Logic.
Proceedings of the Interactive Theorem Proving - 8th International Conference, 2017

2016
Formal Specification and Analysis of Partitioning Operating Systems by Integrating Ontology and Refinement.
IEEE Trans. Ind. Informatics, 2016

Compositional Reasoning for Shared-variable Concurrent Programs.
CoRR, 2016

A formal model for the SPARCv8 ISA and a proof of non-interference for the LEON3 processor.
Arch. Formal Proofs, 2016

Separata: Isabelle tactics for Separation Algebra.
Arch. Formal Proofs, 2016

Reasoning About Information Flow Security of Separation Kernels with Channel-Based Communication.
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2016

An Executable Formalisation of the SPARCv8 Instruction Set Architecture: A Case Study for the LEON3 Processor.
Proceedings of the FM 2016: Formal Methods, 2016

2015
Event-based Formalization of Safety-critical Operating System Standards: An Experience Report on ARINC 653 using Event-B.
CoRR, 2015

Event-based formalization of safety-critical operating system standards: An experience report on ARINC 653 using Event-B.
Proceedings of the 26th IEEE International Symposium on Software Reliability Engineering, 2015

Verifying FreeRTOS' Cyclic Doubly Linked List Implementation: From Abstract Specification to Machine Code.
Proceedings of the 20th International Conference on Engineering of Complex Computer Systems, 2015

2014
Separation Kernel Verification: The Xtratum Case Study.
Proceedings of the Verified Software: Theories, Tools and Experiments, 2014

2013
Verification of complex dynamic data tree with mu-calculus.
Autom. Softw. Eng., 2013

State Space Reduction for Sensor Networks Using Two-Level Partial Order Reduction.
Proceedings of the Verification, 2013

2012
A model-extraction approach to verifying concurrent C programs with CADP.
Sci. Comput. Program., 2012

2011
Towards bug-free implementation for wireless sensor networks.
Proceedings of the 9th International Conference on Embedded Networked Sensor Systems, 2011

2010
Verification of Dynamic Data Tree with mu-calculus Extended with Separation.
Proceedings of the 8th IEEE International Conference on Software Engineering and Formal Methods, 2010

2009
Checking the reliability of socket based communication software.
Int. J. Softw. Tools Technol. Transf., 2009

Model Checking Dynamic Memory Allocation in Operating Systems.
J. Autom. Reason., 2009

2008
Web Services for Accessing Explicit State Space Verification Tools.
ERCIM News, 2008

Model Checking C Programs with Dynamic Memory Allocation.
Proceedings of the 32nd Annual IEEE International Computer Software and Applications Conference, 2008

2007
Extending CADP for Analyzing C Code.
Proceedings of the Modelling, 2007

C.OPEN and ANNOTATOR: Tools for On-the-Fly Model Checking C Programs.
Proceedings of the Model Checking Software, 2007

On-the-fly model checking for C programs with extended CADP in FMICS-jETI.
Proceedings of the 12th International Conference on Engineering of Complex Computer Systems (ICECCS 2007), 2007

2006
Towards Model Checking C Code with OPEN/CÆSAR.
Proceedings of the Modelling, 2006

2005
Model checking software with well-defined APIs: the socket case.
Proceedings of the 10th international workshop on Formal methods for industrial critical systems, 2005


  Loading...