Publication detail

Symbiotic 7: Integration of Predator and More (Competition Contribution)

HRUŠKA, M. CHALUPA, M. JAŠEK, T. STREJČEK, J. ŠOKOVÁ, V. VOJNAR, T. AYAZIOVÁ, P. TOMOVIČ, L.

Original Title

Symbiotic 7: Integration of Predator and More (Competition Contribution)

Type

conference paper

Language

English

Original Abstract

Symbiotic 7 brings improvements in all parts of the tool. In particular, we integrated the advanced shape analysis implemented in Predator to our instrumentation process for memory safety checking. Further, we extended our slicer to correctly handle non-terminating pro- grams. This new slicing is applied in termination analysias, where we also added instrumentation for detection of simple cycles in the program state space. The witness generation process changed as well.

Keywords

Symbiotic, Predator, slicing, symbolic execution, symbolic memory graphs, Klee, static analysis

Authors

HRUŠKA, M.; CHALUPA, M.; JAŠEK, T.; STREJČEK, J.; ŠOKOVÁ, V.; VOJNAR, T.; AYAZIOVÁ, P.; TOMOVIČ, L.

Released

26. 2. 2020

Publisher

Springer International Publishing

Location

Cham

ISBN

978-3-030-45236-0

Book

Proceedings of TACAS 2020 (2)

Edition

Lecture Notes in Computer Science

Pages from

413

Pages to

417

Pages count

5

URL

https://www.fit.vut.cz/research/publication/12199/

BibTex

@inproceedings{BUT162537,
  author="HRUŠKA, M. and CHALUPA, M. and JAŠEK, T. and STREJČEK, J. and ŠOKOVÁ, V. and VOJNAR, T. and AYAZIOVÁ, P. and TOMOVIČ, L.",
  title="Symbiotic 7: Integration of Predator and More (Competition Contribution)",
  booktitle="Proceedings of TACAS 2020 (2)",
  year="2020",
  series="Lecture Notes in Computer Science",
  volume="12079",
  pages="413--417",
  publisher="Springer International Publishing",
  address="Cham",
  doi="10.1007/978-3-030-45237-7\{_}31",
  isbn="978-3-030-45236-0",
  url="https://www.fit.vut.cz/research/publication/12199/"
}

Documents

Chalupa2020_Chapter_Symbiotic7IntegrationOfPredato.pdf