What is Symbiotic?
Symbiotic is a tool for analysis of sequential computer programs written in the programming language C. It can check all common safety properties like assertion violations, invalid pointer dereference, double free, memory leaks, etc. Symbiotic combines light-weight static analysis, compile-time code instrumentation, program slicing, and symbolic execution [1, 2, 3]. We use LLVM as internal program representation. Symbiotic is highly modular and all of its components can be used separately.
Symbiotic won the gold medal in MemSafety and SoftwareSystems categories and took the 4th place in the meta category Overall in SV-COMP 2021.
Symbiotic won the silver medal in MemSafety category, the gold medal in SoftwareSystems category, 2nd place in FalsificationOverall meta category (finding bugs) and 4th place in the meta category Overall in SV-COMP 2020.
Symbiotic won the gold medal in MemSafety category and 4th place in the meta category Overall and FalsificationOverall of SV-COMP 2019. Complete results can be found at the official SV-COMP 2019 site.
Symbiotic won the gold medal in MemSafety category, Bronze medal in the FalsificationOverall meta category and took 4th place in the Overall category of SV-COMP 2018. Complete results can be found official SV-COMP 2018 site.
We participated in SV-COMP 2017 and we won the bronze medal in MemSafety category. Complete results can be found official SV-COMP 2017 site.
We participated in SV-COMP 2016 with this particular release: https://github.com/staticafi/symbiotic/releases/tag/3.0.1 and we won the bronze medal in Arrays category. Complete results can be found official SV-COMP 2016 site.
Components of Symbiotic can be found at https://github.com/staticafi with the only exception of the slicer, that can be found at https://github.com/mchalupa/dg (it will be moved to staticafi in the future though). All parts of Symbiotic are open-source projects and are licensed under various open-source licenses (GPL, MIT license, University of Illinois Open Source license)
For more information send an e-mail to email@example.com. We’ll be happy to answer your questions :)
 Slabý, Jiří and Strejček, Jan and Trtík, Marek. Checking Properties Described by State Machines: On Synergy of Instrumentation, Slicing, and Symbolic Execution. link
 Chalupa, Jonáš, Slaby, Strejček, Vitovská. Symbiotic 3: New Slicer and Error-Witness Generation. link
 Chalupa, Jašek, Tomovič, Hruška, Šoková, Ayaziová, Strejček. Symbiotic 7: Integration of Predator and More. link