• Hello!
    I'm Tzu-Han
    Download CV

  • I am a Research Fellow at
    Harvard University

  • I am also a pianist
    and violinist
    My Recordings
Announcement: I recently joined Harvard University as a Postdoctoral Research Fellow, working with Prof. Nada Amin on Formal Methods + AI (since March 2026)!
About Me

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

keep going

Recent News

2026
May
Our paper "HyperQB2.0: A Bounded Model Checker for Hyperproperties" is accepted to CAV'26!
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
May
Our paper "Syntax-Guided Automated Program Repair for Hyperproperties" is accepted to CAV'24!
2023
May
I will join Microsoft Research (MSR) as a research intern this Summer!
Show more news ▾
Citations
Papers
Piano repertoire
Cups of Coffee
My Publications

Journal Papers

2025
Gray-box Runtime Enforcement of Hyperproperties
Tzu-Han Hsu, Ana Oliveira da Costa, Andrew Wintenberg, Ezio Bartocci, Borzoo Bonakdarpour
 Acta Informaticato appear [pdf]

Conference Papers

2026
HyperQB2.0: A Bounded Model Checker for Hyperproperties
Tzu-Han Hsu, Milad Rabizadeh, Kenneth Rogale, Fedor Filippov, Marco A. de Oliveira Batista, Borzoo Bonakdarpour
 CAV'26to appear [arXiv]
2026
HyPOLE: Hyperproperty-Guided Multi-Agent Reinforcement Learning under Partial Observation
Arshia Rafieioskouei, Tzu-Han Hsu, Matthew Lucas, Borzoo Bonakdarpour
 ICML'26to appear [openreview]
2025
HypRL: Reinforcement Learning of Control Policies for Hyperproperties
Tzu-Han Hsu, Arshia Rafieioskouei, Borzoo Bonakdarpour
 NeurIPS'25to appear [arXiv]
2024
Syntax-Guided Automated Program Repair for Hyperproperties
Raven Beutner, Tzu-Han Hsu, Borzoo Bonakdarpour, Bernd Finkbeiner
 CAV'24Montreal, Canada [pdf] [springer]
2023
Efficient Loop Conditions for Bounded Model Checking Hyperproperties
Tzu-Han Hsu, César Sánchez, Sarai Sheinvald, Borzoo Bonakdarpour
 TACAS'23Paris, France [pdf] [springer]
2023
Bounded Model Checking for Asynchronous Hyperproperties
Tzu-Han Hsu, Borzoo Bonakdarpour, Bernd Finkbeiner, César Sánchez
 TACAS'23Paris, France [pdf] [springer]
2022
Mapping Synthesis for Hyperproperties
Tzu-Han Hsu, Borzoo Bonakdarpour, Eunsuk Kang, Stavros Tripakis
 CSF'22 [pdf]
2021
Bounded Model Checking for Hyperproperties
Tzu-Han Hsu, César Sánchez, Borzoo Bonakdarpour
 TACAS'21Luxembourg [pdf] [springer]

Preprints

2020
Multi-Agent Path Planning with Hyperproperties
Tzu-Han Hsu, Yu Wang, Borzoo Bonakdarpour, Miroslav Pajic
 Preprint [pdf]
My background

Education, Research, Teaching

Education

Ph.D. in Computer Science Engineering
      Advisor: Dr. Borzoo Bonakdarpour
      Michigan State University, 2020-2026 (GPA: 3.94/4.0)

Bachelor of Science in Computer Science
      Iowa State University, 2016-2020 (GPA: 3.86/4.0)
Bachelor of Arts in Piano Performance
      Iowa State University, 2013-2017 (GPA: 3.86/4.0)


Research Experience

Postdoctoral Research Fellow
Harvard University, 2026-Present
  • Working with Prof. Nada Amin
Graduate Research Assistant
Michigan State University, 2020-2026
  • Formal Verification and Synthesis for Hyperproperties on Privacy and Security Policies
Undergrad Research Assitant
Iowa State University, 2019-2020
  • Model Checking and Hyperproperties

Professional Services

