{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,16]],"date-time":"2026-04-16T02:08:02Z","timestamp":1776305282914,"version":"3.50.1"},"publisher-location":"Cham","reference-count":14,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783030995263","type":"print"},{"value":"9783030995270","type":"electronic"}],"license":[{"start":{"date-parts":[[2022,1,1]],"date-time":"2022-01-01T00:00:00Z","timestamp":1640995200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2022,3,30]],"date-time":"2022-03-30T00:00:00Z","timestamp":1648598400000},"content-version":"vor","delay-in-days":88,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2022]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>The development of <jats:sc>Symbiotic<\/jats:sc> \u00a09 focused mainly on two components. One is the symbolic executor <jats:sc>Slowbeast<\/jats:sc>, which newly supports <jats:italic>backward symbolic execution<\/jats:italic> including its extension called <jats:italic>loop folding<\/jats:italic>. This technique can infer inductive invariants from backward symbolic execution states. Thanks to these invariants, <jats:sc>Symbiotic<\/jats:sc> \u00a09 is able to produce non-trivial correctness witnesses, which is a feature that is missing in previous versions of <jats:sc>Symbiotic<\/jats:sc>. We have also extended forward symbolic execution in <jats:sc>Slowbeast<\/jats:sc> with a basic support for parallel programs. The second component with significant improvements is the instrumentation module. In particular, we have extended the static analysis of accesses to arrays with features designed for programs that manipulate C strings.<\/jats:p><jats:p><jats:sc>Symbiotic<\/jats:sc> \u00a09 is the <jats:italic>Overall<\/jats:italic> winner of <jats:sc>SV-COMP<\/jats:sc> \u00a02022. Moreover, it won also the categories <jats:italic>MemSafety<\/jats:italic> and <jats:italic>SoftwareSystems<\/jats:italic>, and placed third in <jats:italic>FalsificationOverall<\/jats:italic>.<\/jats:p>","DOI":"10.1007\/978-3-030-99527-0_32","type":"book-chapter","created":{"date-parts":[[2022,3,29]],"date-time":"2022-03-29T06:37:21Z","timestamp":1648535841000},"page":"462-467","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":22,"title":["Symbiotic 9: String Analysis and Backward Symbolic Execution with Loop Folding"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-1132-5516","authenticated-orcid":false,"given":"Marek","family":"Chalupa","sequence":"first","affiliation":[]},{"given":"Vincent","family":"Mihalkovi\u010d","sequence":"additional","affiliation":[]},{"given":"Anna","family":"\u0158echt\u00e1\u010dkov\u00e1","sequence":"additional","affiliation":[]},{"given":"Luk\u00e1\u0161","family":"Zaoral","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0001-5873-403X","authenticated-orcid":false,"given":"Jan","family":"Strej\u010dek","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2022,3,30]]},"reference":[{"key":"32_CR1","doi-asserted-by":"crossref","unstructured":"Beyer, D.: Progress on software verification: SV-COMP 2022. In: Proc. TACAS. Springer (2022)","DOI":"10.1007\/978-3-030-99527-0_20"},{"key":"32_CR2","doi-asserted-by":"publisher","unstructured":"Beyer, D.: Verifiers and validators of the 11th Intl. Competition on Software Verification (SV-COMP 2022). Zenodo (2022). https:\/\/doi.org\/10.5281\/zenodo.5959149","DOI":"10.5281\/zenodo.5959149"},{"key":"32_CR3","doi-asserted-by":"publisher","unstructured":"Beyer, D., Jakobs, M.: Fred: Conditional model checking via reducers and folders. In: SEFM 2020. LNCS, vol. 12310, pp. 113\u2013132. Springer (2020). https:\/\/doi.org\/10.1007\/978-3-030-58768-0_7","DOI":"10.1007\/978-3-030-58768-0_7"},{"key":"32_CR4","unstructured":"Cadar, C., Dunbar, D., Engler, D.R.: KLEE: Unassisted and automatic generation of high-coverage tests for complex systems programs. In: OSDI. pp. 209\u2013224. USENIX Association (2008), http:\/\/www.usenix.org\/events\/osdi08\/tech\/full_papers\/cadar\/cadar.pdf"},{"key":"32_CR5","doi-asserted-by":"crossref","unstructured":"Chalupa, M.: DG: analysis and slicing of LLVM bitcode. In: ATVA 2020. LNCS, vol. 12302, pp. 557\u2013563. Springer (2020), https:\/\/doi.org\/10.1007\/978-3-030-59152-6_33","DOI":"10.1007\/978-3-030-59152-6_33"},{"key":"32_CR6","doi-asserted-by":"publisher","unstructured":"Chalupa, M.: Symbiotic 9: String analysis and backward symbolic execution with loop folding (artifact). Zenodo (2022). https:\/\/doi.org\/10.5281\/zenodo.5947909","DOI":"10.5281\/zenodo.5947909"},{"key":"32_CR7","doi-asserted-by":"publisher","unstructured":"Chalupa, M., Ja\u0161ek, T., Nov\u00e1k, J., \u0158echt\u00e1\u010dkov\u00e1, A., \u0160okov\u00e1, V., Strej\u010dek, J.: Symbiotic 8: Beyond symbolic execution - (competition contribution). In: TACAS 2021. LNCS, vol. 12652, pp. 453\u2013457. Springer (2021). https:\/\/doi.org\/10.1007\/978-3-030-72013-1_31","DOI":"10.1007\/978-3-030-72013-1_31"},{"key":"32_CR8","doi-asserted-by":"publisher","unstructured":"Chalupa, M., Strej\u010dek, J.: Backward symbolic execution with loop folding. In: SAS 2021. LNCS, vol. 12913, pp. 49\u201376. Springer (2021). https:\/\/doi.org\/10.1007\/978-3-030-88806-0_3","DOI":"10.1007\/978-3-030-88806-0_3"},{"key":"32_CR9","doi-asserted-by":"publisher","unstructured":"Chandra, S., Fink, S.J., Sridharan, M.: Snugglebug: a powerful approach to weakest preconditions. In: PLDI 2009. pp. 363\u2013374. ACM (2009). https:\/\/doi.org\/10.1145\/1542476.1542517","DOI":"10.1145\/1542476.1542517"},{"key":"32_CR10","doi-asserted-by":"crossref","unstructured":"Lattner, C., Adve, V.S.: LLVM: A compilation framework for lifelong program analysis & transformation. In: CGO 2004. pp. 75\u201388. IEEE Computer Society (2004), https:\/\/doi.org\/10.1109\/CGO.2004.1281665","DOI":"10.1109\/CGO.2004.1281665"},{"key":"32_CR11","doi-asserted-by":"crossref","unstructured":"de\u00a0Moura, L.M., Bj\u00f8rner, N.: Z3: an efficient SMT solver. In: TACAS 2008. LNCS, vol.\u00a04963, pp. 337\u2013340. Springer (2008), https:\/\/doi.org\/10.1007\/978-3-540-78800-3_24","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"32_CR12","unstructured":"Slowbeast repository. https:\/\/gitlab.com\/mchalupa\/slowbeast (2021)"},{"key":"32_CR13","unstructured":"Weiser, M.: Program slicing. In: Proceedings of ICSE. pp. 439\u2013449. IEEE (1981)"},{"key":"32_CR14","unstructured":"\u0158cht\u00e1\u010dkov\u00e1 A, A.: Improving out-of-bound access checking in Symbiotic (2020), https:\/\/is.muni.cz\/th\/tmq7m\/, bachelor thesis, accessed 2022-02-02"}],"container-title":["Lecture Notes in Computer Science","Tools and Algorithms for the Construction and Analysis of Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-99527-0_32","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,3,12]],"date-time":"2024-03-12T08:50:54Z","timestamp":1710233454000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-030-99527-0_32"}},"subtitle":["(Competition Contribution)"],"short-title":[],"issued":{"date-parts":[[2022]]},"ISBN":["9783030995263","9783030995270"],"references-count":14,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-99527-0_32","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2022]]},"assertion":[{"value":"30 March 2022","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"TACAS","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Tools and Algorithms for the Construction and Analysis of Systems","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Munich","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Germany","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2022","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2 April 2022","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"7 April 2022","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"28","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"tacas2022","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/etaps.org\/2022\/tacas","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Single-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"EasyChair","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"159","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"46","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"4","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"29% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"10","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Yes","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"16 tool papers of the affiliated competition SV-Comp and 1 paper consisting of the competition report are also included in the proceedings","order":10,"name":"additional_info_on_review_process","label":"Additional Info on Review Process","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}