Improving Software Quality using Formal Reasoning

Abstract:

Formal reasoning establishes a rigorous foundation for ensuring the reliability and security of software systems. However, formal reasoning poses inherent high computational challenges. It typically employs two solving layers to address complex software systems: 1) modeling and translating software problems into logical formulas at the front-end, and 2) utilizing automated logical reasoning techniques to solve these formulas at the back-end. In this talk, aimed at improving the scalability of formal reasoning, I will present both machine learning and symbolic methods to enhance the efficiency of back-end automated logical reasoning. I will first discuss how graph neural networks can be used to facilitate SAT and MaxSAT solving, thus bridging the gap between deep learning and automated logical reasoning. I will then present a symbolic method known as symmetry breaking to enhance model counting, which bridges the gap between front-end modeling and back-end logical reasoning. Finally, I will discuss how the synergy of AI and human intelligence can be leveraged to pioneer the next generation of formal reasoning for a broad range of applications.

Bio:

Wenxi Wang is a Ph.D. candidate at the University of Texas at Austin. Her interests lie at the intersection of Software Engineering, Formal Methods, and Machine Learning, with an emphasis on developing methods and tools in formal reasoning to aid the construction of secure and reliable software systems. Results of her work have been published in top venues such as ICSE, ESEC/FSE, ASE, ICLR, PLDI, and TACAS. She is a recipient of the EECS Rising Stars and the UT Austin Engineering School Continuing Fellowship. She serves on the program committees of top conferences such as ASE, ICLR, NeurIPS, and ICML.