Abstract
Java Ranger is a path-merging tool for Java Programs. It identifies branching regions of code and summarizes them by generating a disjunctive logical constraint that describes the behavior of the code region. Previously, Java Ranger showed that a reduction of 70% of execution paths is possible when used to merge branching regions of code that support numeric constraints. In this paper, we describe the support of two additional features since participation in SV-COMP 2020: symbolic array and symbolic string operations. Finally, we present a preliminary evaluation of the effect of the structure of the disjunctive constraint on the solver’s performance. Results suggest that certain constraint structures can speed up the performance of Java Ranger.
Original language | English (US) |
---|---|
Title of host publication | Tools and Algorithms for the Construction and Analysis of Systems - 29th International Conference, TACAS 2023, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2022, Proceedings |
Editors | Sriram Sankaranarayanan, Natasha Sharygina |
Publisher | Springer Science and Business Media Deutschland GmbH |
Pages | 553-558 |
Number of pages | 6 |
ISBN (Print) | 9783031308192 |
DOIs | |
State | Published - 2023 |
Event | 29th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2023, held as part of the 26th European Joint Conferences on Theory and Practice of Software, ETAPS 2023 - Paris, France Duration: Apr 22 2023 → Apr 27 2023 |
Publication series
Name | Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) |
---|---|
Volume | 13994 LNCS |
ISSN (Print) | 0302-9743 |
ISSN (Electronic) | 1611-3349 |
Conference
Conference | 29th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2023, held as part of the 26th European Joint Conferences on Theory and Practice of Software, ETAPS 2023 |
---|---|
Country/Territory | France |
City | Paris |
Period | 4/22/23 → 4/27/23 |
Bibliographical note
Funding Information:★The research described in this paper has been supported in part by the National Science Foundation under grant 1563920, and Google Summer of Code. ★★ Jury member ★★★Lecturer on a Leave of Absence Ain Shams University, Cairo, Egypt [email protected]
Publisher Copyright:
© 2023, The Author(s).