| CARVIEW |
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:
- PL Research for Hackers (an introductory talk on PL research)
- How to give talks that people can follow by Derek Dreyer
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
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.
Powered by Flask & nginx & gunicorn & pandoc & a trick to improve one’s webpage
Last updated: 2024.12.13