{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,27]],"date-time":"2025-03-27T14:50:13Z","timestamp":1743087013269,"version":"3.40.3"},"publisher-location":"Cham","reference-count":18,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783030994280"},{"type":"electronic","value":"9783030994297"}],"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,29]],"date-time":"2022-03-29T00:00:00Z","timestamp":1648512000000},"content-version":"vor","delay-in-days":87,"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>Finding semantic bugs in code is difficult and requires precious expert time. Lacking comprehensive formal specifications, deductive verification is not an option. We propose an incremental specification procedure: With the help of automatic verification tools, a domain expert is guided through program runs and source code locations. The expert validates a run at certain locations and creates lightweight annotations. Formal methods training is not required. We demonstrate by example that this approach is capable to quickly detect different kinds of semantic bugs. We position our approach in the middle ground between fully-fledged deductive verification and bug finding without semantic guidance.<\/jats:p>","DOI":"10.1007\/978-3-030-99429-7_8","type":"book-chapter","created":{"date-parts":[[2022,3,28]],"date-time":"2022-03-28T20:02:48Z","timestamp":1648497768000},"page":"145-154","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["Finding Semantic Bugs Fast"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-9716-3142","authenticated-orcid":false,"given":"Lukas","family":"Gr\u00e4tz","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-8000-7613","authenticated-orcid":false,"given":"Reiner","family":"H\u00e4hnle","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Richard","family":"Bubel","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2022,3,29]]},"reference":[{"key":"8_CR1","doi-asserted-by":"publisher","unstructured":"Ayewah, N., Hovemeyer, D., Morgenthaler, J.D., Penix, J., Pugh, W.: Using static analysis to find bugs. IEEE Software 25(5), 22\u201329 (2008). https:\/\/doi.org\/10.1109\/MS.2008.130","DOI":"10.1109\/MS.2008.130"},{"key":"8_CR2","doi-asserted-by":"publisher","unstructured":"Baumann, C., Beckert, B., Blasum, H., Bormer, T.: Lessons learned from microkernel verification \u2013 specification is the new bottleneck. In: Cassez, F., Huuck, R., Klein, G., Schlich, B. (eds.) Proc. 7th Conf. on Systems Software Verification. EPTCS, vol.\u00a0102, pp. 18\u201332 (2012). https:\/\/doi.org\/10.4204\/EPTCS.102.4","DOI":"10.4204\/EPTCS.102.4"},{"key":"8_CR3","doi-asserted-by":"publisher","unstructured":"Beyer, D., Keremoglu, M.E.: CPAchecker: A tool for configurable software verification. In: Gopalakrishnan, G., Qadeer, S. (eds.) Computer Aided Verification, 23rd Intl. Conf., Snowbird, UT, USA. LNCS, vol.\u00a06806, pp. 184\u2013190. Springer (2011). https:\/\/doi.org\/10.1007\/978-3-642-22110-1_16","DOI":"10.1007\/978-3-642-22110-1_16"},{"key":"8_CR4","doi-asserted-by":"publisher","unstructured":"Christakis, M., M\u00fcller, P., W\u00fcstholz, V.: Collaborative verification and testing with explicit assumptions. In: Giannakopoulou, D., M\u00e9ry, D. (eds.) Formal Methods, 18th Intl. Symp., Paris, France. LNCS, vol.\u00a07436, pp. 132\u2013146. Springer (2012). https:\/\/doi.org\/10.1007\/978-3-642-32759-9_13","DOI":"10.1007\/978-3-642-32759-9_13"},{"key":"8_CR5","doi-asserted-by":"publisher","unstructured":"Christakis, M., M\u00fcller, P., W\u00fcstholz, V.: Guiding dynamic symbolic execution toward unverified program executions. In: Dillon, L.K., Visser, W., Williams, L.A. (eds.) Proc. 38th Intl. Conf. on Software Engineering, Austin, TX, USA. pp. 144\u2013155. ACM (2016). https:\/\/doi.org\/10.1145\/2884781.2884843","DOI":"10.1145\/2884781.2884843"},{"key":"8_CR6","doi-asserted-by":"publisher","unstructured":"Fagan, M.E.: Design and code inspections to reduce errors in program development. IBM Systems Journal 15(3), 182\u2013211 (1976). https:\/\/doi.org\/10.1147\/sj.153.0182","DOI":"10.1147\/sj.153.0182"},{"key":"8_CR7","doi-asserted-by":"publisher","unstructured":"Godefroid, P.: Test generation using symbolic execution. In: D\u2019Souza, D., Kavitha, T., Radhakrishnan, J. (eds.) IARCS Ann. Conf. on Foundations of Software Technology and Theoretical Computer Science, Hyderabad, India. LIPIcs, vol.\u00a018, pp. 24\u201333. Dagstuhl (2012). https:\/\/doi.org\/10.4230\/LIPIcs.FSTTCS.2012.24","DOI":"10.4230\/LIPIcs.FSTTCS.2012.24"},{"key":"8_CR8","doi-asserted-by":"publisher","unstructured":"Gr\u00e4tz, L., H\u00e4hnle, R., Bubel, R.: Examples for FASE NIER paper \u201cfinding semantics bugs fast\u201d (artifact). In: 25th Intl. Conf. on Fundamental Approaches to Software Engineering, Munich, Germany. Zenodo (2022). https:\/\/doi.org\/10.5281\/zenodo.5806351","DOI":"10.5281\/zenodo.5806351"},{"key":"8_CR9","doi-asserted-by":"publisher","unstructured":"H\u00e4hnle, R., Huisman, M.: Deductive verification: from pen-and-paper proofs to industrial tools. In: Steffen, B., Woeginger, G. (eds.) Computing and Software Science: State of the Art and Perspectives, LNCS, vol. 10000, pp. 345\u2013373. Springer (2019). https:\/\/doi.org\/10.1007\/978-3-319-91908-9_18","DOI":"10.1007\/978-3-319-91908-9_18"},{"key":"8_CR10","doi-asserted-by":"publisher","unstructured":"Hentschel, M., H\u00e4hnle, R., Bubel, R.: Can formal methods improve the efficiency of code reviews? In: \u00c1brah\u00e1m, E., Huisman, M. (eds.) Integrated Formal Methods, 12th Intl. Conf., Reykjavik, Iceland. LNCS, vol.\u00a09681, pp. 3\u201319. Springer (2016). https:\/\/doi.org\/10.1007\/978-3-319-33693-0_1","DOI":"10.1007\/978-3-319-33693-0_1"},{"key":"8_CR11","unstructured":"The Independent Breast Screening Review 2018, House of Commons, HC, vol.\u00a01799. UK Department of Health and Social Care (Dec 2018), https:\/\/www.gov.uk\/government\/publications\/independent-breast-screening-review-report"},{"key":"8_CR12","unstructured":"Leavens, G.T., Poll, E., Clifton, C., Cheon, Y., Ruby, C., Cok, D., M\u00fcller, P., Kiniry, J., Chalin, P., Zimmerman, D.M., Dietl, W.: JML reference manual (2013), revision: 2344."},{"key":"8_CR13","doi-asserted-by":"publisher","unstructured":"Meyer, B.: Applying \u201cdesign by contract\u201d. Computer 25(10), 40\u201351 (1992). https:\/\/doi.org\/10.1109\/2.161279","DOI":"10.1109\/2.161279"},{"key":"8_CR14","doi-asserted-by":"publisher","unstructured":"Stucki, L.G., Foshee, G.L.: New assertion concepts for self-metric software validation. In: Proc. Intl. Conf. on Reliable Software, Los Angeles, California, USA. p. 59\u201371. Association for Computing Machinery (1975). https:\/\/doi.org\/10.1145\/800027.808425","DOI":"10.1145\/800027.808425"},{"key":"8_CR15","doi-asserted-by":"publisher","unstructured":"Tan, L., Liu, C., Li, Z., Wang, X., Zhou, Y., Zhai, C.: Bug characteristics in open source software. Empirical Software Engineering 19(6), 1665\u20131705 (2014). https:\/\/doi.org\/10.1007\/s10664-013-9258-8","DOI":"10.1007\/s10664-013-9258-8"},{"key":"8_CR16","doi-asserted-by":"publisher","unstructured":"Wang, Q., Brun, Y., Orso, A.: Behavioral execution comparison: Are tests representative of field behavior? In: Intl. Conf. on Software Testing, Verification and Validation, Tokyo, Japan. pp. 321\u2013332. IEEE Computer Society (2017). https:\/\/doi.org\/10.1109\/ICST.2017.36","DOI":"10.1109\/ICST.2017.36"},{"key":"8_CR17","doi-asserted-by":"publisher","unstructured":"Wang, Q., Orso, A.: Improving testing by mimicking user behavior. In: Intl. Conf. on Software Maintenance and Evolution, Adelaide, Australia. pp. 488\u2013498. IEEE (2020). https:\/\/doi.org\/10.1109\/ICSME46990.2020.00053","DOI":"10.1109\/ICSME46990.2020.00053"},{"key":"8_CR18","doi-asserted-by":"crossref","unstructured":"Zeller, A.: Why Programs Fail: A Guide to Systematic Debugging. Elsevier, second edn. (2009)","DOI":"10.1016\/B978-0-12-374515-6.00006-X"}],"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-030-99429-7_8","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,3,28]],"date-time":"2022-03-28T20:20:25Z","timestamp":1648498825000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-030-99429-7_8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022]]},"ISBN":["9783030994280","9783030994297"],"references-count":18,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-99429-7_8","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2022]]},"assertion":[{"value":"29 March 2022","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":"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":"4 April 2022","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"5 April 2022","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"25","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"fase2022","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/etaps.org\/2022\/fase","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Double-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":"61","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":"17","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":"0","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":"28% - 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":"7","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)"}}]}}