Formalizing Mobile Ad Hoc and Sensor Networks Using VDM-SL. - Shehla Riaz; Hamra Afzaal; Muhammad Imran 001; Nazir Ahmad Zafar; Mehmet Sabih Aksoy (EUSPN/ICTH, 2015)

Implementing Partitioning Detection and Connectivity Restoration in WSAN Using VDM-SL. - Hamra Afzaal; Muhammad Imran 001; Nazir Ahmad Zafar (FIT, 2015)

Towards Formalism of Earthquake Detection and Disaster Reduction Using WSANs. - Hamra Afzaal; Nazir Ahmad Zafar (FIT, 2016)

Formal analysis of subnet-based failure recovery algorithm in wireless sensor and actor and network. - Hamra Afzaal; Nazir Ahmad Zafar (Complex Adapt. Syst. Model., 2016)

Modeling of Sewerage System Using Internet of Things for Smart City. - Saba Latif; Hamra Afzaal; Nazir Ahmad Zafar (FIT, 2017)

Modeling of IoT-based border protection system. - Hamra Afzaal; Nazir Ahmad Zafar (INTELLECT, 2017)

Formal model of earthquake disaster mitigation and management system. - Nazir Ahmad Zafar; Hamra Afzaal (Complex Adapt. Syst. Model., 2017)

Hybrid subnet-based node failure recovery formal procedure in wireless sensor and actor networks. - Hamra Afzaal; Nazir Ahmad Zafar; Fahad Alhumaidan (Int. J. Distributed Sens. Networks, 2017)

Modelling of Graph-Based Smart Parking System Using Internet of Things. - Saba Latif; Hamra Afzaal; Nazir Ahmad Zafar (FIT, 2018)

Formal Modeling and Verification of a Blockchain-Based Crowdsourcing Consensus Protocol. - Hamra Afzaal; Muhammad Imran 001; Muhammad Umar Janjua; Sarada Prasad Gochhayat (IEEE Access, 2022)

Formal verification of persistence and liveness in the trust-based blockchain crowdsourcing consensus protocol. - Hamra Afzaal; Muhammad Imran 001; Muhammad Umar Janjua (Comput. Commun., 2022)

Formal verification of fraud-resilience in a crowdsourcing consensus protocol. - Hamra Afzaal; Muhammad Imran 001; Muhammad Umar Janjua (Comput. Secur., 2023)

Formal Verification of Justification and Finalization in Beacon Chain. - Hamra Afzaal; Nazir Ahmad Zafar; Aqsa Tehseen; Shaheen Kousar; Muhammad Imran 001 (IEEE Access, 2024)

Formal Verification of Rewards and Penalties Mechanism of FFG Attestations: Ethereum 2.0 Beacon Chain Case Study. - Muhammad Rashid; Imran Rasool; Nazir Ahmad Zafar; Hamra Afzaal (IEEE Access, 2025)

Model Checking of Rewards and Penalties in Beacon Chain. - Hamra Afzaal; Nazir Ahmad Zafar; Aqsa Tehseen; Shaheen Kousar (Int. J. Networked Distributed Comput., 2025)