Formalization of Laplace Transform Using the Multivariable Calculus Theory of HOL-Light. - Syeda Hira Taqdees; Osman Hasan (LPAR, 2013)

Reasoning about Translation Lookaside Buffers. - Hira Taqdees Syeda; Gerwin Klein (LPAR, 2017)

Formally Verifying Transfer Functions of Linear Analog Circuits. - Syeda Hira Taqdees; Osman Hasan (IEEE Des. Test, 2017)

Program Verification in the Presence of Cached Address Translation. - Hira Taqdees Syeda; Gerwin Klein (ITP, 2018)

Low-level program verification under cached address translation. - Hira Taqdees Syeda (2019)

Formal Reasoning Under Cached Address Translation. - Hira Taqdees Syeda; Gerwin Klein (J. Autom. Reason., 2020)

Do you have space for dessert? a verified space cost semantics for CakeML programs. - Alejandro Gómez-Londoño; Johannes Åman Pohjola; Hira Taqdees Syeda; Magnus O. Myreen; Yong Kiam Tan (Proc. ACM Program. Lang., 2020)

Pancake: Verified Systems Programming Made Sweeter. - Johannes Åman Pohjola; Hira Taqdees Syeda; Miki Tanaka; Krishnan Winter; Tsun Wang Sau; Benjamin Nott; Tiana J. Tsang Ung; Craig McLaughlin; Remy Seassau; Magnus O. Myreen; Michael Norrish; Gernot Heiser (PLOS@SOSP, 2023)

A Formally Verified Robustness Certifier for Neural Networks. - James Tobler; Hira Taqdees Syeda; Toby Murray (CAV (2), 2025)

Formally Verified Cloud-Scale Authorization. - Aleks Chakarov; Jaco Geldenhuys; Matthew Heck; Michael Hicks 001; Sam Huang; Georges-Axel Jaloyan; Anjali Joshi; K. Rustan M. Leino; Mikael Mayer; Sean McLaughlin; Akhilesh Mritunjai; Clément Pit-Claudel; et al. (ICSE, 2025)

Verifying Device Drivers with Pancake. - Junming Zhao; Alessandro Legnani; Tiana J. Tsang Ung; H. Truong; Tsun Wang Sau; Miki Tanaka; Johannes Åman Pohjola; Thomas Sewell; Robert Sison; Syeda Hira; Magnus Myreen; Michael Norrish; et al. (CoRR, 2025)

A Formally Verified Robustness Certifier for Neural Networks (Extended Version). - James Tobler; Hira Taqdees Syeda; Toby Murray (CoRR, 2025)