Travelled to:2 × Italy
Collaborated with:M.Gallardo Y.Zhao M.Zheng J.Sun Y.Liu J.S.Dong Y.Gu S.Lin J.S.0001 H.Xiao Y.L.0003 H.Hansen
Talks about:reduct (2) transform (1) interpol (1) guarante (1) calculus (1) backward (1) partial (1) network (1) forward (1) concurr (1)
Person: David Sanán
DBLP: San=aacute=n:David
Contributed to:
2013
2010
2017
2019Wrote 4 papers:
- VMCAI-2013-ZhengS0LD0 #network #partial order #reduction #using
- State Space Reduction for Sensor Networks Using Two-Level Partial Order Reduction (MZ, DS, JS, YL, JSD, YG), pp. 515–535.
- SEFM-2010-GallardoS #calculus #verification #μ-calculus
- Verification of Dynamic Data Tree with μ-calculus Extended with Separation (MdMG, DS), pp. 211–221.
- ASE-2017-LinSXLSH #invariant #named
- FiB: squeezing loop invariants by interpolation between Forward/Backward predicate transformers (SWL, JS0, HX, YL0, DS, HH), pp. 793–803.
- CAV-2019-ZhaoS #concurrent #memory management #reasoning
- Rely-Guarantee Reasoning About Concurrent Memory Management in Zephyr RTOS (YZ, DS), pp. 515–533.