Interval Analysis and Methods in Software Analysis
No Thumbnail Available
Date
2024
Authors
Journal Title
Journal ISSN
Volume Title
Publisher
Manchester University
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.
Description
Keywords
Interval Analysis, Software Verification, Contractors (Interval Methods), State Space Explosion, Bounded Model Checking (BMC), Abstract Interpretation, Fuzz Testing, Fuzzing, Constraint Satisfaction Problem (CSP), Static Analysis, Dynamic Analysis, Symbolic Execution, SMT Solvers, Verification Soundness, Verification Completeness, Control Flow Analysis, ESBMC, FuSeBMC, Incremental-BMC, Formal Methods in Software Engineering, Benchmarking in Software Verification, Interval Arithmetic, Software Vulnerability Detection, Program Analysis Scalability, Numerical Methods in Verification, Hybrid Verification Techniques, Automated Software Testing, CP-based Interval Contraction, Test Case Generation, Verification Toolchains, Formal Verification Efficiency