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).
- 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.
- alternatively, find my email from this paper
- github: github.com/zqy1018
- Google Scholar page: Qiyuan
Zhao - Google Scholar
- CV: a version updated in Apr 2024 can be found here.
News
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.
Selected Publications
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 ][ 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 ]
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 ]
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.
Projects
Coming soon …
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:
Powered by Flask & nginx & gunicorn & pandoc
Last updated: 2024.04.10