We look forward to seeing you in person in 3401 SC or online.
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 analysis layers to address complex software systems: 1) problem modeling layer, which models and translates software problems into logical formulas, and 2) logical reasoning layer, which utilizes automated logical reasoning techniques to solve these formulas. In this talk, aimed at improving the scalability and applicability of formal reasoning, I will present both machine learning and symbolic methods to enhance and bridge both the problem modeling layer and the logical reasoning layer. I will first discuss applying machine learning approaches to enhance both the analysis layers, by introducing how graph neural networks are used to facilitate SAT solving and MaxSAT encoding. I will then demonstrate how to utilize symbolic approaches to bridge the two analysis layers, by presenting how symmetry breaking is used to facilitate domain-specific propositional model counting and enumeration. Finally, I will discuss how the synergy of Artificial Intelligence 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.
