{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,10]],"date-time":"2025-10-10T19:08:16Z","timestamp":1760123296947,"version":"3.40.3"},"publisher-location":"Cham","reference-count":12,"publisher":"Springer Nature Switzerland","isbn-type":[{"type":"print","value":"9783031572586"},{"type":"electronic","value":"9783031572593"}],"license":[{"start":{"date-parts":[[2024,1,1]],"date-time":"2024-01-01T00:00:00Z","timestamp":1704067200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2024,4,6]],"date-time":"2024-04-06T00:00:00Z","timestamp":1712361600000},"content-version":"vor","delay-in-days":96,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2024]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>Dynamic Symbolic Execution (DSE) is an important method for the testing of programs. The major advantage of DSE is its path-by-path exploration of the program execution space. However, this often leads to the path explosion problem. To address this issue, a method of abstraction learning has been used. The key step here is the computation of an interpolant to represent the learned abstraction. In Test-Comp 2024, we use two different approaches of interpolant generation viz., Deletion Interpolation and Weakest Precondition Interpolation. The former is our more stable and mature system and briefly discussed in [8]. In this paper, we present the latter approach which is the heart of TracerX. In general, the Weakest Precondition (WP) is the ideal (most general) interpolant. However, WP is intractable to compute and is exponentially disjunctive. A major challenge is to obtain a conjunctive approximation of the WP. Therefore, we generate an approximation of the WP.<\/jats:p>","DOI":"10.1007\/978-3-031-57259-3_19","type":"book-chapter","created":{"date-parts":[[2024,4,5]],"date-time":"2024-04-05T13:01:39Z","timestamp":1712322099000},"page":"320-325","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":2,"title":["TracerX: Pruning Dynamic Symbolic Execution with Deletion and Weakest Precondition Interpolation (Competition Contribution)"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-7887-3264","authenticated-orcid":false,"given":"Arpita","family":"Dutta","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-8147-6590","authenticated-orcid":false,"given":"Rasool","family":"Maghareh","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0001-9988-6144","authenticated-orcid":false,"given":"Joxan","family":"Jaffar","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-6169-6334","authenticated-orcid":false,"given":"Sangharatna","family":"Godboley","sequence":"additional","affiliation":[]},{"given":"Xiao Liang","family":"Yu","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2024,4,6]]},"reference":[{"key":"19_CR1","doi-asserted-by":"crossref","unstructured":"Test-comp 2024, https:\/\/test-comp.sosy-lab.org\/2024\/","DOI":"10.2172\/2376289"},{"key":"19_CR2","unstructured":"TracerX with Deletion Interpolation, https:\/\/doi.org\/10.5281\/zenodo.10200610"},{"key":"19_CR3","unstructured":"TracerX with WP Interpolation, https:\/\/doi.org\/10.5281\/zenodo.10202605"},{"key":"19_CR4","unstructured":"Beyer, D.: Automatic testing of C programs: Test-Comp 2024. Springer (2024)"},{"key":"19_CR5","unstructured":"Cadar, C., Dunbar, D., Engler, D.R., et\u00a0al.: KLEE: unassisted and automatic generation of high-coverage tests for complex systems programs. In: 8th USENIX Symposium on Operating Systems Design and Implementation, OSDI. pp. 209\u2013224 (2008)"},{"key":"19_CR6","doi-asserted-by":"crossref","unstructured":"Godboley, S., Jaffar, J., Maghareh, R., Dutta, A.: Toward optimal MC\/DC test case generation. In: Proceedings of the 30th ACM SIGSOFT International Symposium on Software Testing and Analysis. pp. 505\u2013516 (2021)","DOI":"10.1145\/3460319.3464841"},{"key":"19_CR7","doi-asserted-by":"crossref","unstructured":"Jaffar, J., Godboley, S., Maghareh, R.: Optimal MC\/DC test case generation. In: 2019 IEEE\/ACM 41st International Conference on Software Engineering: Companion Proceedings (ICSE-Companion). pp. 288\u2013289. IEEE (2019)","DOI":"10.1109\/ICSE-Companion.2019.00118"},{"key":"19_CR8","doi-asserted-by":"crossref","unstructured":"Jaffar, J., Maghareh, R., Godboley, S., Ha, X.L.: TracerX: Dynamic symbolic execution with interpolation (competition contribution). In: Fundamental Approaches to Software Engineering (FASE). vol. 12076, p.\u00a0530. Springer (2020)","DOI":"10.1007\/978-3-030-45234-6_28"},{"key":"19_CR9","doi-asserted-by":"crossref","unstructured":"Jaffar, J., Murali, V., Navas, J.A., Santosa, A.E.: TRACER: a symbolic execution tool for verification. In: 24th International Conference on Computer Aided Verification (CAV). pp. 758\u2013766. Springer (2012)","DOI":"10.1007\/978-3-642-31424-7_61"},{"key":"19_CR10","doi-asserted-by":"crossref","unstructured":"Jaffar, J., Santosa, A.E., Voicu, R.: An interpolation method for CLP traversal. In: 15th International Conference on Principles and Practice of Constraint Programming (CP). pp. 454\u2013469. Springer (2009)","DOI":"10.1007\/978-3-642-04244-7_37"},{"key":"19_CR11","unstructured":"Lattner, C., Adve, V.: LLVM: A compilation framework for lifelong program analysis & transformation. In: International symposium on code generation and optimization, 2004. CGO 2004. pp. 75\u201386. IEEE (2004)"},{"key":"19_CR12","unstructured":"O\u2019Hearn, P., Reynolds, J., Yang, H.: Local reasoning about programs that alter data structures. In: Computer Science Logic: 15th International Workshop, CSL 2001 10th Annual Conference of the EACSL Paris. pp. 1\u201319. Springer (2001)"}],"container-title":["Lecture Notes in Computer Science","Fundamental Approaches to Software Engineering"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-57259-3_19","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,11,15]],"date-time":"2024-11-15T19:39:04Z","timestamp":1731699544000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-57259-3_19"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024]]},"ISBN":["9783031572586","9783031572593"],"references-count":12,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-57259-3_19","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2024]]},"assertion":[{"value":"6 April 2024","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"FASE","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Fundamental Approaches to Software Engineering","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Luxembourg City","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Luxembourg","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2024","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"6 April 2024","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"11 April 2024","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"27","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"fase2024","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/etaps.org\/2024\/conferences\/fase\/","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":"41","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":"14","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":"5","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":"34% - 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-4","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":"4","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)"}}]}}