Yes, we did not modify the instrumentation. We only changed the search strategy. We did some simplifications to the code when presenting it in the paper, but did not change the order. Does the order look weird to you?

Thank you, Frank! Sorry for the super long delay for the reply—I did not check Bluesky frequently. The KLEE-SA sources are actually decent :). We quickly understood the implementation and found where we should modify for improvement. Thank you very much for your great work and artefect.

The FUZZING workshop paper revisits combining static analysis and symbolic execution for precise bug finding. We show that accurate error traces from static analysis can actually help symbolic execution, but inaccurate traces can mislead symbolic execution and potentially human users.

The SIGMOD work is a collaboration with @mrigger.bsky.social, Wenjing Deng, and Qiuyang Mang. We propose a geometry-aware test generator for spatial databases and prove metamorphic relations under affine transformations. We uncovered 34 previously unknown bugs in mainstream spatial databases.

I will be working on trustworthy automated reasoning and its applications to software reliability.

Feel free to reach out if you are interested in PhD opportunities, visiting, or collaboration.