• Hello!
    I'm Tzu-Han
    Download CV

  • I am a CSE Ph.D. student at
    Michigan State University

  • I am also a pianist
    and violinist
    My Recordings
keep going

Recent News

Feb. 2, 2022 | Internship

Very excited to share that I will join Amazon ARG team as an applied scientist intern to work on symbolic model checking for P system, and will be spending this Summer in beautiful Seattle!

Dec. 11, 2021 | Talk

I gave a collaborative talk with my advisor prof. Borzoo Bonakdarpour at RWTH Aachen University, Germany!
(Thank prof. Joost-Pieter Katoen and prof. Erika Abraham for the invitation.)

Sep. 24, 2021 | Honor

I am nominated as one of the only 4 PhD students by MSU for Google PhD Fellowship!

Sep. 22, 2021 | Milestone

I successfully passed my qualifying exam!

July 16, 2021 | Paper

Our paper "Mapping Synthesis for Hyperproperties" with Borzoo Bonakdarpour, Eunsuk Kang, and Stavros Tripakis, is accepted to CSF 2022!

June 23, 2021 | Service >>> 2021 CAV Conference Page

I will join CAV 2021 as a student volunteer this year!

May 7, 2021 | Honor

I received full Summer graduate fellowship from MSU!

March 29, 2021 | Talk >>> Link to the TACAS'21 BMC talk recording

I gave my first conference talk at TACAS 2021!

March 13, 2021 | Milestone

I received the very first paper citation on my Google Scholar Page!

December 23, 2020 | Paper

My first paper "Bounded Model Checking for Hyperproperties" with prof. César Sánchez and prof. Borzoo Bonakdarpour, is accepted to TACAS 2021!

May 5, 2020 | Honor

I graduated from ISU with double degrees, COM S and MUSIC, in Summa Cum Laude!

April 21, 2020 | Honor

I reveiced the Nomination of Outstanding Senior by the department of music!

About Me

Tzu-Han Hsu

Hi I'm Tzu-Han, from Taiwan!

Computer Science Engineering Ph.D. student at Michigan State University.
My Advisor is Dr. Borzoo Bonakdarpour.
I am also a pianist, violinist, and romanticist.

My research interests are:
  • Formal Methods
  • Model Checking
  • Synthesis of Hyperproperties
  • Security and Privacy
  • Information-Flow Security

I am highly interested in applications of formal methods in computer security in order to ensure soundness of computer programs, including designing efficient verification algorithms. Given the importance of trustworthiness and security in cyberspace, this is an extremely important area of research with many practical applications.

Besides research, I have learned piano and violin for 18+ years. I performed Tchaikovsky Piano Concerto No.1 with ISU Symphony Orchestra in 2015, held a Solo Piano Recital in 2017, and I was the Assistant Principal violinist for ISU Symphony Orchestra. In the past, I have worked as a Software Engineer Intern, Virtual Reality Application Developer, Website Developer, Teaching Assistant, accompanist, and piano instructor.

Cups of coffee
Piano repertoire
Good Movies
My Publications

Conference Papers

  • Tzu-Han Hsu, Borzoo Bonakdarpour, Eunsuk Kang, and Stavros Tripakis
    "Mapping Synthesis for Hyperproperties" (2022)
    In IEEE International Symposium on Computer Security Foundations (CSF'22). To appear. [pdf]

  • Tzu-Han Hsu, César Sánchez, and Borzoo Bonakdarpour
    "Bounded Model Checking for Hyperproperties" (2021)
    In International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'21), Luxembourg, Luxembourg. To appear. [pdf] [arXiv]


  • Tzu-Han Hsu, Borzoo Bonakdarpour, and César Sánchez
    HyperQube: A QBF-Based Bounded Model Checker for Hyperproperties” (2021)

  • Tzu-Han Hsu, Yu Wang, Borzoo Bonakdarpour, and Miroslav Pajic
    Multi-Agent Path Planning with Hyperproperties” (2020)

My ackground

Education, Research, Teaching


3rd Year Ph.D. Student in Computer Science Engineering
      Advisor: Dr. Borzoo Bonakdarpour
      Michigan State University, 2020-Present (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

Graduate Research Assistant
Michigan State University, 2020-Present
  • 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

Conference Paper Review
  • 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)
Journal Review
  • Acta Informatica (ACTA'22)
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


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


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)


Industiral Experience

Applied Scientists Intern @ Amazon
Amazon Development Center US Inc., Summer 2022
  • Developed symbolic model checking (SMC) technique with pmulti-threaded parallization.
  • Improved SMC efficiency with AWS cloud services.
  • Performed SMC with multiple real-world protocols from the industry.
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.

highlights of me

  • 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)
  • 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)
  • 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)

Ph.D. Student, Michigan State University
Dept. of Computer Science Engineering
Email: tzuhan@msu.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!