Publications

Book Chapters

Developing portable embedded software for multicore systems through formal abstraction and refinement
Asieh Salehi Fathabadi, Sadegh Dalvandi and Michael Butler
in Many-Core Computing: Hardware and Software 2019 Book Chapter

Journal Papers

Implementing and verifying release-acquire transactional memory in C11
Sadegh Dalvandi, Brijesh Dongol
in Proceedings of the ACM on Programming Languages, Volume 6, Issue OOPSLA2 2022 Journal
Unifying Operational Weak Memory Verification: An Axiomatic Approach
Simon Doherty, Sadegh Dalvandi, Brijesh Dongol , Heike Wehrheim
in ACM Transactions on Computational Logic 2022 Journal
Integrating Owicki–Gries for C11-Style Memory Models into Isabelle/HOL
Sadegh Dalvandi, Brijesh Dongol, Simon Doherty & Heike Wehrheim
in Journal of Automated Reasoning 2021 Journal
Formalising the Hybrid ERTMS Level 3 specification in iUML-B and Event-B
Dana Dghaym, Sadegh Dalvandi, Michael Poppleton & Colin Snook
in International Journal on Software Tools for Technology Transfer 2020 Journal
Verifying Cross-Layer Interactions Through Formal Model-Based Assertion Generation
Asieh Salehi Fathabadi, Sadegh Dalvandi, Michael Butler and Bashir M. Al-Hashimi
in IEEE Embedded Systems Letters 2020 Journal
Derivation of algorithmic control structures in Event-B refinement
Sadegh Dalvandi, Michael Butler & Abdolbaghi Rezazadeh
in Science of Computer Programming 2017 Journal

Conference Papers

Verifying C11-style weak memory libraries
Sadegh Dalvandi & Brijesh Dongol
in PPoPP '21: Proceedings of the 26th ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming 2021 Conference
Owicki-Gries Reasoning for C11 RAR
Sadegh Dalvandi, Simon Doherty, Brijesh Dongol, and Heike Wehrheim
in 34th European Conference on Object-Oriented Programming (ECOOP 2020) 2020 Conference
SEB-CG: Code Generation Tool with Algorithmic Refinement Support for Event-B
Sadegh Dalvandi, Michael Butler, and Asieh Salehi Fathabadi
in FM 2019 International Workshops 2019 Conference
Towards deductive verification of C11 programs with Event-B and ProB
Sadegh Dalvandi and Brijesh Dongol
in FTfJP '19: Proceedings of the 21st Workshop on Formal Techniques for Java-like Program 2019 Conference
Transforming Event-B models to Dafny contracts
Sadegh Dalvandi, Michael Butler, Abdolbaghi Rezazadeh
in 15th International Workshop on Automated Verification of Critical Systems (AVoCS 2015) 2015 Conference
From Event-B models to Dafny code contracts
Sadegh Dalvandi, Michael Butler, Abdolbaghi Rezazadeh
in 6th IPM International Conference on Fundamentals of Software Engineering (FSEN 2015) 2015 Conference

Thesis

Developing verified sequential programs with Event-B
Sadegh Dalvandi
in University of Southampton 2018 Publications

PrePrints/Technical Reports

Implementing and Verifying Release-Acquire Transactional Memory (Extended Version)
Sadegh Dalvandi, Brijesh Dongol
in arXiv preprint arXiv:2208.00315 2022 Preprint
Verifying C11-Style Weak Memory Libraries via Refinement
Sadegh Dalvandi, Brijesh Dongol
in arXiv preprint arXiv:2108.06944 2021 Preprint
Integrating Owicki-Gries for C11-Style Memory Models into Isabelle/HOL
Sadegh Dalvandi, Brijesh Dongol, and Simon Doherty
in arXiv 2020 Preprint