cv
Basics
| Name | Shabnam Ghasemirad |
| Label | PhD Student at Information Security Group, Department of Computer Science, ETH Zurich |
| shabnam.ghasemirad (at) inf.ethz.ch |
Interests
| Formal Verification | |
| Protocol Verification | |
| Isabelle/HOL | |
| Refinement | |
| Formal Methods | |
| Foundations of Programming |
| Distributed Database Systems | |
| Concurrency Control Protocols | |
| Isolation Guarantees | |
| Database Transactions | |
| Data Management | |
| Distributed Systems |
Education
-
2022.11 - Present Zurich, Switzerland
-
2020.09 - 2022.11 Zurich, Switzerland
MSc
ETH Zurich
Computer Science
- Formal Methods in Information Security (6)
- Program Verification (5.75)
- Data Management Systems (5.75)
- Informal Methods (5.75)
- Information Security Lab (6)
-
2015.09 - 2020.02 Tehran, Iran
Publications
-
September 2026 Reduce Once, Verify Many: Verifying Isolation Guarantees via Hierarchical Abstractions
SCCP 2026, co-located with VLDB 2026 — accepted for presentation (non-archival)
To be presented at the 1st Symposium on Consistency Checking Principles (SCCP 2026).
-
May 2025 Pushing the Limit: Verified Performance-Optimal Causally-Consistent Database Transactions
TACAS 2025, as Part of ETAPS 2025
Presented at TACAS 2025 in Hamilton, ON, Canada. Isabelle/HOL formalization: https://github.com/ShabnamRad/EPplus
-
January 2025 VerIso: Verifiable Isolation Guarantees for Database Transactions
Proc. VLDB Endow., 2025
Presented at VLDB 2025 in London, UK. Isabelle/HOL framework: https://github.com/ShabnamRad/VerIso
Projects
- Apr 2022 - Oct 2022
Master’s Thesis, ETH Zurich
Mechanized Data Consistency Models for Distributed Database Transactions
- Supervisors: Dr. Christoph Sprenger, Dr. Si Liu, Prof. David Basin
- Information Security Group
- Feb 2021 - Jun 2021
Master’s Semester Project, ETH Zurich
Modular Reasoning about Distributed Systems in Igloo
- Supervisors: Dr. Christoph Sprenger, Dr. Si Liu, Prof. David Basin
- Information Security Group
- Jul 2019 - Dec 2019
Bachelor’s Thesis, Sharif University of Technology
Strategy Design for Expert Aggregation to Predict Stock Market
- Supervisor: Dr. MohammadAmin Fazli
- Algorithms & Systems Design Group
Work
-
Jun 2018 - Dec 2018 Research Intern
EPFL (École Polytechnique Fédérale de Lausanne)
An Improved Materialization Algorithm for DBToaster
- Supervisor: Prof. Amir Shaikhha
- Data Analysis Theory and Applications Lab (led by Prof. Christoph Koch)
-
Jul 2019 - Sep 2019 Research Intern
Max Planck Institute for Software Systems (MPI-SWS)
A Fine-Grained Concurrent Queue Verification in Iris/Coq Separation Logic Framework
- Supervisor: Prof. Derek Dreyer
- Foundations of Programming Group
Awards
- 2024
SNSF grant’s Employee (PhD Candidate) for the Project “Formal Verification of Isolation Guarantees in Database Systems”
SNSF (Swiss National Science Foundation)
- 2020
Direct Doctorate position and scholarship
ETH Zurich
- 2019
Ranked 8th in Cumulative GPA in the Department of Computer Engineering
Among about 130 B.Sc. students of the department, class of 2019
- 2019
Ranked 10th in National Student Olympiad for Computer Engineering
Among about 1,000 students
- 2015
Ranked 81st in Iranian National University Entrance Exam for BSc degree
Among about 300,000 students
Languages
| English | |
| Proficient (C1), TOEFL: 109 |
| German | |
| Upper Intermediate (B2) |
| French | |
| Pre-Intermediate (A2) |
| Persian | |
| Native Speaker |
Skills
| Theorem Provers | |
| Isabelle/HOL (expert) | |
| Rocq (Intermediate) | |
| Tamarin (Intermediate) | |
| LLM-assisted proof engineering in Isabelle/HOL |
| Database Systems | |
| SQL & RDBMSs (PostgreSQL, MySQL, SQLite) | |
| JSONiq | |
| Spark |
| Programming Languages | |
| Java | |
| Scala | |
| OCaml | |
| Python | |
| C/C++ |
| Web & Tools | |
| Git | |
| LaTeX | |
| Django | |
| ReactJs | |
| JavaScript | |
| HTML & CSS/SCSS |
| Arts and Sports | |
| Professional Classical Violin | |
| Piano | |
| Choir | |
| Ballet |