HYBRID TEMPLATE ANALYSING FOR AN EFFICIENT AND PRECISE POLYHEDRAL ANALYSIS

Abstract

This paper proposes a new static analysis technique that combines two complemen- tary approaches: Principal Component Analysis (PCA)-guided template generation and dynamic threshold-based Smart Widening. Building on recent advances in weakly-relational polyhedral analysis and efficient convergence strategies, we introduce a hybrid method that achieves a better trade-off between precision and performance. Our technique leverages PCA to identify the most relevant invariant directions and dynamically adapts widening thresholds based on intermediate abstract states. Empirical evaluation demonstrates significant improvements over existing techniques in both accuracy and scalability.

The specified framework is not only more efficient regarding computing but also adds another layer of automation to the process of finding invariants. The method does not use manually defined thresholds to guarantee adaptative behavior regardless of the program structure and numerical complexity. Moreover, the direction choice of the PCA will give a better understanding of the relationship between the variables of the program, and allow making more significant abstractions, and fewer false alarm on the way to verification. This flexibility causes the approach to be ideal in studying real-time systems of control, reactive programs and embedded applications. In general, the hybrid PCA-smart widening framework is a data-based improvement of the traditional data non-dynamic techniques of analysis.