Presentation
Time:
Ph.D. Dissertation Defense: Jianghao Wang
Date:
10:00 am –
12:00 pm
Virtual Location:
Zoom
Target Audiences:
Ph.D. Dissertation Defense: Jianghao Wang
Friday, August 2, 2024
10:00 AM CST
Join Zoom: https://unl.zoom.us/j/6683430542
“Optimizing Scalability for Formal Analysis with Evolutionary Algorithm”
Predominantly employed to tackle hardware validation challenges in the early years, formal methods have since expanded to software engineering, introducing a significant level of rigor and precision to software analysis. Its use of mathematical notations and logical reasoning allows for abstract modeling of programs, enabling researchers and engineers to perform a multitude of analysis tasks to verify system dependability and rigorously prove the correctness of system properties. Despite the availability of many automated analysis tools including those considered lightweight, the practical adoption of formal methods in software development has been limited due to scalability concerns, especially when applied to large real-world applications. My prior research effort, EvoAlloy, explored the feasibility of substituting the computational heavy constraint-solving technique adopted by the popular bounded verification tool Alloy with an evolutionary algorithm. By loosening the completeness while preserving soundness, EvoAlloy has demonstrated the potential to enhance the scalability of Alloy Analyzer. Yet its coarse-grained fitness evaluation in Kodkod poses a major obstacle to generalizing this approach to more diverse and complex Alloy specifications. This dissertation presents two novel techniques for optimizing the genetic algorithm (GA) based search toward scalable Alloy formal analysis. First, I introduce an innovative constraint violation assessment scheme, which traverses the Abstract Syntax Tree (AST) of the relational formula and computes the degree of violation for each subformula. This comprehensive and granular evaluation facilitates solution exploration with refined differentiation capability, thereby electively generalizing my GA-based analysis to a wider array of problems. Second, I present an adaptive fitness function, implementing a dynamic weight adjustment mechanism that optimizes the allocation of computational resources. This approach contributes to effective instance space navigation and efficient convergence on valid solutions, thus greatly improving the run-time performance. Taking advantage of both techniques, I created an advanced GA-boosted Alloy Analysis, AdaptiveAlloy. The experimental results illustrate that Adaptive Alloy is capable of finding models of higher scope and achieving greater scalability and efficiency than both EvoAlloy and the state-of-the-art Alloy analyzer.
Committee:
Dr. Hamid Bagheri, Advisor
Dr. Rahul Purandare
Dr. Qiuming Yao
Dr. M.R. Hasan
Friday, August 2, 2024
10:00 AM CST
Join Zoom: https://unl.zoom.us/j/6683430542
“Optimizing Scalability for Formal Analysis with Evolutionary Algorithm”
Predominantly employed to tackle hardware validation challenges in the early years, formal methods have since expanded to software engineering, introducing a significant level of rigor and precision to software analysis. Its use of mathematical notations and logical reasoning allows for abstract modeling of programs, enabling researchers and engineers to perform a multitude of analysis tasks to verify system dependability and rigorously prove the correctness of system properties. Despite the availability of many automated analysis tools including those considered lightweight, the practical adoption of formal methods in software development has been limited due to scalability concerns, especially when applied to large real-world applications. My prior research effort, EvoAlloy, explored the feasibility of substituting the computational heavy constraint-solving technique adopted by the popular bounded verification tool Alloy with an evolutionary algorithm. By loosening the completeness while preserving soundness, EvoAlloy has demonstrated the potential to enhance the scalability of Alloy Analyzer. Yet its coarse-grained fitness evaluation in Kodkod poses a major obstacle to generalizing this approach to more diverse and complex Alloy specifications. This dissertation presents two novel techniques for optimizing the genetic algorithm (GA) based search toward scalable Alloy formal analysis. First, I introduce an innovative constraint violation assessment scheme, which traverses the Abstract Syntax Tree (AST) of the relational formula and computes the degree of violation for each subformula. This comprehensive and granular evaluation facilitates solution exploration with refined differentiation capability, thereby electively generalizing my GA-based analysis to a wider array of problems. Second, I present an adaptive fitness function, implementing a dynamic weight adjustment mechanism that optimizes the allocation of computational resources. This approach contributes to effective instance space navigation and efficient convergence on valid solutions, thus greatly improving the run-time performance. Taking advantage of both techniques, I created an advanced GA-boosted Alloy Analysis, AdaptiveAlloy. The experimental results illustrate that Adaptive Alloy is capable of finding models of higher scope and achieving greater scalability and efficiency than both EvoAlloy and the state-of-the-art Alloy analyzer.
Committee:
Dr. Hamid Bagheri, Advisor
Dr. Rahul Purandare
Dr. Qiuming Yao
Dr. M.R. Hasan
Download this event to my calendar
This event originated in School of Computing.