• 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
About Me

Tzu-Han Hsu

Hi I'm Tzu-Han, from Taiwan! I am a computer Science Ph.D. student at Michigan State University, advised by Dr. Borzoo Bonakdarpour. 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.

keep going

Recent News

July 2025 | Journal paper

Our journal paper "Gray-box Runtime Enforcement of Hyperproperties" is accepted to Acta Informatica!

April 2025 | Milestone

I successfully passed the comprehensive exam and officially became a Ph.D. candidate!

May 2024 | Paper

Our paper "Syntax-Guided Automated Program Repair for Hyperproperties" is accepted to CAV'24!

May 2023 | Paper

I will join Microsoft Research (MSR) as a research intern this Summer!

Dec. 2022 | Paper

Our two papers "Bounded Model Checking for Asynchronous Hyperproperties" and "Efficient Loop Conditions for Bounded Model Checking Hyperproperties" are both accepted to TACAS'23!

Aug. 2022 | Talk

I gave my first in-person conference talk at FLoC'22!

Feb. 2021 | Talk

I am invited to give a talk @UCSC!

Feb. 2, 2022 | Internship

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!

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" is accepted to CSF'22 (FLoC'22)!

June 23, 2021 | Service

I will join CAV21 as a student volunteer this year!

May 7, 2021 | Honor

I received full Summer graduate fellowship from MSU!

March 29, 2021 | Talk

I gave my first conference talk at TACAS'21 !

March 13, 2021 | Milestone

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

Dec. 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!

Cups of coffee
Papers
Piano repertoire
Good Movies
My Publications

Conference Papers

  1. Raven Beutner, Tzu-Han Hsu, Borzoo Bonakdarpour, and Bernd Finkbeiner
    "Syntax-Guided Automated Program Repair For Hyperproperties" (2024)
     International Conference on Computer Aided Verification (CAV'24), Montreal, Canada. [pdf] [springer]

  2. Tzu-Han Hsu, César Sánchez, Sarai Sheinvald, Borzoo Bonakdarpour
    "Efficient Loop Conditions for Bounded Model Checking Hyperproperties" (2023)
     In International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'23), Paris, France. To appear. [pdf] [springer]

  3. Tzu-Han Hsu, Borzoo Bonakdarpour, Bernd Finkbeiner, César Sánchez
    "Bounded Model Checking for Asynchronous Hyperproperties" (2023)
     In International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'23), Paris, France. To appear. [pdf] [springer]

  4. 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]

  5. 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] [springer]

Journal Papers

  1. Tzu-Han Hsu, Ana Oliveira da Costa, Andrew Wintenberg, Ezio Bartocci, and Borzoo Bonakdarpour
    "Gray-box Runtime Enforcement of Hyperproperties" (2025)
     Acta Informatica, To appear. [pdf]

Preprints

  • Tzu-Han Hsu, Borzoo Bonakdarpour, and César Sánchez
    "HyperQB: A QBF-Based Bounded Model Checker for Hyperproperties" (2021)     [arXiv]

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


My ackground

Education, Research, Teaching

Education

5th 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

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

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)

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!