10 Aug 2023 — NUS Presidential Young Professor Kuldeep S. Meel and PhD student Jiong Yang won the Distinguished Paper Award at the 35th International Conference on Computer-Aided Verification (CAV 2023).
CAV 2023 is a conference dedicated to the advancement of the theory and practice of computer-aided formal analysis methods for hardware and software systems. It was held from 17 to 22 July 2023 in Paris, France.
Their winning paper, “Rounding Meets Approximate Model Counting,” focuses on the problem of model counting. Model counting refers to counting the number of ways (solutions) that a given formula can be satisfied. This can be a really hard and slow process. We may have some success with existing hashing-based approaches but in scenarios that require estimates with high confidence, the model counting’s scalability becomes severely impacted.
The researchers propose a novel technique, “rounding” which rounds the model count estimate to a value with higher confidence. The resulting approach achieved a significant theoretical reduction in runtime and was in fact, four times faster than the state-of-the-art approximate model counting algorithm.
Model counting is a fundamental problem in Computer Science that is present in a wide range of applications such as control improvisation, network reliability, and neural network verification. By introducing this new technique, “rounding” can effectively address the scalability issue and drive the advancement of downstream applications that are built on top of model counting problems (smarter programs, more reliable networks, and accurate calculations).
The pair were pleasantly surprised and grateful to the community for their win.
“I think our approach stood out for its practical simplicity. A single-line change is all we needed and theoretical rigour (more than 15 pages of proof to accompany the change),” commented Yang.
Meel added: “At the early stages of the project, we were able to achieve considerable speedup in some but not all cases, and I thought it was good enough, but Jiong strongly believed in the power of “rounding” and targeted universal speedup.”
Besides the Distinguished Paper Award, the researchers also walked away with a cash prize of $500 euros.
