Scalable Relational Analysis via Relational Bound Propagation.
Saved in:
| Title: | Scalable Relational Analysis via Relational Bound Propagation. |
|---|---|
| Authors: | Stevens, Clay1 cdsteven@iastate.edu, Bagheri, Hamid2 bagheri@unl.edu |
| Source: | ICSE: International Conference on Software Engineering. 2024, p1-12. 12p. |
| Subjects: | Software engineers, Computer programmers, Robust statistics, Semantics, Information theory |
| Abstract: | 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). [ABSTRACT FROM AUTHOR] |
| Copyright of ICSE: International Conference on Software Engineering is the property of Association for Computing Machinery and its content may not be copied or emailed to multiple sites without the copyright holder's express written permission. Additionally, content may not be used with any artificial intelligence tools or machine learning technologies. However, users may print, download, or email articles for individual use. This abstract may be abridged. No warranty is given about the accuracy of the copy. Users should refer to the original published version of the material for the full abstract. (Copyright applies to all Abstracts.) | |
| Database: | Engineering Source |
|
Full text is not displayed to guests.
Login for full access.
|
|
| Abstract: | 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). [ABSTRACT FROM AUTHOR] |
|---|---|
| DOI: | 10.1145/3597503.3639171 |
