David Miguel Sanan Baena

Publications

• Formalisation of a separation micro-kernel for common criteria certification
• Towards model checking C code with OPEN/CæSAR
• Extending CADP for analyzing C code
• C.OPEN and ANNOTATOR: Tools for on-the-fly model checking C programs
• Verification of dynamic data tree with mu-calculus extended with separation
• Model checking software with well-defined APIs: The socket case
• Refinement-based specification and security analysis of separation kernels
• Verification of complex dynamic data tree with mu-calculus
• FiB: Squeezing loop invariants by interpolation between forward/backward predicate transformers
• An executable formalisation of the SPARCv8 instruction set architecture: A case study for the LEON3 processor
• Demo: Towards bug-free implementation for wireless sensor networks
• A parametric rely-guarantee reasoning framework for concurrent reactive systems
• Model checking dynamic memory allocation in operating systems
• Verifying FreeRTOS' Cyclic Doubly Linked List Implementation: From Abstract Specification to Machine Code
• Rely-guarantee reasoning about concurrent memory management in zephyr RTOs
• A formally verified buddy memory allocation model
• Separation kernel verification: The xtratum case study
• Event-based formalization of safety-critical operating system standards: An experience report on ARINC 653 using Event-B
• A model-extraction approach to verifying concurrent C programs with CADP
• State space reduction for sensor networks using two-level partial order reduction
• Compositional reasoning for shared-variable concurrent programs
• CSimpl: A rely-guarantee-based framework for verifying concurrent programs
• Formal Specification and Analysis of Partitioning Operating Systems by Integrating Ontology and Refinement
• Checking the reliability of socket based communication software
• Proof tactics for assertions in separation logic
• Reasoning about information flow security of separation kernels with channel-based communication
• A verified specification of TLSF memory management allocator using state monads
• On embedding a hardware description language in Isabelle/HOL
• Model checking C programs with dynamic memory allocation
• On-the-fly model checking for C programs with extended CADP in FMICS-jETI
• VeriFormal: An executable formal model of a hardware description language
• CSim 2
• Automatic Verification of Multi-threaded Programs by Inference of Rely-Guarantee Specifications
• Semantic Understanding of Smart Contracts: Executable Operational Semantics of Solidity
• CANeleon: Protecting CAN Bus With Frame ID Chameleon
• An Isabelle/HOL Formalisation of the SPARC Instruction Set Architecture and the TSO Memory Model
• Formalizing x86-64 ISA in Isabelle/HOL: A Binary Semantics for eBPF JIT Correctness
• Generically Automating Separation Logic by Functors, Homomorphisms, and Modules
• Automated Program Refinement: Guide and Verify Code Large Language Model with Refinement Calculus