(she/her/hers)
The University of Texas at Austin
Automated Reasoning, Formal Methods, Software Engineering, Artificial Intelligent learning, Neural Networks
Wenxi Wang is a fifth-year Ph.D. student at the Electrical and Computer Engineering (ECE) Department, The University of Texas at Austin, supervised by Prof. Sarfraz Khurshid. Her interests mainly focus on SAT/SMT solving, Model Counting, Software Testing, Programming Languages, and Machine Learning. She works on improving software verification from front-end to back-end. For the front end, she works on improving the analysis efficiency of a software modeling tool called Alloy. For the back end, she works on improving SAT/SMT solving and propositional model counting for problems translated from the front end.
Improving Propositional Model Counting for Alloy
Propositional model counting is the classic problem of counting the number of all solutions for the given formula in propositional logic. The modern model counters have seen significant advances in recent years, which have fueled various applications in software verification and reliability domains, such as probabilistic analysis, automated program repair, side-channel analysis, and quantitative verification of neural networks. Users routinely employ tools that translate domain-specific problems to propositional formulas and count their solutions using off-the-shelf model counters. Alloy is a mature software modeling tool for writing and analyzing specifications of software systems. The Alloy toolset automatically translates the Alloy specifications into propositional formulas. Despite the remarkable success of modern propositional model counters, performing model counting on Alloy specifications remains challenging due to scalability and robustness issues.
To improve the scalability of model counting, we first studied the impact of symmetry breaking on model counting. Symmetry breaking is a widely used approach in facilitating constraint solving but has never been considered in model counting. The study found that counting under domain-level symmetry breaking provided by Alloy is much faster than counting under no symmetry breaking, which shows a promising direction to improve the model counting efficiency. Inspired by the finding, a multi-functional model counting approach called SymMC is proposed for Alloy specifications, utilizing symmetry information extracted during the Alloy translation. Given an Alloy specification, SymMC can automatically 1) enumerate/count its non-isomorphic models, 2) count its isomorphic models, and 3) evaluate the symmetry breaking ability of Alloy. Our experimental results show that SymMC significantly outperforms state-of-the-art propositional model counters, not only in functionality but also in counting efficiency. To improve the robustness of model counters, we tested four state-of-the-art model counters using differential and metamorphic testing. We found various bugs in all four subject counters, including crashes, segmentation faults, incorrect model counts, and resource exhaustion.