Skip to main content

Tzu-Han Hsu

Tzu-Han Hsu
Ph.D. student
Biography:

I'm a Ph.D. student at Michigan State University Computer Science & Engineering Department. My research interests are: Formal Methods for Verification, Model Checking, Synthesis of Hyperproperties, Security and Privacy.

I am interested in applications of formal methods in computer security for ensuring 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 also learned piano and violin for 15+ years. I performed Tchaikovsky Piano Concerto No.1 with Iowa State University (ISU) Symphony Orchestra in 2015, held a Solo Piano Recital in 2017, and was the Assistant Principal violinist for ISU Symphony Orchestra.

tzuhan@msu.edu

Publications

2023

Tzu-Han Hsu, Cesar Sanchez, Sarai Sheinvald, Borzoo Bonakdarpour, "Efficient Loop Conditions for Bounded Model Checking Hyperproperties" International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), , 2023.   tacas23-2.pdf (837.58 KB)   
Tzu-Han Hsu, Borzoo Bonakdarpour, Bernd Finkbeiner, Cesar Sanchez, "Bounded Model Checking for Asynchronous Hyperproperties" International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), , 2023.   tacas23-1.pdf (684.71 KB)   

2022

Tzu-Han Hsu, Borzoo Bonakdarpour, Eunsuk Kang, Stavros Tripakis, "Mapping Synthesis for Hyperproperties" The 35th IEEE International Symposium on Computer Security Foundations (CSF), IEEE, 2022.   main.pdf (466 KB)   

2021

Tzu-Han Hsu, Cesar Sanchez, Borzoo Bonakdarpour, "Bounded Model Checking for Hyperproperties" The 27th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), Springer, 2021.   tacas21.pdf (579.32 KB)