| CHALUPA, Marek, Tomáš JAŠEK, Jakub NOVÁK, Anna ŘECHTÁČKOVÁ, Veronika ŠOKOVÁ and Jan STREJČEK. Symbiotic 8: Beyond Symbolic Execution. In Jan Friso Groote, Kim Guldstrand Larsen. Tools and Algorithms for the Construction and Analysis of Systems - 27th International Conference, TACAS 2021, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2021, Luxembourg City, Luxembourg, March 27 - April 1, 2021, Proceedings, Part II. Cham (Švýcarsko): Springer, Cham, 2021, p. 453-457. ISBN 978-3-030-72012-4. Available from: https://dx.doi.org/10.1007/978-3-030-72013-1_31. |
Other formats:
BibTeX
LaTeX
RIS
@inproceedings{1783925,
author = {Chalupa, Marek and Jašek, Tomáš and Novák, Jakub and Řechtáčková, Anna and Šoková, Veronika and Strejček, Jan},
address = {Cham (Švýcarsko)},
booktitle = {Tools and Algorithms for the Construction and Analysis of Systems - 27th International Conference, TACAS 2021, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2021, Luxembourg City, Luxembourg, March 27 - April 1, 2021, Proceedings, Part II},
doi = {http://dx.doi.org/10.1007/978-3-030-72013-1_31},
editor = {Jan Friso Groote, Kim Guldstrand Larsen},
keywords = {symbolic execution;k-induction;program slicing;symbiotic;predator;klee},
howpublished = {tištěná verze "print"},
language = {eng},
location = {Cham (Švýcarsko)},
isbn = {978-3-030-72012-4},
pages = {453-457},
publisher = {Springer, Cham},
title = {Symbiotic 8: Beyond Symbolic Execution},
url = {https://link.springer.com/chapter/10.1007%2F978-3-030-72013-1_31},
year = {2021}
}
TY - JOUR
ID - 1783925
AU - Chalupa, Marek - Jašek, Tomáš - Novák, Jakub - Řechtáčková, Anna - Šoková, Veronika - Strejček, Jan
PY - 2021
TI - Symbiotic 8: Beyond Symbolic Execution
PB - Springer, Cham
CY - Cham (Švýcarsko)
SN - 9783030720124
KW - symbolic execution;k-induction;program slicing;symbiotic;predator;klee
UR - https://link.springer.com/chapter/10.1007%2F978-3-030-72013-1_31
N2 - Symbiotic 8 extends the traditional combination of static analyses, instrumentation, program slicing, and symbolic execution with one substantial novelty, namely a technique mixing symbolic execution with k-induction. This technique can prove the correctness of programs with possibly unbounded loops, which cannot be done by classic symbolic execution. Symbiotic 8 delivers also several other improvements. In particular, we have modified our fork of the symbolic executor Klee to support the comparison of symbolic pointers. Further, we have tuned the shape analysis tool Predator (integrated already in Symbiotic 7) to perform better on llvm bitcode. We have also developed a light-weight analysis of relations between variables that can prove the absence of out-of-bound accesses to arrays.
ER -
CHALUPA, Marek, Tomáš JAŠEK, Jakub NOVÁK, Anna ŘECHTÁČKOVÁ, Veronika ŠOKOVÁ and Jan STREJČEK. Symbiotic 8: Beyond Symbolic Execution. In Jan Friso Groote, Kim Guldstrand Larsen. \textit{Tools and Algorithms for the Construction and Analysis of Systems - 27th International Conference, TACAS 2021, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2021, Luxembourg City, Luxembourg, March 27 - April 1, 2021, Proceedings, Part II}. Cham (Švýcarsko): Springer, Cham, 2021, p.~453-457. ISBN~978-3-030-72012-4. Available from: https://dx.doi.org/10.1007/978-3-030-72013-1\_{}31.
|
