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:
|
|
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