David Sanán
TitleCited byYear
Model checking software with well-defined apis: the socket case
P de la Cámara, MM Gallardo, P Merino, D Sanan
Proceedings of the 10th international workshop on Formal methods for …, 2005
272005
Model checking dynamic memory allocation in operating systems
M del Mar Gallardo, P Merino, D Sanán
Journal of Automated Reasoning 42 (2-4), 229-264, 2009
232009
Towards model checking c code with open/cæsar
M del Mar Gallardo, P Merino, D Sanán
MSVVEIS, 198-201, 2006
162006
Separation kernel verification: The xtratum case study
D Sanán, A Butterfield, M Hinchey
Working Conference on Verified Software: Theories, Tools, and Experiments …, 2014
132014
CSimpl: A rely-guarantee-based framework for verifying concurrent programs
D Sanán, Y Zhao, Z Hou, F Zhang, A Tiu, Y Liu
International Conference on Tools and Algorithms for the Construction and …, 2017
122017
Reasoning about information flow security of separation kernels with channel-based communication
Y Zhao, D Sanán, F Zhang, Y Liu
International Conference on Tools and Algorithms for the Construction and …, 2016
112016
Event-based formalization of safety-critical operating system standards: An experience report on ARINC 653 using Event-B
Y Zhao, Z Yang, D Sanan, Y Liu
2015 IEEE 26th International Symposium on Software Reliability Engineering …, 2015
92015
State space reduction for sensor networks using two-level partial order reduction
M Zheng, D Sanán, J Sun, Y Liu, JS Dong, Y Gu
International Workshop on Verification, Model Checking, and Abstract …, 2013
82013
Towards bug-free implementation for wireless sensor networks
M Zheng, J Sun, D Sanán, Y Liu, JS Dong, Y Gu
Proceedings of the 9th ACM Conference on Embedded Networked Sensor Systems …, 2011
82011
Checking the reliability of socket based communication software
P de la Cámara, M del Mar Gallardo, P Merino, D Sanán
International journal on software tools for technology transfer 11 (5), 359, 2009
82009
On-the-fly model checking for C programs with extended CADP in FMICS-jETI
M del Mar Gallardo, P Merino, C Joubert, D Sanan
12th IEEE International Conference on Engineering Complex Computer Systems …, 2007
82007
FiB: Squeezing loop invariants by interpolation between forward/backward predicate transformers
SW Lin, J Sun, H Xiao, Y Liu, D Sanán, H Hansen
2017 32nd IEEE/ACM International Conference on Automated Software …, 2017
72017
An executable formalisation of the SPARCv8 instruction set architecture: a case study for the LEON3 processor
Z Hou, D Sanan, A Tiu, Y Liu, KC Hoa
International Symposium on Formal Methods, 388-405, 2016
72016
Executable operational semantics of Solidity
J Jiao, S Kan, SW Lin, D Sanan, Y Liu, J Sun
arXiv preprint arXiv:1804.01295, 2018
52018
Proof tactics for assertions in separation logic
Z Hóu, D Sanán, A Tiu, Y Liu
International Conference on Interactive Theorem Proving, 285-303, 2017
52017
Refinement-based specification and security analysis of separation kernels
Y Zhao, D Sanán, F Zhang, Y Liu
IEEE Transactions on Dependable and Secure Computing 16 (1), 127-141, 2017
52017
Formal specification and analysis of partitioning operating systems by integrating ontology and refinement
Y Zhao, D Sanán, F Zhang, Y Liu
IEEE Transactions on Industrial Informatics 12 (4), 1321-1331, 2016
52016
A model-extraction approach to verifying concurrent C programs with CADP
MM Gallardo, C Joubert, P Merino, D Sanán
Science of Computer Programming 77 (3), 375-392, 2012
52012
High-assurance separation kernels: a survey on formal methods
Y Zhao, D Sanán, F Zhang, Y Liu
arXiv preprint arXiv:1701.01535, 2017
42017
C. open and annotator: Tools for on-the-fly model checking c programs
M del Mar Gallardo, C Joubert, P Merino, D Sanán
International SPIN Workshop on Model Checking of Software, 268-273, 2007
42007
The system can't perform the operation now. Try again later.
Articles 1–20