{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,27]],"date-time":"2025-03-27T02:45:24Z","timestamp":1743043524993,"version":"3.40.3"},"publisher-location":"Cham","reference-count":15,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783030452339"},{"type":"electronic","value":"9783030452346"}],"license":[{"start":{"date-parts":[[2020,1,1]],"date-time":"2020-01-01T00:00:00Z","timestamp":1577836800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2020]]},"DOI":"10.1007\/978-3-030-45234-6_27","type":"book-chapter","created":{"date-parts":[[2020,4,20]],"date-time":"2020-04-20T14:04:23Z","timestamp":1587391463000},"page":"525-529","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":7,"title":["ESBMC: Scalable and Precise Test Generation based on the Floating-Point Theory"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-6540-6587","authenticated-orcid":false,"given":"Mikhail R.","family":"Gadelha","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-6102-4343","authenticated-orcid":false,"given":"Rafael","family":"Menezes","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0001-9420-9056","authenticated-orcid":false,"given":"Felipe R.","family":"Monteiro","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-6235-4272","authenticated-orcid":false,"given":"Lucas C.","family":"Cordeiro","sequence":"additional","affiliation":[]},{"given":"Denis","family":"Nicole","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2020,4,17]]},"reference":[{"key":"27_CR1","doi-asserted-by":"crossref","unstructured":"Beyer, D.: Second competition on software testing: Test-comp 2020. In: Proc. FASE. LNCS, Springer (2020)","DOI":"10.1007\/978-3-030-45234-6_25"},{"key":"27_CR2","doi-asserted-by":"crossref","unstructured":"Clarke, E., Kroening, D., Lerda, F.: A tool for checking ANSI-C programs. In: Tools And Algorithms For The Construction And Analysis Of Systems. LNCS, vol.\u00a02988, pp. 168\u2013176 (2004)","DOI":"10.1007\/978-3-540-24730-2_15"},{"key":"27_CR3","doi-asserted-by":"crossref","unstructured":"Cordeiro, L.C., Fischer, B.: Verifying multi-threaded software using SMT-based context-bounded model checking. In: International Conference on Software Engineering. pp. 331\u2013340 (2011)","DOI":"10.1145\/1985793.1985839"},{"key":"27_CR4","unstructured":"Dutertre, B.: Yices 2.2. In: Computer-Aided Verification. LNCS, vol. 8559, pp. 737\u2013744 (2014)"},{"issue":"4","key":"27_CR5","doi-asserted-by":"publisher","first-page":"543","DOI":"10.1016\/S1571-0661(05)82542-3","volume":"89","author":"N E\u00e9n","year":"2003","unstructured":"E\u00e9n, N., S\u00f6rensson, N.: Temporal induction by incremental SAT solving. Electronic Notes in Theoretical Computer Science 89(4), 543\u2013560 (2003)","journal-title":"Electronic Notes in Theoretical Computer Science"},{"key":"27_CR6","unstructured":"Erkk, L.: Bug in floating-point conversions. \nhttps:\/\/github.com\/Z3Prover\/z3\/issues\/1564\n\n (2018), [Online; accessed January-2020]"},{"key":"27_CR7","doi-asserted-by":"crossref","unstructured":"Gadelha, M.R., Monteiro, F., Cordeiro, L., Nicole, D.: ESBMC v6.0: Verifying C programs using $$k$$-induction and invariant inference. In: Tools And Algorithms For The Construction And Analysis Of Systems. LNCS, vol. 11429, pp. 209\u2013213 (2019)","DOI":"10.1007\/978-3-030-17502-3_15"},{"key":"27_CR8","doi-asserted-by":"crossref","unstructured":"Gadelha, M.R., Monteiro, F.R., Morse, J., Cordeiro, L.C., Fischer, B., Nicole, D.A.: ESBMC 5.0: An industrial-strength C model checker. In: Automated Software Engineering. pp. 888\u2013891 (2018)","DOI":"10.1145\/3238147.3240481"},{"key":"27_CR9","doi-asserted-by":"crossref","unstructured":"Gadelha, M.Y.R., Cordeiro, L.C., Nicole, D.A.: Encoding floating-point numbers using the SMT theory in ESBMC: An empirical evaluation over the SV-COMP benchmarks. In: Simp\u00f3sio Brasileiro De M\u00e9todos Formais. LNCS, vol. 10623, pp. 91\u2013106 (2017)","DOI":"10.1007\/978-3-319-70848-5_7"},{"issue":"1","key":"27_CR10","doi-asserted-by":"publisher","first-page":"97","DOI":"10.1007\/s10009-015-0407-9","volume":"19","author":"MYR Gadelha","year":"2017","unstructured":"Gadelha, M.Y.R., Ismail, H.I., Cordeiro, L.C.: Handling loops in bounded model checking of C programs via $$k$$-induction. Software Tools for Technology Transfer 19(1), 97\u2013114 (2017)","journal-title":"Software Tools for Technology Transfer"},{"key":"27_CR11","unstructured":"IEEE: IEEE Standard For Floating-Point Arithmetic (2008), IEEE 754\u20132008"},{"key":"27_CR12","doi-asserted-by":"crossref","unstructured":"Muller, J.M., Brisebarre, N., Dinechin, F., Jeannerod, C.P., Lefe, V., Melquiond, G., Revol, N., Stehl., Torres, S.: Handbook of Floating-Point Arithmetic. Birkher Boston, 1st edn. (2010)","DOI":"10.1007\/978-0-8176-4705-6"},{"key":"27_CR13","doi-asserted-by":"crossref","unstructured":"Niemetz, A., Preiner, M., Biere, A.: Boolector 2.0 system description. Journal on Satisfiability, Boolean Modeling and Computation 9, 53\u201358 (2014)","DOI":"10.3233\/SAT190101"},{"key":"27_CR14","unstructured":"Noetzli, A.: Failing precondition when multiplying 4-bit significand\/4-bit exponent floats. \nhttps:\/\/github.com\/CVC4\/CVC4\/issues\/2182\n\n (2018), [Online; accessed January-2020]"},{"issue":"5","key":"27_CR15","doi-asserted-by":"publisher","first-page":"911","DOI":"10.1007\/s00165-017-0419-1","volume":"29","author":"P Schrammel","year":"2017","unstructured":"Schrammel, P., Kroening, D., Brain, M., Martins, R., Teige, T., Bienm\u00fcller, T.: Incremental bounded model checking for embedded software (extended version). Formal Aspects of Computing 29(5), 911\u2013931 (2017)","journal-title":"Formal Aspects of Computing"}],"container-title":["Lecture Notes in Computer Science","Fundamental Approaches to Software Engineering"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-45234-6_27","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,8,11]],"date-time":"2020-08-11T12:24:21Z","timestamp":1597148661000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-030-45234-6_27"}},"subtitle":["(Competition Contribution)"],"short-title":[],"issued":{"date-parts":[[2020]]},"ISBN":["9783030452339","9783030452346"],"references-count":15,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-45234-6_27","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2020]]},"assertion":[{"value":"17 April 2020","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":"Dublin","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Ireland","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2020","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"25 April 2020","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"30 April 2020","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"23","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"fase2020","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/www.etaps.org\/2020\/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":"81","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":"23","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":"9","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":"The conference could not take place due to the COVID-19 pandemic. There was an online event on July 2, 2020.","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)"}}]}}