Welcome :-)


I have know-how and know-why about:


Programs: low-level (operating system kernels, compilers);
Hardware: software-visible (caches, page tables);
Modelling: mathematical;
Abstraction: functional;
Logic & reasoning: higher-order;
Verification: theorem proving;
Proof: machine-checked;
Guarantees: functional, security, privacy;
Programming: functional; and
Types: static.

Theorem provers that I frequently use:

isabelle
Isabelle/HOL
hol
HOL4

Postdoctoral Research:

I am the main contributor to Pancake: an imperative language with simpler memory model and formally verified implementation to program cyber-physical systems. Pancake compiles to the lower stack of the CakeML compiler.
With: Magnus Myreen, Affiliation: Chalmers University, Sweden

PhD Research:

My PhD research addresses low-level program verification in the presence of cached address translation. [more] [thesis]
Advisor: Gerwin Klein, Affiliation: Data61, CSIRO and UNSW, Australia

Community Service:


Program Committee Member: CPP 2022
Artifact Evaluation Committee Member: CAV 2021
Reviewer and Sub-reviewer: ITP 2021, CPP 2021, ASPLOS 2020, SEFM 2020, TFP 2020, CPP 2019, FM 2018, ICFP 2018, CADE26

Publications:

Journal Papers

Formal reasoning under cached address translation [pdf]
Hira T. Syeda and Gerwin Klein
In: JAR2020

Formally verifying transfer functions of linear analog circuits [pdf]
Hira T. Syeda and Osman Hasan
In: IEEE Design & Test, 2017

Conference Papers:

Do you have space for dessert? a verified space cost semantics for CakeML programs [pdf]
Alejandro Gomez and Johannes A. Pohjola and Hira T. Syeda and Magnus Myreen and Yong Kiam Tan
In: OOPSLA2020

Program verification in the presence of cached address translation [pdf] [slides]
Hira T. Syeda and Gerwin Klein
In: ITP2018

Reasoning about translation lookaside buffers [pdf] [slides]
Hira T. Syeda and Gerwin Klein
In: LPAR2017

Formalization of laplace transform using the multivariable calculus theory of HOL Light [pdf] [slides]
Hira T. Syeda and Osman Hasan
In: LPAR2013