David Sanán

Available identifiers

zbMath Open sanan.davidMaRDI QIDQ835782

List of research outcomes

Publication	Date of Publication	Type
Formally understanding Rust's ownership and borrowing system at the memory level	2025-01-13	Paper
A parametric rely-guarantee reasoning framework for concurrent reactive systems	2024-03-14	Paper
A verified specification of TLSF memory management allocator using state monads	2024-03-12	Paper
An Isabelle/HOL formalisation of the SPARC instruction set architecture and the TSO memory model	2021-06-09	Paper
Compositional reasoning for shared-variable concurrent programs	2021-05-04	Paper
CSimpl: a rely-guarantee-based framework for verifying concurrent programs	2020-08-05	Paper
Proof tactics for assertions in separation logic	2018-01-04	Paper
State space reduction for sensor networks using two-level partial order reduction	2014-11-03	Paper
Model checking dynamic memory allocation in operating systems	2009-08-31	Paper

Research outcomes over time

This page was built for person: David Sanán