Main Page

Qiyuan Zhao (赵启元)

In case you are interested in how to pronounce my name …

“Qiyuan Zhao” is the Chinese Pinyin form of my name. In Pinyin, the “Qi” part pronounces like the “chi” part of “chip”; the “Zh” part pronounces like the “dr” part of “draw”; the “ao” part pronounces like the “ow” part of “now”.

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).

Personal Information

email address:
- find my email address directly from this paper (personal) or this paper (institutional)
github: github.com/zqy1018
Google Scholar page: Qiyuan Zhao - Google Scholar
CV (in PDF) (last updated in Dec 2024, last checked in Dec 2024)

News

Time format: YYYY.MM.DD

2024.08.15: Accepted to be a volunteer at SPLASH’24!
2024.07.05: Our paper on compositionally verifying safety and liveness of (potentially compositional) Byzantine protocols has been accepted to CCS’24.
2024.07.03: The paper describing the successor of SamplingCA and CAmpactor has been accepted to ISSTA’24.
2024.04.01: Our paper on mechanized verification of tensor-manipulating programs using hyperlogic has been accepted to PLDI’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).
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.

Selected Publications

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

2024

(CCS’24) Compositional Verification of Composite Byzantine Protocols

Qiyuan Zhao, George Pîrlea, Karolina Grzeszkiewicz, Seth Gilbert, Ilya Sergey

[ Preprint ] [ Artifact ] [ Github repo ] [ Slides ]

(The slides are scripted, since the presentation video seems not to be publicly available)
- Topics: Byzantine protocol correctness verification
- Artifact status: available & reusable & results reproduced
- Simple introduction:
  The conclusion section of the paper is already a good summary of this work.
(ISSTA’24) Beyond Pairwise Testing: Advancing 3-wise Combinatorial Interaction Testing for Highly Configurable Systems

Chuan Luo, Shuangyu Lyu, Qiyuan Zhao, Wei Wu, Hongyu Zhang, Chunming Hu

[ Preprint ] [ Artifact ] [ Github repo ]
- Topics: combinatorial testing with strength 3
- Artifact status: available & functional
- Simple introduction:
  We built a tool for generating relatively small 3-wise CAs from 2-wise CAs (i.e., PCAs). Those 2-wise CAs are typically generated by SamplingCA, thus resulting in a toolchain for 2 to 3-wise CA generation.
(PLDI’24) Mechanised Hypersafety Proofs about Structured Data

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

[ Preprint ] [ Extended version ] [ Artifact ] [ Github repo ] [ Presentation video ]
- Topics: mechanized verification of tensor-manipulating programs using hyperlogic
- Artifact status: available & reusable
- 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

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

[ Preprint ] [ Artifact ] [ Github repo ] [ Slides ] [ Presentation video ] 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.

2023

(ESEC/FSE’23) CAmpactor: A Novel and Effective Local Search Algorithm for Optimizing Pairwise Covering Arrays

Qiyuan Zhao, Chuan Luo, Shaowei Cai, Wei Wu, Jinkun Lin, Hongyu Zhang, Chunming Hu

[ Preprint ] [ Artifact ] [ Github repo ] [ Slides ] [ Presentation video ]
- 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.

2022

(ESEC/FSE’22) SamplingCA: Effective and Efficient Sampling-Based Pairwise Testing for Highly Configurable Software Systems

Chuan Luo, Qiyuan Zhao, Shaowei Cai, Hongyu Zhang, Chunming Hu

[ Preprint ] [ Artifact ] [ Github repo ] [ Presentation video ]
- 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.

Resources & Misc

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:

For fun:

A guide on how to order Kopi (coffee) in Singapore
A deprecated approach to find my email:

Apply base64 decoder three times on this: Wlc1R05VMVVRWGhQUlVKdllqTlNkRmxYYkhOTWJVNTJZbEU5UFE9PQ==.

I set the number to be three because, by the beginning of 2024, a capable machine like ChatGPT could quickly resolve text encoded once or twice, but not when encoded three times. However, as found in August 2024, ChatGPT could already generate a Python script capable of decoding text regardless of how many times it is encoded. Therefore, this trick to prevent email plaintext from appearing is no longer meaningful.

Last updated: 2024.12.13