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

Investor logo

Warning

This publication doesn't include Institute of Computer Science. It includes Faculty of Informatics. Official publication website can be found on muni.cz.
Authors

CHALUPA Marek JAŠEK Tomáš TOMOVIČ Lukáš HRUŠKA Martin ŠOKOVÁ Veronika AYAZIOVÁ Paulína STREJČEK Jan VOJNAR Tomáš

Year of publication 2020
Type Article in Proceedings
Conference Tools and Algorithms for the Construction and Analysis of Systems
MU Faculty or unit

Faculty of Informatics

Citation
Web https://doi.org/10.1007/978-3-030-45237-7_31
Doi http://dx.doi.org/10.1007/978-3-030-45237-7_31
Keywords Symbiotic;Predator;Program Slicing;Termination Analysis;Shape Analysis;Symbolic Execution
Description 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 programs. This new slicing is applied in termination analysis, where we also added instrumentation for detection of simple cycles in the program state space. The witness generation process changed as well.
Related projects:

You are running an old browser version. We recommend updating your browser to its latest version.

More info