Symbiotic 5: Boosted Instrumentation (Competition Contribution)

Investor logo

Warning

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

CHALUPA Marek VITOVSKÁ Martina STREJČEK Jan

Year of publication 2018
Type Article in Proceedings
Conference Tools and Algorithms for the Construction and Analysis of Systems, 24th International Conference, Proceedings, Part II
MU Faculty or unit

Faculty of Informatics

Citation
Doi http://dx.doi.org/10.1007/978-3-319-89963-3_29
Keywords Symbiotic; program analysis; program verification; SV-COMP 2018
Description The fifth version of Symbiotic significantly improves instrumentation capabilities that the tool uses to participate in the category MemSafety. It leverages an extended pointer analysis re-designed for instrumenting programs with memory safety errors, and staged instrumentation reducing the number of inserted function calls that track or check the memory state. Apart from various bugfixes, we have ported Symbiotic (including the external symbolic executor Klee) to llvm 3.9 and improved the generation of violation witnesses by providing values of some variables.
Related projects:

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