Scalable Relational Analysis via Relational Bound Propagation

Bounded formal analysis techniques (such as bounded model checking) are incredibly powerful tools for today's software engineers. However, such techniques often suffer from scalability challenges when applied to large-scale, real-world systems. It can be very difficult to ensure the bounds are set properly, which can have a profound impact on the performance and scalability of any bounded formal analysis. In this paper, we propose a novel approach---relational bound propagation---which leverages the semantics of the underlying relational logic formula encoded by the specification to automatically tighten the bounds for any relational specification. Our approach applies two sets of semantic rules to propagate the bounds on the relations via the abstract syntax tree of the formula, first upward to higher-level expressions on those relations then downward from those higher-level expressions to the relations. Thus, relational bound propagation can reduce the number of variables examined by the analysis and decrease the cost of performing the analysis. This paper presents formal definitions of these rules, all of which have been rigorously proven. We realize our approach in an accompanying tool, Propter, and present experimental results using Propter that test the efficacy of relational bound propagation to decrease the cost of relational bounded model checking. Our results demonstrate that relational bound propagation reduces the number of primary variables in 63.58% of tested specifications by an average of 30.68% (N=519) and decreases the analysis time for the subject specifications by an average of 49.30%. For large-scale, real-world specifications, Propter was able to reduce total analysis time by an average of 68.14% (N=25) while introducing comparatively little overhead (6.14% baseline analysis time).