Ph.D. Dissertation Defense: Clay Stevens
Monday, May 1, 2023
11:30 AM
Zoom: https://unl.zoom.us/j/95165152322
"Improving Scalability for Formal Analysis through Automated Tightening of Analysis Bounds"
Formal analysis is an invaluable tool for software engineers, yet state-of-the-art formal analysis techniques suffer from well-known limitations in terms of scalability. Modern, real-world software systems are often too large or change too frequently to justify the cost of a full formal analysis, leading software designers and engineers to abandon formal techniques and thus forego the insights such tools can provide. This dissertation presents three novel approaches to improving the scalability of bounded model checking, a formal technique frequently used to analyze software designs and systems. First, I describe a method of analyzing evolving software systems which can automatically determine domain-specific optimizations that can dramatically reduce the cost of repeated analysis. This approach, implemented in a tool called SoRBoT, combines solution reuse and bound tightening---the two primary methods employed to analyze evolving systems in the state-of-the-art---while avoiding the main pitfalls of each. SoRBoT substantially exceeds the run-time performance of other state-of-the-art techniques while introducing only a negligible overhead. Second, I present another novel approach which targets the scalability of formal analysis when applied to software design tasks, many of which require systematic exploration of potentially huge model spaces. This approach, Parasol, uses unsupervised learning to automatically derive domain knowledge about the structure of the system specification, allowing for efficient synthesis of the model space in parallel. This significantly reduces synthesis time, making large-scale systematic model space exploration for real-world systems more tractable. The empirical results presented here corroborate that Parasol substantially reduces the time required for model space synthesis, compared to state-of-the-art model space synthesis techniques relying on both incremental and parallel constraint solving technologies as well as competing, non-learning-based partitioning methods. Lastly, I present relational bound propagation, a new, automated method of tightening the bounds for any relational bounded model checking problem. By applying the rules and algorithms presented in this dissertation, software engineers can develop analysis tools which can automatically optimize relational specifications, easing their use for others in our industry.
Committee:
Dr. Hamid Bagheri, Advisor
Dr. Witawas Srisa-An
Dr. ThanhVu Nguyen
Dr. Reina Hayaki