• 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

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
Papers
Piano repertoire
Good Movies
My Publications

Conference Papers

  1. 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. [arXiv]

  2. 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. [arXiv]

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

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

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

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

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


Industiral 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!