What is Symbiotic?

Symbiotic is a framework for analysis of 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. Additionally, it can decide termination property. Symbiotic combines static analysis, compile-time code instrumentation, program slicing, and symbolic execution and it integrates several libraries and tools including DG, our clone of Klee called JetKlee, Predator, SlowBeast, Z3 and others. The framework uses LLVM as internal program representation. Symbiotic is highly modular and all of its components can be used separately.

Symbiotic Components

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).

Awards

Publications

  1. J. Slaby, J. Strejček, and M. Trtík: Checking Properties Described by State Machines: On Synergy of Instrumentation, Slicing, and Symbolic Execution, in Proceedings of FMICS 2012, volume 7437 of LNCS, pages 207-221. Springer, 2012. [link]

  2. J. Slaby, J. Strejček, and M. Trtík: Symbiotic: Synergy of Instrumentation, Slicing, and Symbolic Execution (Competition Contribution), in Proceedings of TACAS 2013, volume 7795 of LNCS, pages 630-632. Springer, 2013. [link]

  3. J. Slaby and J. Strejček: Symbiotic 2: More Precise Slicing (Competition Contribution), in Proceedings of TACAS 2014, volume 8413 of LNCS, pages 415-417. Springer, 2014. [link]

  4. M. Chalupa, M. Jonáš, J. Slaby, J. Strejček, and M. Vitovská: Symbiotic 3: New Slicer and Error-Witness Generation (Competition Contribution), in Proceedings of TACAS 2016, volume 9636 of LNCS, pages 946-949. Springer, 2016. [link]

  5. M. Chalupa, M. Vitovská, M. Jonáš, J. Slaby, and J. Strejček: Symbiotic 4: Beyond Reachability (Competition Contribution), in Proceedings of TACAS 2017, volume 10206 of LNCS, pages 385-389. Springer, 2017. [link]

  6. M. Chalupa, M. Vitovská, and J. Strejček: Symbiotic 5: Boosted Instrumentation (Competition Contribution), in Proceedings of TACAS 2018, volume 10806 of LNCS, pages 442-226. Springer, 2018. [link]

  7. M. Chalupa, M. Vitovská, T. Jašek, M. Šimáček, and J. Strejček: Symbiotic 6: Generating Test-Cases by Slicing and Symbolic Execution, International Journal on Software Tools for Technology Transfer 23(6): 875-877, 2021. [link]

  8. M. Chalupa, T. Jašek, L. Tomovič, M. Hruška, V. Šoková, P. Ayaziová, J. Strejček, and T. Vojnar: Symbiotic 7: Integration of Predator and More (Competition Contribution), in Proceedings of TACAS 2020, volume 12079 of LNCS, pages 413-417. Springer, 2020. [link]

  9. M. Chalupa, T. Jašek, J. Novák, A. Řechtáčková, V. Šoková, and J. Strejček: Symbiotic 8: Beyond Symbolic Execution (Competition Contribution), in Proceedings of TACAS 2021, volume 12652 of LNCS, pages 453-457. Springer, 2021. [link]

  10. M. Chalupa, J. Novák, and J. Strejček: Symbiotic 8: Parallel and Targeted Test Generation (Competition Contribution), in Proceedings of FASE 2021, volume 12649 of LNCS, pages 368-372. Springer, 2021. [link]

  11. M. Chalupa, V. Mihalkovič, A. Řechtáčková, L. Zaoral, and J. Strejček: Symbiotic 9: String Analysis and Backward Symbolic Execution with Loop Folding (Competition Contribution), in Proceedings of TACAS 2022, volume 13244 of LNCS, pages 462-467. Springer, 2022. [link]

Contact

For more information send an e-mail to statica@fi.muni.cz. We’ll be happy to answer your questions :)