- Google PhD Fellowship Nominee – one of only 4 Ph.D. students selected by MSU (2021)
- University Graduate Research Fellowship – full summer support, MSU (2020)
Announcement:
I recently joined Harvard University as a
Postdoctoral Research Fellow, working with
Prof. Nada Amin on Formal Methods + AI (since March 2026)!
Tzu-Han Hsu
Hi, I'm Tzu-Han, from Taiwan! I am a Postdoctoral Research Fellow at Harvard University, working with Prof. Nada Amin on integrating AI with formal methods. I earned my Ph.D. in Computer Science from Michigan State University, advised by Dr. Borzoo Bonakdarpour.
My Ph.D.: Security & Privacy
My doctoral research centered on the formal verification and security of computer systems — spanning Formal Methods / Model Checking / Synthesis of Hyperproperties / Security and Privacy / Information-Flow Security — all driven by one goal: ensuring the soundness and trustworthiness of programs through efficient, provably correct verification algorithms.
Now Exploring: AI + Formal Methods
Building on my Ph.D. training, my current research focuses on integrating AI — specifically large language models (LLMs) — with formal methods.
The aim is to unite the reasoning power of modern AI with the rigor of formal guarantees, so that intelligent systems can be both capable and provably trustworthy.
Beyond Research: Musik!
I have studied piano and violin for 18+ years. I performed Tchaikovsky's Piano Concerto No.1 with the ISU Symphony Orchestra in 2015, held a Solo Piano Recital in 2017, and served as Assistant Principal violinist of the ISU Symphony Orchestra.
I have also worked as a concert accompanist, and piano/violin instructor for young musicians.
Recent News
2026
May
Our paper "HyPOLE: Hyperproperty-Guided Multi-Agent Reinforcement Learning under Partial Observation" is accepted to ICML'26!
Feb.
I successfully passed my Ph.D. defense!
2025
Sep.
Our paper "HypRL: Reinforcement Learning of Control Policies for Hyperproperties" is accepted to NeurIPS'25!
July
Our journal paper "Gray-box Runtime Enforcement of Hyperproperties" is accepted to Acta Informatica!
April
I successfully passed the comprehensive exam and officially became a Ph.D. candidate!
2024
2023
May
I will join Microsoft Research (MSR) as a research intern this Summer!
Citations
Papers
Piano repertoire
Cups of Coffee
Journal Papers
| 2025 | Gray-box Runtime Enforcement of Hyperproperties |
Acta Informaticato appear | [pdf] |
Conference Papers
| 2026 | HyperQB2.0: A Bounded Model Checker for Hyperproperties |
CAV'26to appear | [arXiv] |
| 2026 | HyPOLE: Hyperproperty-Guided Multi-Agent Reinforcement Learning under Partial Observation |
ICML'26to appear | [openreview] |
| 2025 | HypRL: Reinforcement Learning of Control Policies for Hyperproperties |
NeurIPS'25San Diego, CA | [arXiv] |
| 2024 | Syntax-Guided Automated Program Repair for Hyperproperties |
CAV'24Montreal, Canada | [pdf] [springer] |
| 2023 | Efficient Loop Conditions for Bounded Model Checking Hyperproperties |
TACAS'23Paris, France | [pdf] [springer] |
| 2023 | Bounded Model Checking for Asynchronous Hyperproperties |
TACAS'23Paris, France | [pdf] [springer] |
| 2022 | Mapping Synthesis for Hyperproperties |
CSF'22Haifa, Israel | [pdf] |
| 2021 | Bounded Model Checking for Hyperproperties |
TACAS'21Luxembourg | [pdf] [springer] |
Preprints
Education, Research, Teaching
Education
Ph.D., Computer Science & Engineering
Michigan State University · 2020–2026 · GPA 3.94/4.0 · Advisor: Dr. Borzoo Bonakdarpour
Michigan State University · 2020–2026 · GPA 3.94/4.0 · Advisor: Dr. Borzoo Bonakdarpour
B.S., Computer Science
Iowa State University · 2016–2020 · GPA 3.86/4.0
Iowa State University · 2016–2020 · GPA 3.86/4.0
B.A., Piano Performance
Iowa State University · 2013–2017 · GPA 3.86/4.0
Iowa State University · 2013–2017 · GPA 3.86/4.0
Research Experience
Postdoctoral Research Fellow · Harvard University
2026–Present · with Prof. Nada Amin
2026–Present · with Prof. Nada Amin
Graduate Research Assistant · Michigan State University
2020–2026 · Formal verification & synthesis for hyperproperties on privacy & security policies
2020–2026 · Formal verification & synthesis for hyperproperties on privacy & security policies
Undergraduate Research Assistant · Iowa State University
2019–2020 · Model checking & hyperproperties
2019–2020 · Model checking & hyperproperties
Professional Services
Program Committee Conference Reviewer Artifact Review Journal Review Student VolunteerResearch Mentoring & Teaching
Graduate Mentees (MSU) Undergraduate Mentees (MSU) Teaching AssistantReferences
Dr. Borzoo Bonakdarpour
Ph.D. Advisor · Associate Professor, CSE, Michigan State University · borzoo@msu.edu
Ph.D. Advisor · Associate Professor, CSE, Michigan State University · borzoo@msu.edu
Dr. César Sánchez
Research Collaborator · Associate Research Professor, IMDEA Software / CSIC · cesar.sanchez@imdea.org
Research Collaborator · Associate Research Professor, IMDEA Software / CSIC · cesar.sanchez@imdea.org
Industrial Experience
Research Intern · Microsoft Research
Summer 2023 · Framework to prove smart-contract safety, applied to Uniswap v2 [arXiv]
Summer 2023 · Framework to prove smart-contract safety, applied to Uniswap v2 [arXiv]
Applied Scientist Intern · Amazon (AWS)
Summer 2022 · Multi-threaded symbolic model checking on EC2 for industrial-scale protocols
Summer 2022 · Multi-threaded symbolic model checking on EC2 for industrial-scale protocols
Software Engineer Intern · Worrell Medical Design
Summer 2018 · VR usability-testing environment on Oculus Quest (Unity / C#)
Summer 2018 · VR usability-testing environment on Oculus Quest (Unity / C#)
Highlights of My Research Career
I won the MSU CSE Graduate 3MT Award!
I graduated from Dr. Borzoo Bonakdarpour’s group
I defended my Ph.D. thesis!
Joining Prof. Nada Amin’s group @ Harvard
I met with Prof. Ruzica!
← scroll for more → · add your photos to images/honors/
- 3MT Winner – Michigan State University CSE Department (2026)
- Outstanding Senior Nominee (2020)
- Magna Cum Laude – double-degree GPA 3.86 (2020)
- ISU CLAS Dean's List (2013–2020)
- International Student Ambassador Gold Scholarship, ISU (2013–2018)
- Music Dept. Outstanding Student Scholarship, ISU (2013–2018)
- Student Representative Council, Dept. Rep. elected, ISU (2015)
- 1st Prize – Fort Dodge Orchestra Young Artists Concerto Competition (2015)
- 1st Prize – ISU Symphony Orchestra Concerto Competition (2014); performed Tchaikovsky Piano Concerto No.1 at the Winner's Concert
- State Winner – MTNA Piano Competition (2014)
- Iowa Education without Borders – Volunteer / Event Coordinator (2017–18)
- Iowa Youth Leadership Summer Camp – Student Volunteer (2017–18)
- ISU K-12 Computational Thinking Competition (2018)
My Piano Recordings
"Music gives a soul to the universe, wings to the mind, flight to the imagination and life to everything." – Plato
Get in Touch!
Tzu-Han Hsu (she/her/hers)
Postdoctoral Research Fellow · Harvard University
School of Engineering and Applied Sciences
- tzuhan@seas.harvard.edu
- Harvard University, Science and Engineering Complex
Room 4.420, 150 Western Ave, Boston, MA - tzuhancs.github.io