Qiyuan Zhao (赵启元)

Ph.D. student at VERSE lab, School of Computing, National University of Singapore

I have worked in the general field of programming languages, formal methods and software engineering. That said, I decide to focus my research in my Ph.D. on programming language theory, and formal verification (using automated/interactive theorem provers).

- email:
- apply base64 decoder three times on this:
`Wlc1R05VMVVRWGhQUlVKdllqTlNkRmxYYkhOTWJVNTJZbEU5UFE9PQ==`

- hint: apply
`(lambda f: lambda x: f (f (f (x))))(base64.b64decode)`

on the encoding above in Python3 ## Why three?

Because a capable machine like ChatGPT can quickly resolve an once or twice encoded text.

- hint: apply
- alternatively, find my email from this paper

- apply base64 decoder three times on this:
- github: github.com/zqy1018
- Google Scholar page: Qiyuan Zhao - Google Scholar
- CV: a version updated in May 2024 can be found here.

Time format: YYYY.MM.DD

- 2024.04.01: Our paper on mechanized verification of tensor-manipulating programs using hyperlogic has been accepted to PLDI’24. Details will be added later.
- 2024.01.21: Came back from POPL’24.
- 2023.12.14: Our CPP’24 paper got a Distinguished Paper Award!
- 2023.11.21: I am greatly honored to have my first formal verification paper accepted to CPP’24 (co-located with POPL’24). Details will be added later.
- 2023.07.29: Our paper
*CAmpactor: A Novel and Effective Local Search Algorithm for Optimizing Pairwise Covering Arrays*got accepted (without major revision!) to ESEC/FSE’23. - 2023.01.04: Arrived at Singapore.
- 2022.11.11: After aborting my old blog site for more than three years, it is time to establish a new one.

For the full list of my publications, please refer to my Google scholar page or my CV.

(PLDI’24) Mechanised Hypersafety Proofs about Structured Data [ Preprint ][ Extended version ][ Github repo ]

Vladimir Gladshtein, Qiyuan Zhao, Willow Ahrens, Saman Amarasinghe, Ilya Sergey

- Topics: mechanized verification of tensor-manipulating programs using hyperlogic
## Simple introduction:

We design and formalize (in Coq) a hyper separation logic, which is useful for verifying programs manipulating structured data (*e.g.,*tensors). We demonstrate the power of this program logic and the methodology of using such hyperlogic (rather than using a "unary" program logic) by verifying a diverse set of benchmark programs with relatively low efforts.

(CPP’24) Rooting for Efficiency: Mechanised Reasoning about Array-Based Trees in Separation Logic [ Preprint ][ Github repo ][ Slides ][ Presentation video ]

Qiyuan Zhao, George Pîrlea, Zhendong Ang, Umang Mathur, Ilya Sergey

**Distinguished Paper Award**- Topics: formal verification of array-based trees
- Artifact status: available (there was no artifact evaluation in CPP’24)
## Simple introduction:

We propose some useful techniques to reason about some common programming patterns appearing in the programs that operate with*array-based trees*(*i.e.*, trees implemented using one or more arrays). There are two by-products: one is a small library about generic trees in Coq (see the Github repo above), the other is the verification of*tree clock*, a state-of-the-art logical clock instance.

(ESEC/FSE’23)

*CAmpactor*: A Novel and Effective Local Search Algorithm for Optimizing Pairwise Covering Arrays [ Preprint ][ Github repo ][ Slides ][ Presentation video ]Qiyuan Zhao, Chuan Luo, Shaowei Cai, Wei Wu, Jinkun Lin, Hongyu Zhang, Chunming Hu

- Topics: pairwise testing
- Artifact status: available & reusable
## Simple introduction:

We build a tool*CAmpactor*to effectively (while moderately efficiently) reduce the size of PCA, even for PCAs of large benchmarks. For a simple introduction to PCA, please refer to the simple introduction below.

(ESEC/FSE’22)

*SamplingCA*: Effective and Efficient Sampling-Based Pairwise Testing for Highly Configurable Software Systems [ Preprint ][ Github repo ][ Presentation video ]Chuan Luo, Qiyuan Zhao, Shaowei Cai, Hongyu Zhang, Chunming Hu

- Topics: pairwise testing
- Artifact status: available & reusable
## Simple introduction:

Pairwise covering arrays (PCAs) are a class of important test suites in the context of pairwise testing, where pairwise testing is a practical variant of combinatorial (interaction) testing. We build a tool*SamplingCA*to generate (moderately small) PCAs quickly, even for large benchmarks.

**Note**: I decide to update this section periodically,
probably every 1-2 weeks? Or every 1-2 months? I don’t know; it just
depends.

Great talks:

Useful resources (can be publicly found on the Internet):

The (soft) things-one-should-know-before-or-during-one’s-PhD series:

- PhD, Research, and Programming Languages by Gabriel Scherer
- How to Give an Academic Talk by Paul N. Edwards

Powered by Flask & nginx & gunicorn & pandoc

Last updated: 2024.05.16