Y. Cyrus Liu

I’m a senior AI compiler research engineer at Samsung Semiconductor, AGI Computing Lab. My work primarily focus on translation validation, AI compiler correctness.

Research Interests

Formal Verification, Program Languages, Software Engineering, Systems and Security, Artificial Intelligence as well as theories and applications in practical problems.

Before Samsung

I was a postdoc fellow at Grinnell College, working with Peter-Michael Osera on program synthesis. I completed my PhD from Stevens, advised by Prof. Koskinen. I like mathematical modeling, which dissects practical problems using precise mathematical logics. The abstracted models can then subsequently be employed to address a wide spectrum of real-world challenges, they are great tools to enhance our ability to comprehend and interpret the reality through the lense of software systems.

On the personal side I enjoy sports (workout, running, hiking, swimming), dancing to the music, reading (my bookshelves), and traveling to interesting cities. Occasionally, I like writing blog.

projects

2023-2024 Foundations and Applications of Constraint-based Synthesis.
2021-2022 Dynamic Temporal Verification. DrNLA
2018-2021 Automatically Verifying Temporal Properties of Lifted Binaries. DarkSea
2014-2017 Mathematical Modeling and Information Security, archived.

teaching/mentoring

Fall 2024 PLMW@SPLASH, SIGPLAN-M on programming languages, academics and industry.
Summer 2024 CSC499 Temporal Verification, Grinnell College.
Spring 2024 CSC208 Discrete Structures, Grinnell College.

public talks

April 2023 Automatic Verification of Lifted Binaries, Empire Hacking, slides.
Nov. 2022 Seminar talk on DrNLA and cybersecurity, Seton Hall University.
Oct. 2022 Research work on DrNLA, NJPLS 2022, slides.
Dec. 2021 Successfully defend my dissertation proposal, slides.
Oct. 2021 Paper presentation on APLAS 2021 📽;
Oct. 2021 Student forum, poster presentation, FMCAD 2021, 📇, 📃.
July 2018 Participant talk on LTL, OPLSS 2018, slides.

community service

Paper Reviews: APLAS 2022.
Artifact Evaluation Committee: SLE 2025, OOPSLA 2025, POPL 2025, PLDI 2024, CAV 2023, CAV 2022, TAP 2021, CGO 2021.
Volunteers: PLDI 2018.

selected publications

VESC: Towards Temporal Verification of Smart Contracts

Samuel Larsen, Kevin Johanson, and Yuandong Cyrus Liu

In Companion Proceedings of the 2024 ACM SIGPLAN International Conference on Systems, Programming, Languages, and Applications: Software for Humanity, 2024

Bib PDF Poster

@inproceedings{larsen2024vesc,
  title = {VESC: Towards Temporal Verification of Smart Contracts},
  author = {Larsen, Samuel and Johanson, Kevin and Liu, Yuandong Cyrus},
  booktitle = {Companion Proceedings of the 2024 ACM SIGPLAN International Conference on Systems, Programming, Languages, and Applications: Software for Humanity},
  pages = {46--48},
  year = {2024}
}

DrNLA: Extending Verification to Non-linear Programs through Dual Re-writing

Yuandong Cyrus Liu, Ton-Chanh Le, Timos Antonopoulos, and 2 more authors

arXiv e-prints, 2023

Bib PDF

@article{cyrus2023drnla,
  title = {DrNLA: Extending Verification to Non-linear Programs through Dual Re-writing},
  author = {Liu, Yuandong Cyrus and Le, Ton-Chanh and Antonopoulos, Timos and Koskinen, Eric and Nguyen, ThanhVu},
  journal = {arXiv e-prints},
  pages = {arXiv--2306},
  year = {2023}
}

Proving LTL Properties of Bitvector Programs and Decompiled Binaries

Yuandong Cyrus Liu, Chengbin Pang, Daniel Dietsch, and 4 more authors

In Programming Languages and Systems: 19th Asian Symposium, APLAS 2021, Chicago, IL, USA, October 17–18, 2021, Proceedings 19, 2021

Bib PDF Video Slides

@inproceedings{liu2021proving,
  title = {Proving LTL Properties of Bitvector Programs and Decompiled Binaries},
  author = {Liu, Yuandong Cyrus and Pang, Chengbin and Dietsch, Daniel and Koskinen, Eric and Le, Ton-Chanh and Portokalidis, Georgios and Xu, Jun},
  booktitle = {Programming Languages and Systems: 19th Asian Symposium, APLAS 2021, Chicago, IL, USA, October 17--18, 2021, Proceedings 19},
  pages = {285--304},
  year = {2021},
  organization = {Springer International Publishing}
}