{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,3]],"date-time":"2026-07-03T16:33:57Z","timestamp":1783096437631,"version":"3.54.6"},"publisher-location":"Cham","reference-count":11,"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>BRICK is a bounded reachability checker for embedded C programs. BRICK conducts a path-oriented style checking of the bounded state space of the program, that enumerates and checks all the possible paths of the program in the threshold one by one. To alleviate the path explosion problem, BRICK locates and records unsatisfiable core path segments during the checking of each path and uses them to prune the search space. Furthermore, derivative free optimization based falsification and loop induction are introduced to handle complex program features like nonlinear path conditions and loops efficiently.<\/jats:p>","DOI":"10.1007\/978-3-030-99527-0_22","type":"book-chapter","created":{"date-parts":[[2022,3,29]],"date-time":"2022-03-29T06:37:21Z","timestamp":1648535841000},"page":"408-412","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":14,"title":["BRICK: Path Enumeration Based Bounded Reachability Checking of C Program (Competition Contribution)"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-0517-7801","authenticated-orcid":false,"given":"Lei","family":"Bu","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Zhunyi","family":"Xie","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Lecheng","family":"Lyu","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Yichao","family":"Li","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Xiao","family":"Guo","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Jianhua","family":"Zhao","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Xuandong","family":"Li","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2022,3,30]]},"reference":[{"key":"22_CR1","unstructured":"L. Bu, et al.. BACH: Bounded Reachability Checker for Linear Hybrid Automata. In FMCAD\u201908, pp. 65-68."},{"key":"22_CR2","doi-asserted-by":"crossref","unstructured":"D. Xie, et al.. SAT-LP-IIS Joint-Directed Path-Oriented Bounded Reachability Analysis of Linear Hybrid Automata. In FMSD. 45(1): 42-62, 2014.","DOI":"10.1007\/s10703-014-0210-3"},{"key":"22_CR3","doi-asserted-by":"crossref","unstructured":"N. E\u00e9nand N. S\u00f6rensson. An extensible SAT-solver. In SAT\u201903, 502-518.","DOI":"10.1007\/978-3-540-24605-3_37"},{"key":"22_CR4","doi-asserted-by":"crossref","unstructured":"S. Gao, et al.. dReal: An SMT solver for nonlinear theories over the reals. In CADE\u201913, 208-214.","DOI":"10.1007\/978-3-642-38574-2_14"},{"key":"22_CR5","doi-asserted-by":"crossref","unstructured":"D. Kroening, et al.. CBMC - C Bounded Model Checker. In TACAS\u201914: 389-391.","DOI":"10.1007\/978-3-642-54862-8_26"},{"key":"22_CR6","doi-asserted-by":"crossref","unstructured":"L. De Moura and N. Bj\u00f8rner. Z3: An Efficient SMT Solver. In TACAS\u201908: 337-340.","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"22_CR7","doi-asserted-by":"crossref","unstructured":"P. Darke, et al.. VeriAbs: Verification by Abstraction and Test Generation - (Competition Contribution). In TACAS\u201918: 457-462.","DOI":"10.1007\/978-3-319-89963-3_32"},{"key":"22_CR8","doi-asserted-by":"crossref","unstructured":"L. Bu, et al.. Machine learning steered symbolic execution framework for complex software code. In Formal Aspects of Computing, 33:3, 301-323, 2021.","DOI":"10.1007\/s00165-021-00538-3"},{"key":"22_CR9","unstructured":"Y. Yu, et al.. Derivative-free optimization via classification. In AAAI\u201916, 2286-2292."},{"key":"22_CR10","doi-asserted-by":"crossref","unstructured":"D. Beyer, Progress on Software Verification: SV-COMP 2022. In TACAS\u201922","DOI":"10.1007\/978-3-030-99527-0_20"},{"key":"22_CR11","doi-asserted-by":"publisher","unstructured":"D. Beyer, Verifiers and Validators of the 11th Intl. Competition on Software Verification (SV-COMP 2022). Zenodo, https:\/\/doi.org\/10.5281\/zenodo.5959149, 2022","DOI":"10.5281\/zenodo.5959149"}],"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_22","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,3,12]],"date-time":"2024-03-12T08:49:47Z","timestamp":1710233387000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-030-99527-0_22"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022]]},"ISBN":["9783030995263","9783030995270"],"references-count":11,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-99527-0_22","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)"}}]}}