Java Ranger at SV-COMP 2020 (Competition Contribution)

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, verit...

Descripción completa

Detalles Bibliográficos
Autores principales: Sharma, Vaibhav, Hussein, Soha, Whalen, Michael W., McCamant, Stephen, Visser, Willem
Formato: Online Artículo Texto
Lenguaje:English
Publicado: 2020
Materias:
Article
Acceso en línea:https://www.ncbi.nlm.nih.gov/pmc/articles/PMC7480705/
http://dx.doi.org/10.1007/978-3-030-45237-7_27
_version_ 1783580463493808128
author Sharma, Vaibhav
Hussein, Soha
Whalen, Michael W.
McCamant, Stephen
Visser, Willem
author_facet Sharma, Vaibhav
Hussein, Soha
Whalen, Michael W.
McCamant, Stephen
Visser, Willem
author_sort Sharma, Vaibhav
collection PubMed
description 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.
format Online
Article
Text
id pubmed-7480705
institution National Center for Biotechnology Information
language English
publishDate 2020
record_format MEDLINE/PubMed
spelling pubmed-74807052020-09-10 Java Ranger at SV-COMP 2020 (Competition Contribution) Sharma, Vaibhav Hussein, Soha Whalen, Michael W. McCamant, Stephen Visser, Willem Tools and Algorithms for the Construction and Analysis of Systems Article 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. 2020-03-13 /pmc/articles/PMC7480705/ http://dx.doi.org/10.1007/978-3-030-45237-7_27 Text en © The Author(s) 2020 Open Access This chapter is licensed under the terms of the Creative Commons Attribution 4.0 International License (http://creativecommons.org/licenses/by/4.0/), which permits use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons license and indicate if changes were made. The images or other third party material in this chapter are included in the chapter's Creative Commons license, unless indicated otherwise in a credit line to the material. If material is not included in the chapter's Creative Commons license and your intended use is not permitted by statutory regulation or exceeds the permitted use, you will need to obtain permission directly from the copyright holder.
spellingShingle Article
Sharma, Vaibhav
Hussein, Soha
Whalen, Michael W.
McCamant, Stephen
Visser, Willem
Java Ranger at SV-COMP 2020 (Competition Contribution)
title Java Ranger at SV-COMP 2020 (Competition Contribution)
title_full Java Ranger at SV-COMP 2020 (Competition Contribution)
title_fullStr Java Ranger at SV-COMP 2020 (Competition Contribution)
title_full_unstemmed Java Ranger at SV-COMP 2020 (Competition Contribution)
title_short Java Ranger at SV-COMP 2020 (Competition Contribution)
title_sort java ranger at sv-comp 2020 (competition contribution)
topic Article
url https://www.ncbi.nlm.nih.gov/pmc/articles/PMC7480705/
http://dx.doi.org/10.1007/978-3-030-45237-7_27
work_keys_str_mv AT sharmavaibhav javarangeratsvcomp2020competitioncontribution
AT husseinsoha javarangeratsvcomp2020competitioncontribution
AT whalenmichaelw javarangeratsvcomp2020competitioncontribution
AT mccamantstephen javarangeratsvcomp2020competitioncontribution
AT visserwillem javarangeratsvcomp2020competitioncontribution

Ejemplares similares