Program Committee
  • International Conference on Embedded Software, WiP-LB TPC (EMSOFT'25)
Conference Paper Review
  • European Association for Computer Science Logic (CSL'25)
  • International Symposium on Reliable Distributed Systems (SRDS'24)
  • International Conference on Embedded Software (EMSOFT'24)
  • International Conference on Computer Aided Verification (CAV'24)
  • International Conference on Runtime Verification (RV'24'25)
  • Tools and Algorithms for the Construction and Analysis of Systems (TACAS'23'25)
  • International Symposium on Formal Methods (FM'23)
  • International Conference ON Cyber-Physical Systems (ICCPS'23)
  • Verified Software: Theories, Tools, Experiments (VSTTE'23)
  • NASA Formal Methods (NFM'23)
  • International Symposium on Distributed Computing (DISC'22)
  • Computer Security Foundations Symposium (CSF'22)
  • International Symposium on Automated Technology for Verification and Analysis (ATVA'21)
Conference Artifact Review
  • International Conference on Computer Aided Verification (CAV'23'24)
Journal Review
  • Acta Informatica (ACTA'22'25)
Conference Student Volunteer
  • International Conference on Computer-Aided Verification (CAV'21)

Research Mentoring and Teaching Experience

Grduate Student Mentees
Michigan State University
  • Ali Eshtehardian (PhD, 2022-present)
  • Caitlin Coggins (Master, 2022 Summer)
Undergrduate Student Mentees
Michigan State University
  • Peyton Ross (2022-present)
  • Tess Murphy (2022-present)
  • Lilly Yanke (2022-present)
  • Nika Ghasemi Barmi (2022-present)
Courses Teaching Assistant
Michigan State University
  • Discrete Structures in Computer Science (CSE 260), Spring'21
Iowa State University
  • Introduction to Object-Oriented Programming (COM S 227), Spring'18, Fall'18

References

Dr. Borzoo Bonakdarpour, Ph.D Advisor, MSU
Associate Professor at Department of Computer Science and Engineering, Michigan State University

borzoo@msu.edu


Dr. César Sánchez, Research Collaborator, IMDEA
Associate Research Professor at IMDEA Software Institue of Spain, dual Appointment with Scientific Researcher at the Spanish National Research Council (CSIC)

cesar.sanchez@imdea.org


Industrial Experience

Research Intern @ Microsoft
MSR, Summer 2023
  • Developed a framework to prove smart-contract safety.
  • Applied on UniSwap v2 decentralized exchange protocol.
  • Preprint available on [arXiV].
Applied Scientists Intern @ Amazon
Amazon Development Center US Inc., Summer 2022
  • Developed symbolic model checking (SMC) technique with multi-threaded parallization.
  • Improved SMC efficiency with AWS cloud services EC2.
  • Performed SMC with multiple industrial-level protocols.
Software Engineer Intern @ Worrell
Worrell Medical Design Inc., Summer 2018
  • Developed a Virtual Reality Environment on Oculus Quest for Human Factor Engineering usability testing.
  • Programed well-functioning C# scripts in Unity3D engine with desired behaviors and outcomes.
  • Analyzed user feedback and debug/adjust/improve the existing versions of the program with HF engineers.
Honors&Awards

highlights of me

Fellowships
  • Nominated as Google Fellowship Applicant, one of the only 4 Ph.D. students selected by the Graduate College of MSU (2021)
  • University Graduate Research Fellowship, full Summer support, Michigan State University. (2020)
Honors
  • Nominated as Outstanding Seniors (2020)
  • Graduate with MAGNA CUM LAUDE, with double-degree GPA: 3.86 (2020)
  • ISU College of Liberal Arts and Sciences Dean’s List (2013-2020)
Scholarships
  • ISU International Student Ambassador Gold Level Scholarship Recipient (2013-2018)
  • ISU Music Department Outstanding Student Scholarship Recipient (2013-2018)
  • ISU Student Representative Council, Department Representative elected (2015)
Music Awards
  • 1st Prize Winner, Fort Dodge Orchestra Young Artists Concerto Competition (2015)
  • 1st Prize Winner, Iowa State University Symphony Orchestra Concerto Competition (2014)
    (Performed Tchaikovsky Piano Concerto No.1 at Winner's Concert)
  • State Winner, Music Teacher National Association (MTNA) Piano Competition (2014)
Other Volunteer Experience
  • Iowa Education without Borders (non-profit) Volunteer/Event Coordinator (2017-18)
  • Iowa Youth Leadership Summer Camp Student Volunteer (2017-18)
  • Iowa State University Annual K-12 Computational Thinking Competition (2018)
As a Musician

My Piano Recordings

"Music gives a soul to the universe, wings to the mind, flight to the imagination and life to everything." – Plato
Contact Me

Get in Touch!

Tzu-Han Hsu (she/her/hers)

Postdoctoral Research Fellow, Harvard University
School of Engineering and Applied Sciences
Email: tzuhan@seas.harvard.edu
Phone: +1 (515)441-6303
Website: https://tzuhancs.github.io/

I am a proud member of the Trustworthy and Reliable Technologies Lab (TART) @MSU!

Thank you for visiting my website!