From Event-B Models to Dafny Code Contracts. - Mohammadsadegh Dalvandi; Michael J. Butler; Abdolbaghi Rezazadeh (FSEN, 2015)

Transforming Event-B Models to Dafny Contracts. - Mohammadsadegh Dalvandi; Michael J. Butler; Abdolbaghi Rezazadeh (Electron. Commun. Eur. Assoc. Softw. Sci. Technol., 2015)

Derivation of algorithmic control structures in Event-B refinement. - Mohammadsadegh Dalvandi; Michael J. Butler; Abdolbaghi Rezazadeh (Sci. Comput. Program., 2017)

Verifiable Code Generation from Scheduled Event-B Models. - Mohammadsadegh Dalvandi; Michael J. Butler; Abdolbaghi Rezazadeh; Asieh Salehi Fathabadi (ABZ, 2018)

Towards deductive verification of C11 programs with Event-B and ProB. - Mohammadsadegh Dalvandi; Brijesh Dongol (FTfJP@ECOOP, 2019)

SEB-CG: Code Generation Tool with Algorithmic Refinement Support for Event-B. - Mohammadsadegh Dalvandi; Michael J. Butler; Asieh Salehi Fathabadi (FM Workshops (1), 2019)

Owicki-Gries Reasoning for C11 RAR. - Sadegh Dalvandi; Simon Doherty; Brijesh Dongol; Heike Wehrheim (ECOOP, 2020)

Integrating Owicki-Gries for C11-Style Memory Models into Isabelle/HOL. - Sadegh Dalvandi; Brijesh Dongol; Simon Doherty (CoRR, 2020)

Owicki-Gries Reasoning for C11 RAR (Artifact). - Sadegh Dalvandi; Simon Doherty; Brijesh Dongol; Heike Wehrheim (Dagstuhl Artifacts Ser., 2020)

Verifying Cross-Layer Interactions Through Formal Model-Based Assertion Generation. - Asieh Salehi Fathabadi; Mohammadsadegh Dalvandi; Michael J. Butler; Bashir M. Al-Hashimi (IEEE Embed. Syst. Lett., 2020)

Formalising the Hybrid ERTMS Level 3 specification in iUML-B and Event-B. - Dana Dghaym; Mohammadsadegh Dalvandi; Michael Poppleton; Colin F. Snook (Int. J. Softw. Tools Technol. Transf., 2020)

Verifying C11-style weak memory libraries. - Sadegh Dalvandi; Brijesh Dongol (PPoPP, 2021)

Verifying C11-Style Weak Memory Libraries via Refinement. - Sadegh Dalvandi; Brijesh Dongol (CoRR, 2021)

Implementing and Verifying Release-Acquire Transactional Memory (Extended Version). - Sadegh Dalvandi; Brijesh Dongol (CoRR, 2022)

Integrating Owicki-Gries for C11-Style Memory Models into Isabelle/HOL. - Sadegh Dalvandi; Brijesh Dongol; Simon Doherty; Heike Wehrheim (J. Autom. Reason., 2022)

Implementing and verifying release-acquire transactional memory in C11. - Sadegh Dalvandi; Brijesh Dongol (Proc. ACM Program. Lang., 2022)

Unifying Operational Weak Memory Verification: An Axiomatic Approach. - Simon Doherty; Sadegh Dalvandi; Brijesh Dongol; Heike Wehrheim (ACM Trans. Comput. Log., 2022)

Mechanised Operational Reasoning for C11 Programs with Relaxed Dependencies. - Daniel Wright 001; Sadegh Dalvandi; Mark Batty; Brijesh Dongol (Formal Aspects Comput., 2023)