⠀

I am a research fellow at University of Surrey working with Dr Brijesh Dongol. My main research interest is Formal Methods in Software Engineering. I am particularly interested in tools and methods for developing verified programs and program verification. Currently my focus is on verification of concurrent programs under weak memory. Prior to joining Surrey University, I was a research fellow at University of Southampton working with Professor Michael Butler on PRiME project.

I did my PhD in Computer Science under supervision of Professor Michael Butler at School of Electronic and Computer Science, University of Southampton. I obtained a Master’s degree in Software Engineering from the University of Southampton (2012).

I can be reached at sadegh [at sign] dalvandi [dot] com.

Social Media

News

[09/04/2020] Our paper "Owicki-Gries Reasoning for C11 RAR" was accepted to ECOOP 2020.
[18/09/2019] Our paper "Formalising the Hybrid ERTMS Level 3 specification in iUML-B and Event-B" has been accepted to the International Journal on Software Tools for Technology Transfer.
[16/09/2019] Our paper "Verifying Cross-layer Interactions through Formal Model-based Assertion Generation" has been accepted to IEEE Embedded Systems Letters.
[08/08/2019] Our paper "SEB-CG: Code Generation Tool with Algorithmic Refinement Support for Event-B" has been accepted to Workshop on Practical Formal Verification for Software Dependability (AFFORD 2019)
[12/06/2019] Our paper "Towards Deductive Verification of C11 Programs with Event-B and ProB" has been accepted to the 21st Workshop on Formal Techniques for Java-like Programs (FTfJP 2019)
[7/06/2019] Our book chapter "Developing portable embedded software for multicore systems through formal abstraction and refinement" has been published.

Publications

Dalvandi, M., Dongol, B. and Doherty, S., 2020. Integrating Owicki-Gries for C11-Style Memory Models into Isabelle/HOL. arXiv preprint arXiv:2004.02983.
Fathabadi, A.S., Dalvandi, M., Butler, M. and Al-Hashimi, B.M., 2019. Verifying Cross-layer Interactions through Formal Model-based Assertion Generation. IEEE Embedded Systems Letters.
Dghaym, D., Dalvandi, M., Poppleton, M. and Snook, C., 2019. Formalising the Hybrid ERTMS Level 3 specification in iUML-B and Event-B. International Journal on Software Tools for Technology Transfer, pp.1-17.
Dalvandi, M, Butler, Michael and Salehi Fathabadi, Asieh (2019) SEB-CG: Code generation tool with algorithmic refinement support for Event-B. Practical Formal Verification for Software Dependability: co-located with the Formal Methods 2019 (FM'19), Portugal. 07 Oct 2019.
M Dalvandi, B Dongol. (2019, July). Towards deductive verification of C11 programs with Event-B and ProB. In Proceedings of the 21st Workshop on Formal Techniques for Java-like Programs (p. 4). ACM.
A Salehi Fathabadi , M Dalvandi and M Butler (2019) Developing portable embedded software for multicore systems through formal abstraction and refinement. In, Al-Hashimi, Bashir M. and Merrett, Geoff V. (eds.) Many-Core Computing: Hardware and Software. Institute of Engineering and Technology, IET.
M Dalvandi, A Salehi Fathabadi, M Butler, A report on PRiME code generation activities. 7th Rodin Workshop, Southampton, United Kingdom. 05 Jun 2018.
M Dalvandi, A Salehi Fathabadi, M Butler, Using formal methods for automatic platform-independent code generation of run-time management. University Booth at DATE 2018, Dresden, Germany. 19 - 22 Mar 2018.
M Dalvandi, M Butler, A Rezazadeh, A Salehi Fathabadi (2018) Verifiable code generation from scheduled Event-B models. In 6th International ABZ Conference ASM, Alloy, B, TLA, VDM, Z, 2018, Proceedings of
M Dalvandi, M Butler, A Rezazadeh, Derivation of algorithmic control structures in Event-B refinement, Journal of Science of Computer Programming, Volume 148, 2017, Pages 49-65, ISSN 0167-6423,
M Dalvandi, M Butler, A Rezazadeh, Transforming Event-B models to Dafny contracts, 15th International Workshop on Automated Verification of Critical Systems (AVoCS 2015), 2015
M Dalvandi, M Butler, A Rezazadeh, From Event-B models to Dafny code contracts, 6th IPM International Conference on Fundamentals of Software Engineering (FSEN 2015), 2015
M Dalvandi, M Butler, Towards Verified Implementation of Event-B Models in Dafny, 5th Rodin User and Developer Workshop, 2014