Java Ranger at SV-COMP 2020 (Competition Contribution)

Vaibhav Sharma; Soha Hussein; Michael W. Whalen; Stephen McCamant; Willem Visser

doi:10.1007/978-3-030-45237-7_27

Java Ranger at SV-COMP 2020 (Competition Contribution)

Vaibhav Sharma, Soha Hussein, Michael W. Whalen, Stephen McCamant, Willem Visser

Computer Science and Engineering

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

8 Scopus citations

Abstract

Path-merging is a known technique for accelerating symbolic execution. One technique, named “veritesting” by Avgerinos et al. uses summaries of bounded control-flow regions and has been shown to accelerate symbolic execution of binary code. But, when applied to symbolic execution of Java code, veritesting needs to be extended to summarize dynamically dispatched methods and exceptional control-flow. Such an extension of veritesting has been implemented in Java Ranger by implementing as an extension of Symbolic PathFinder, a symbolic executor for Java bytecode. In this paper, we briefly describe the architecture of Java Ranger and describe its setup for SV-COMP 2020.

Original language	English (US)
Title of host publication	Tools and Algorithms for the Construction and Analysis of Systems- 26th International Conference, TACAS 2020, held as part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2020, Proceedings, Part II
Editors	Armin Biere, David Parker
Publisher	Springer
Pages	393-397
Number of pages	5
ISBN (Print)	9783030452360
DOIs	https://doi.org/10.1007/978-3-030-45237-7_27
State	Published - 2020
Event	26th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2020, held as part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2020 - Dublin, Ireland Duration: Apr 25 2020 → Apr 30 2020

Publication series

Name	Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume	12079 LNCS
ISSN (Print)	0302-9743
ISSN (Electronic)	1611-3349

Conference

Conference	26th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2020, held as part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2020
Country/Territory	Ireland
City	Dublin
Period	4/25/20 → 4/30/20

Bibliographical note

Publisher Copyright:
© 2020, The Author(s).

Access

10.1007/978-3-030-45237-7_27

OpenUrl availability

Full text

Cite this

Sharma, V., Hussein, S., Whalen, M. W., McCamant, S., & Visser, W. (2020). Java Ranger at SV-COMP 2020 (Competition Contribution). In A. Biere, & D. Parker (Eds.), Tools and Algorithms for the Construction and Analysis of Systems- 26th International Conference, TACAS 2020, held as part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2020, Proceedings, Part II (pp. 393-397). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 12079 LNCS). Springer. https://doi.org/10.1007/978-3-030-45237-7_27

Java Ranger at SV-COMP 2020 (Competition Contribution). / Sharma, Vaibhav; Hussein, Soha; Whalen, Michael W. et al.
Tools and Algorithms for the Construction and Analysis of Systems- 26th International Conference, TACAS 2020, held as part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2020, Proceedings, Part II. ed. / Armin Biere; David Parker. Springer, 2020. p. 393-397 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 12079 LNCS).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

Sharma, V, Hussein, S, Whalen, MW, McCamant, S & Visser, W 2020, Java Ranger at SV-COMP 2020 (Competition Contribution). in A Biere & D Parker (eds), Tools and Algorithms for the Construction and Analysis of Systems- 26th International Conference, TACAS 2020, held as part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2020, Proceedings, Part II. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 12079 LNCS, Springer, pp. 393-397, 26th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2020, held as part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2020, Dublin, Ireland, 4/25/20. https://doi.org/10.1007/978-3-030-45237-7_27

Sharma V, Hussein S, Whalen MW, McCamant S, Visser W. Java Ranger at SV-COMP 2020 (Competition Contribution). In Biere A, Parker D, editors, Tools and Algorithms for the Construction and Analysis of Systems- 26th International Conference, TACAS 2020, held as part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2020, Proceedings, Part II. Springer. 2020. p. 393-397. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). doi: 10.1007/978-3-030-45237-7_27

