Symbiotic 4: Beyond Reachability (Competition Contribution)

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 JONÁŠ Martin SLABÝ Jiří STREJČEK Jan

Type Article in Proceedings
Conference Tools and Algorithms for the Construction and Analysis of Systems: 23rd International Conference
MU Faculty or unit

Faculty of Informatics

Citation
Web https://link.springer.com/chapter/10.1007/978-3-662-54580-5_28
Doi http://dx.doi.org/10.1007/978-3-662-54580-5_28
Field Informatics
Keywords Symbiotic; program analysis; program verification; SV-COMP 2017
Description The fourth version of Symbiotic brings a brand new instrumentation part, which can now instrument the analyzed program with code pieces checking various specification properties. As a consequence, Symbiotic 4 participates for the first time also in categories focused on memory safety. Further, we have ported both Symbiotic and Klee to LLVM 3.8 and added new features to the slicer which is now modular and easily extensible.
Related projects: