The University of Southampton

Research

Research interests

Formal Methods, Program Analysis, Code Generation

Publications

Dalvandi, Mohammadsadegh, Butler, Michael and Rezazadeh, Abdolbaghi (2015) From Event-B models to Dafny code contracts. 6th IPM International Conference on Fundamentals of Software Engineering, Iran, Islamic Republic of. 22 - 24 Apr 2015.

Dalvandi, Mohammadsadegh, Butler, Michael and Rezazadeh, Abdolbaghi (2015) Transforming Event-B models to Dafny contracts. 15th International Workshop on Automated Verification of Critical Systems (AVoCS 2015), United Kingdom. 01 - 04 Sep 2015.

Dalvandi, Mohammad Sadegh, Butler, Michael and Rezazadeh, Abdolbaghi (2017) Derivation of algorithmic control structures in Event-B refinement. Science of Computer Programming, 148, 49-65. (doi:10.1016/j.scico.2017.05.010).

Dalvandi, Mohammad Sadegh, Butler, Michael, Rezazadeh, Abdolbaghi and Salehi Fathabadi, Asieh (2018) Verifiable code generation from scheduled event-B models. In Abstract State Machines, Alloy, B, TLA, VDM, and Z: ABZ 2018. vol. 10817, Springer. pp. 1-15 . (doi:10.1007/978-3-319-91271-4_16).

Dalvandi, Mohammad Sadegh, Salehi Fathabadi, Asieh and Butler, Michael (2018) Using formal methods for automatic platform-independent code generation of run-time management. University Booth at DATE 2018, Dresden, Germany. 19 - 22 Mar 2018.

Dalvandi, Mohammad Sadegh and Butler, Michael (2014) Towards verified implementation of Event-B models in Dafny. 5th Rodin User and Developer Workshop, Toulouse, France. 02 - 03 Jun 2014.

Dalvandi, Mohammad Sadegh, Salehi Fathabadi, Asieh and Butler, Michael (2018) A report on PRiME code generation activities. 7th Rodin Workshop, Southampton, United Kingdom. 05 Jun 2018.

Dalvandi, Mohammad Sadegh (2018) Developing verified sequential programs with Event-B. Electronics & Computer Science, Doctoral Thesis, 167pp.

Salehi Fathabadi, Asieh, Dalvandi, Mohammad Sadegh and Butler, Michael (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.

Dghaym, Dana and Snook, Colin (2019) Dataset for: Formalising the Hybrid ERTMS Level 3 specification in iUML-B and Event-B. University of Southampton doi:10.5258/SOTON/D0991 [Dataset]

Dalvandi, Mohammad Sadegh, 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), Porto, Portugal. 07 Oct 2019.

Dghaym, Dana, Dalvandi, Mohammad Sadegh, Poppleton, Michael and Snook, Colin (2019) Formalising the hybrid ERTMS level 3 specification in iUML-B and Event-B. International Journal on Software Tools for Technology Transfer. (doi:10.1007/s10009-019-00548-w). (In Press)

Contact

Share this profile FacebookTwitterWeibo