Interval Analysis and Methods in Software Analysis

Abstract

This thesis investigates the application of interval analysis and methods within the domain of software verification, with a particular focus on mitigating the state space explosion problem. State space explosion poses a significant challenge to static and dynamic software verification techniques, such as fuzzing, bounded model checking (BMC), and abstract interpretation. These methods, despite their robustness, struggle to scale when faced with complex programs that generate a vast number of execution paths and states. To address this, the thesis introduces the use of contractors—interval methods that refine the search space by eliminating non-solution regions—across several verification frameworks. By applying interval contractors in fuzzing, BMC, and abstract interpretation, the search space is systematically reduced without compromising the soundness or completeness of the verification process. Contractors are employed to navigate guard conditions, narrow down variable domains, and simplify control structures, leading to a more efficient exploration of execution paths. The thesis presents a detailed implementation of these methods and evaluates their performance through rigorous benchmarking. Results demonstrate that the integration of contractors significantly enhances verification efficiency, reducing both computational resource consumption and time while preserving accuracy in identifying potential software vulnerabilities. This research offers a novel contribution to improving the scalability of software verification methods, making them more practical for real-world applications.