Sharma, Vaibhav ; Hussein, Soha ; Whalen, Michael W. et al. / Java Ranger at SV-COMP 2020 (Competition Contribution). Tools and Algorithms for the Construction and Analysis of Systems- 26th International Conference, TACAS 2020, held as part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2020, Proceedings, Part II. editor / Armin Biere ; David Parker. Springer, 2020. pp. 393-397 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).

@inproceedings{1b55b9d28a594d3c98282ece991736cf,

title = "Java Ranger at SV-COMP 2020 (Competition Contribution)",

abstract = "Path-merging is a known technique for accelerating symbolic execution. One technique, named “veritesting” by Avgerinos et al. uses summaries of bounded control-flow regions and has been shown to accelerate symbolic execution of binary code. But, when applied to symbolic execution of Java code, veritesting needs to be extended to summarize dynamically dispatched methods and exceptional control-flow. Such an extension of veritesting has been implemented in Java Ranger by implementing as an extension of Symbolic PathFinder, a symbolic executor for Java bytecode. In this paper, we briefly describe the architecture of Java Ranger and describe its setup for SV-COMP 2020.",

author = "Vaibhav Sharma and Soha Hussein and Whalen, {Michael W.} and Stephen McCamant and Willem Visser",

note = "Publisher Copyright: {\textcopyright} 2020, The Author(s).; 26th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2020, held as part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2020 ; Conference date: 25-04-2020 Through 30-04-2020",

year = "2020",

doi = "10.1007/978-3-030-45237-7_27",

language = "English (US)",

isbn = "9783030452360",

series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

publisher = "Springer",

pages = "393--397",

editor = "Armin Biere and David Parker",

booktitle = "Tools and Algorithms for the Construction and Analysis of Systems- 26th International Conference, TACAS 2020, held as part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2020, Proceedings, Part II",

}

TY - GEN

T1 - Java Ranger at SV-COMP 2020 (Competition Contribution)

AU - Sharma, Vaibhav

AU - Hussein, Soha

AU - Whalen, Michael W.

AU - McCamant, Stephen

AU - Visser, Willem

PY - 2020

Y1 - 2020

N2 - Path-merging is a known technique for accelerating symbolic execution. One technique, named “veritesting” by Avgerinos et al. uses summaries of bounded control-flow regions and has been shown to accelerate symbolic execution of binary code. But, when applied to symbolic execution of Java code, veritesting needs to be extended to summarize dynamically dispatched methods and exceptional control-flow. Such an extension of veritesting has been implemented in Java Ranger by implementing as an extension of Symbolic PathFinder, a symbolic executor for Java bytecode. In this paper, we briefly describe the architecture of Java Ranger and describe its setup for SV-COMP 2020.

AB - Path-merging is a known technique for accelerating symbolic execution. One technique, named “veritesting” by Avgerinos et al. uses summaries of bounded control-flow regions and has been shown to accelerate symbolic execution of binary code. But, when applied to symbolic execution of Java code, veritesting needs to be extended to summarize dynamically dispatched methods and exceptional control-flow. Such an extension of veritesting has been implemented in Java Ranger by implementing as an extension of Symbolic PathFinder, a symbolic executor for Java bytecode. In this paper, we briefly describe the architecture of Java Ranger and describe its setup for SV-COMP 2020.

UR - http://www.scopus.com/inward/record.url?scp=85083988398&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=85083988398&partnerID=8YFLogxK

U2 - 10.1007/978-3-030-45237-7_27

DO - 10.1007/978-3-030-45237-7_27

M3 - Conference contribution

AN - SCOPUS:85083988398

SN - 9783030452360

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 393

EP - 397

BT - Tools and Algorithms for the Construction and Analysis of Systems- 26th International Conference, TACAS 2020, held as part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2020, Proceedings, Part II

A2 - Biere, Armin

A2 - Parker, David

PB - Springer

T2 - 26th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2020, held as part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2020

Y2 - 25 April 2020 through 30 April 2020

ER -

Java Ranger at SV-COMP 2020 (Competition Contribution)

Abstract

Publication series

Conference

Bibliographical note

Access

OpenUrl availability

Other files and links

Fingerprint

Cite this