{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,9]],"date-time":"2025-10-09T21:07:25Z","timestamp":1760044045140,"version":"3.40.3"},"publisher-location":"Cham","reference-count":78,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783030720124"},{"type":"electronic","value":"9783030720131"}],"license":[{"start":{"date-parts":[[2021,1,1]],"date-time":"2021-01-01T00:00:00Z","timestamp":1609459200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2021,3,23]],"date-time":"2021-03-23T00:00:00Z","timestamp":1616457600000},"content-version":"vor","delay-in-days":81,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2021]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>Tools that automatically prove the absence or detect the presence of large floating-point roundoff errors or the special values NaN and Infinity greatly help developers to reason about the unintuitive nature of floating-point arithmetic. We show that state-of-the-art tools, however, support or provide non-trivial results only for relatively short programs. We propose a framework for combining different static and dynamic analyses that allows to increase their reach beyond what they can do individually. Furthermore, we show how adaptations of existing dynamic and static techniques effectively trade some soundness guarantees for increased scalability, providing conditional verification of floating-point kernels in realistic programs.<\/jats:p>","DOI":"10.1007\/978-3-030-72013-1_3","type":"book-chapter","created":{"date-parts":[[2021,3,22]],"date-time":"2021-03-22T18:03:10Z","timestamp":1616436190000},"page":"43-63","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":3,"title":["A Two-Phase Approach for Conditional Floating-Point Verification"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-8639-4116","authenticated-orcid":false,"given":"Debasmita","family":"Lohar","sequence":"first","affiliation":[]},{"given":"Clothilde","family":"Jeangoudoux","sequence":"additional","affiliation":[]},{"given":"Joshua","family":"Sobel","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-6848-3163","authenticated-orcid":false,"given":"Eva","family":"Darulova","sequence":"additional","affiliation":[]},{"given":"Maria","family":"Christakis","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2021,3,23]]},"reference":[{"unstructured":"FBench: Trigonometry Intense Floating Point Benchmark. https:\/\/www.fourmilab.ch\/fbench\/fbench.html, Accessed: 2020-10-05","key":"3_CR1"},{"unstructured":"Inverted-pendulum Control Problem. http:\/\/www.toddsifleet.com\/projects\/inverted-pendulum, Accessed: 2020-10-05","key":"3_CR2"},{"unstructured":"LINPACK Benchmark. https:\/\/people.sc.fsu.edu\/~jburkardt\/c_src\/linpack_bench\/linpack_bench.html, Accessed: 2020-10-05","key":"3_CR3"},{"unstructured":"Molecular Dynamics. https:\/\/people.math.sc.edu\/Burkardt\/cpp_src\/md\/md.html, Accessed: 2020-10-05","key":"3_CR4"},{"unstructured":"N-body Problem. https:\/\/rosettacode.org\/wiki\/N-body_problem#C, Accessed: 2020-10-05","key":"3_CR5"},{"unstructured":"Ray-casting Algorithm. https:\/\/rosettacode.org\/wiki\/Ray-casting_algorithm#C, Accessed: 2020-10-05","key":"3_CR6"},{"unstructured":"Simulated Test of Reactor Shielding. https:\/\/people.math.sc.edu\/Burkardt\/cpp_src\/reactor_simulation\/reactor_simulation.html, Accessed: 2020-10-05","key":"3_CR7"},{"unstructured":"Project Sklearn-porter. https:\/\/github.com\/nok\/sklearn-porter (2018)","key":"3_CR8"},{"doi-asserted-by":"crossref","unstructured":"Barr, E.T., Vo, T., Le, V., Su, Z.: Automatic Detection of Floating-Point Exceptions. In: ACM Sigplan Notices. No.\u00a01, ACM (2013)","key":"3_CR9","DOI":"10.1145\/2480359.2429133"},{"doi-asserted-by":"crossref","unstructured":"Benz, F., Hildebrandt, A., Hack, S.: A Dynamic Program Analysis to Find Floating-Point Accuracy Problems. In: Programming Language Design and Implementation (PLDI) (2012)","key":"3_CR10","DOI":"10.1145\/2254064.2254118"},{"doi-asserted-by":"crossref","unstructured":"Blanchet, B., Cousot, P., Cousot, R., Feret, J., Mauborgne, L., Min\u00e9, A., Monniaux, D., Rival, X.: A Static Analyzer for Large Safety-Critical Software. In: Programming Language Design and Implementation (PLDI) (2003)","key":"3_CR11","DOI":"10.1145\/781131.781153"},{"doi-asserted-by":"crossref","unstructured":"B\u00f6hme, M., Pham, V., Nguyen, M., Roychoudhury, A.: Directed Greybox Fuzzing. In: Computer and Communications Security (CCS) (2017)","key":"3_CR12","DOI":"10.1145\/3133956.3134020"},{"doi-asserted-by":"crossref","unstructured":"Boldo, S., Cl\u00e9ment, F., Filli\u00e2tre, J.C., Mayero, M., Melquiond, G., Weis, P.: Wave Equation Numerical Resolution: A Comprehensive Mechanized Proof of a C Program. Journal of Automated Reasoning 50(4) (2013)","key":"3_CR13","DOI":"10.1007\/s10817-012-9255-4"},{"doi-asserted-by":"crossref","unstructured":"Boldo, S., Filli\u00e2tre, J., Melquiond, G.: Combining Coq and Gappa for Certifying Floating-Point Programs. In: Intelligent Computer Mathematics (2009)","key":"3_CR14","DOI":"10.1007\/978-3-642-02614-0_10"},{"doi-asserted-by":"crossref","unstructured":"Boldo, S., Melquiond, G.: Flocq: A Unified Library for Proving Floating-Point Algorithms in Coq. In: Computer Arithmetic (ARITH) (2011)","key":"3_CR15","DOI":"10.1109\/ARITH.2011.40"},{"doi-asserted-by":"crossref","unstructured":"Brain, M., D\u2019Silva, V., Griggio, A., Haller, L., Kroening, D.: Deciding Floating-Point Logic with Abstract Conflict Driven Clause Learning. Formal Methods Syst. Des. 45(2) (2014)","key":"3_CR16","DOI":"10.1007\/s10703-013-0203-7"},{"doi-asserted-by":"crossref","unstructured":"Brain, M., Schanda, F., Sun, Y.: Building Better Bit-Blasting for Floating-Point Problems. In: Tools and Algorithms for the Construction and Analysis of Systems (TACAS) (2019)","key":"3_CR17","DOI":"10.1007\/978-3-030-17462-0_5"},{"doi-asserted-by":"crossref","unstructured":"Chen, H., Xue, Y., Li, Y., Chen, B., Xie, X., Wu, X., Liu, Y.: Hawkeye: Towards a Desired Directed Grey-box Fuzzer. In: Computer and Communications Security (CCS) (2018)","key":"3_CR18","DOI":"10.1145\/3243734.3243849"},{"doi-asserted-by":"crossref","unstructured":"Chen, L., Min\u00e9, A., Cousot, P.: A Sound Floating-Point Polyhedra Abstract Domain. In: Asian Symposium on Programming Languages and Systems (APLAS) (2008)","key":"3_CR19","DOI":"10.1007\/978-3-540-89330-1_2"},{"doi-asserted-by":"crossref","unstructured":"Chiang, W.F., Baranowski, M., Briggs, I., Solovyev, A., Gopalakrishnan, G., Rakamari\u0107, Z.: Rigorous Floating-point Mixed-precision Tuning. In: Principles of Programming Languages (POPL) (2017)","key":"3_CR20","DOI":"10.1145\/3009837.3009846"},{"doi-asserted-by":"crossref","unstructured":"Chiang, W., Gopalakrishnan, G., Rakamaric, Z., Solovyev, A.: Efficient Search for Inputs Causing High Floating-Point Errors. In: Symposium on Principles and Practice of Parallel Programming (PPoPP) (2014)","key":"3_CR21","DOI":"10.1145\/2555243.2555265"},{"unstructured":"Chowdhury, A.B., Medicherla, R.K., Venkatesh, R.: VeriFuzz: Program Aware Fuzzing\u2014(Competition Contribution). In: Tools and Algorithms for the Construction and Analysis of Systems (TACAS) (2019)","key":"3_CR22"},{"doi-asserted-by":"crossref","unstructured":"Christakis, M., M\u00fcller, P., W\u00fcstholz, V.: Guiding Dynamic Symbolic Execution Toward Unverified Program Executions. In: International Conference on Software Engineering (ICSE) (2016)","key":"3_CR23","DOI":"10.1145\/2884781.2884843"},{"unstructured":"Claude, M., Moy, Y.: The Jessie plugin for Deductive Verification in Frama-C, Tutorial and Reference Manual. INRIA Saclay-\u00cele-de-France & LRI, CNRS UMR 8623 (2018), http:\/\/krakatoa.lri.fr\/jessie.html","key":"3_CR24"},{"unstructured":"Correnson, L., Cuoq, P., Kirchner, F., Prevosto, V., Puccetti, A., Signoles, J., Yakobowski, B.: Frama-C User Manual (2011), http:\/\/frama-c.com\/\/support.html","key":"3_CR25"},{"doi-asserted-by":"crossref","unstructured":"Cousot, P., Cousot, R.: Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: Principles of Programming Languages (POPL) (1977)","key":"3_CR26","DOI":"10.1145\/512950.512973"},{"doi-asserted-by":"crossref","unstructured":"Csallner, C., Smaragdakis, Y.: Check \u2019n\u2019 Crash: Combining Static Checking and Testing. In: International Conference on Software Engineering (ICSE) (2005)","key":"3_CR27","DOI":"10.1145\/1062455.1062533"},{"doi-asserted-by":"crossref","unstructured":"Czech, M., Jakobs, M.C., Wehrheim, H.: Just Test What You Cannot Verify! In: Fundamental Approaches to Software Engineering (FASE) (2015)","key":"3_CR28","DOI":"10.1007\/978-3-662-46675-9_7"},{"doi-asserted-by":"crossref","unstructured":"Damouche, N., Martel, M., Panchekha, P., Qiu, J., Sanchez-Stern, A., Tatlock, Z.: Toward a Standard Benchmark Format and Suite for Floating-Point Analysis. In: NSV (2016)","key":"3_CR29","DOI":"10.1007\/978-3-319-54292-8_6"},{"doi-asserted-by":"crossref","unstructured":"Darulova, E., Izycheva, A., Nasir, F., Ritter, F., Becker, H., Bastian, R.: Daisy - Framework for Analysis and Optimization of Numerical Programs. In: Tools and Algorithms for the Construction and Analysis of Systems (TACAS) (2018)","key":"3_CR30","DOI":"10.1007\/978-3-319-89960-2_15"},{"doi-asserted-by":"crossref","unstructured":"Darulova, E., Kuncak, V.: Towards a Compiler for Reals. TOPLAS 39(2) (2017)","key":"3_CR31","DOI":"10.1145\/3014426"},{"doi-asserted-by":"crossref","unstructured":"Darulova, E., Horn, E., Sharma, S.: Sound Mixed-precision Optimization with Rewriting. In: International Conference on Cyber-Physical Systems (ICCPS) (2018)","key":"3_CR32","DOI":"10.1109\/ICCPS.2018.00028"},{"doi-asserted-by":"crossref","unstructured":"De\u00a0Dinechin, F., Lauter, C.Q., Melquiond, G.: Assisted Verification of Elementary Functions Using Gappa. In: ACM Symposium on Applied Computing (2006)","key":"3_CR33","DOI":"10.1145\/1141277.1141584"},{"doi-asserted-by":"crossref","unstructured":"Devecsery, D., Chen, P.M., Flinn, J., Narayanasamy, S.: Optimistic Hybrid Analysis: Accelerating Dynamic Analysis Through Predicated Static Analysis. In: Architectural Support for Programming Languages and Operating Systems (ASPLOS) (2018)","key":"3_CR34","DOI":"10.1145\/3173162.3177153"},{"doi-asserted-by":"crossref","unstructured":"Dwyer, M.B., Purandare, R.: Residual Dynamic Typestate Analysis Exploiting Static Analysis: Results to Reformulate and Reduce the Cost of Dynamic Analysis. In: ASE (2007)","key":"3_CR35","DOI":"10.1145\/1321631.1321651"},{"doi-asserted-by":"crossref","unstructured":"Ferles, K., W\u00fcstholz, V., Christakis, M., Dillig, I.: Failure-Directed Program Trimming. In: Foundations of Software Engineering (ESEC\/FSE) (2017)","key":"3_CR36","DOI":"10.1145\/3106237.3106249"},{"unstructured":"Fox, A., Harrison, J., Akbarpour, B.: A Formal Model of IEEE Floating Point Arithmetic. HOL4 Theorem Prover Library (2017)","key":"3_CR37"},{"doi-asserted-by":"crossref","unstructured":"Fu, Z., Su, Z.: Effective Floating-Point Analysis via Weak-Distance Minimization. In: Programming Language Design and Implementation (PLDI) (2019)","key":"3_CR38","DOI":"10.1145\/3314221.3314632"},{"doi-asserted-by":"crossref","unstructured":"Ganesh, V., Leek, T., Rinard, M.C.: Taint-Based Directed Whitebox Fuzzing. In: International Conference on Software Engineering (ICSE) (2009)","key":"3_CR39","DOI":"10.1109\/ICSE.2009.5070546"},{"doi-asserted-by":"crossref","unstructured":"Ge, X., Taneja, K., Xie, T., Tillmann, N.: DyTa: Dynamic Symbolic Execution Guided with Static Verification Results. In: International Conference on Software Engineering (ICSE) (2011)","key":"3_CR40","DOI":"10.1145\/1985793.1985971"},{"doi-asserted-by":"crossref","unstructured":"Godefroid, P., Nori, A.V., Rajamani, S.K., Tetali, S.: Compositional May-Must Program Analysis: Unleashing the Power of Alternation. In: Principles of Programming Languages (POPL) (2010)","key":"3_CR41","DOI":"10.1145\/1706299.1706307"},{"doi-asserted-by":"crossref","unstructured":"Goldberg, D.: What Every Computer Scientist Should Know About Floating-point Arithmetic. ACM Comput. Surv. 23(1) (1991)","key":"3_CR42","DOI":"10.1145\/103162.103163"},{"doi-asserted-by":"crossref","unstructured":"Goubault, E., Putot, S.: Static Analysis of Finite Precision Computations. In: Verification, Model Checking, and Abstract Interpretation (VMCAI) (2011)","key":"3_CR43","DOI":"10.1007\/978-3-642-18275-4_17"},{"doi-asserted-by":"crossref","unstructured":"Guo, H., Rubio-Gonz\u00e1lez, C.: Efficient Generation of Error-Inducing Floating-Point Inputs via Symbolic Execution. In: International Conference on Software Engineering (ICSE) (2020)","key":"3_CR44","DOI":"10.1145\/3377811.3380359"},{"unstructured":"Haller, I., Slowinska, A., Neugschwandtner, M., Bos, H.: Dowsing for Overflows: A Guided Fuzzer to Find Buffer Boundary Violations. In: Security (2013)","key":"3_CR45"},{"unstructured":"Harrison, J.: Floating Point Verification in HOL Light: The Exponential Function. Formal Methods in System Design 16(3) (2000)","key":"3_CR46"},{"doi-asserted-by":"crossref","unstructured":"Hatton, L., Roberts, A.: How Accurate is Scientific Software? IEEE Trans. Softw. Eng. 20 (1994)","key":"3_CR47","DOI":"10.1109\/32.328993"},{"unstructured":"IEEE, C.S.: IEEE Standard for Floating-Point Arithmetic. IEEE Std 754-2008 (2008)","key":"3_CR48"},{"doi-asserted-by":"crossref","unstructured":"Jacobsen, C., Solovyev, A., Gopalakrishnan, G.: A Parameterized Floating-Point Formalizaton in HOL Light. Electronic Notes in Theoretical Computer Science 317 (2015)","key":"3_CR49","DOI":"10.1016\/j.entcs.2015.10.010"},{"doi-asserted-by":"crossref","unstructured":"Jeannet, B., Min\u00e9, A.: Apron: A Library of Numerical Abstract Domains for Static Analysis. In: Computer Aided Verification (CAV) (2009)","key":"3_CR50","DOI":"10.1007\/978-3-642-02658-4_52"},{"unstructured":"Karlin, I., Bhatele, A., Chamberlain, B.L., Cohen, J., Devito, Z., Gokhale, M., Haque, R., Hornung, R., Keasler, J., Laney, D., Luke, E., Lloyd, S., McGraw, J., Neely, R., Richards, D., Schulz, M., Still, C.H., Wang, F., Wong, D.: LULESH Programming Model and Performance Ports Overview. Tech. Rep. LLNL-TR-608824 (2012)","key":"3_CR51"},{"doi-asserted-by":"crossref","unstructured":"Kroening, D., Tautschnig, M.: CBMC\u2013C bounded model checker. In: Tools and Algorithms for the Construction and Analysis of Systems (TACAS). Springer (2014)","key":"3_CR52","DOI":"10.1007\/978-3-642-54862-8_26"},{"unstructured":"Leino, K.R.M.: This is Boogie 2 (2008), https:\/\/www.microsoft.com\/en-us\/research\/publication\/this-is-boogie-2-2\/","key":"3_CR53"},{"doi-asserted-by":"crossref","unstructured":"Lemieux, C., Sen, K.: FairFuzz: A Targeted Mutation Strategy for Increasing Greybox Fuzz Testing Coverage. In: Automated Software Engineering (ASE) (2018)","key":"3_CR54","DOI":"10.1145\/3238147.3238176"},{"doi-asserted-by":"crossref","unstructured":"Li, Y., Chen, B., Chandramohan, M., Lin, S., Liu, Y., Tiu, A.: Steelix: Program-State Based Binary Fuzzing. In: Foundations of Software Engineering (ESEC\/FSE) (2017)","key":"3_CR55","DOI":"10.1145\/3106237.3106295"},{"unstructured":"Li, Y., Ji, S., Lv, C., Chen, Y., Chen, J., Gu, Q., Wu, C.: V-Fuzz: Vulnerability-Oriented Evolutionary Fuzzing. CoRR abs\/1901.01142 (2019)","key":"3_CR56"},{"doi-asserted-by":"crossref","unstructured":"Liew, D., Schemmel, D., Cadar, C., Donaldson, A.F., Z\u00e4hl, R., Wehrle, K.: Floating-Point Symbolic Execution: A Case Study in N-Version Programming. In: Automated Software Engineering (ASE) (2017)","key":"3_CR57","DOI":"10.1109\/ASE.2017.8115670"},{"doi-asserted-by":"crossref","unstructured":"Ma, K.K., Khoo, Y.P., Foster, J.S., Hicks, M.: Directed Symbolic Execution. In: Static Analysis Symposium (SAS) (2011)","key":"3_CR58","DOI":"10.1007\/978-3-642-23702-7_11"},{"doi-asserted-by":"crossref","unstructured":"Ma, L., Artho, C., Zhang, C., Sato, H., Gmeiner, J., Ramler, R.: GRT: Program-Analysis-Guided Random Testing. In: Automated Software Engineering (ASE) (2015)","key":"3_CR59","DOI":"10.1109\/ASE.2015.49"},{"doi-asserted-by":"crossref","unstructured":"Magron, V., Constantinides, G., Donaldson, A.: Certified Roundoff Error Bounds Using Semidefinite Programming. ACM Trans. Math. Softw. 43(4) (2017)","key":"3_CR60","DOI":"10.1145\/3015465"},{"doi-asserted-by":"crossref","unstructured":"Mahmoud, A., Venkatagiri, R., Ahmed, K., Misailovic, S., Marinov, D., Fletcher, C.W., Adve, S.V.: Minotaur: Adapting Software Testing Techniques for Hardware Errors. In: Architectural Support for Programming Languages and Operating Systems (ASPLOS) (2019)","key":"3_CR61","DOI":"10.1145\/3297858.3304050"},{"doi-asserted-by":"crossref","unstructured":"Marinescu, P.D., Cadar, C.: KATCH: High-Coverage Testing of Software Patches. In: Foundations of Software Engineering (ESEC\/FSE) (2013)","key":"3_CR62","DOI":"10.1145\/2491411.2491438"},{"unstructured":"Min\u00e9, A., Mauborgne, L., Rival, X., Feret, J., Cousot, P., K\u00e4stner, D., Wilhelm, S., Ferdinand, C.: Taking Static Analysis to the Next Level: Proving the Absence of Run-Time Errors and Data Races with Astr\u00e9e. In: Embedded Real Time Software and Systems (ERTS) (2016)","key":"3_CR63"},{"doi-asserted-by":"crossref","unstructured":"Moore, R.E., Kearfott, R.B., Cloud, M.J.: Introduction to Interval Analysis. Society for Industrial and Applied Mathematics (2009)","key":"3_CR64","DOI":"10.1137\/1.9780898717716"},{"doi-asserted-by":"crossref","unstructured":"Moscato, M., Titolo, L., Dutle, A., Mu\u00f1oz, C.: Automatic Estimation of Verified Floating-Point Round-Off Errors via Static Analysis. In: SAFECOMP (2017)","key":"3_CR65","DOI":"10.1007\/978-3-319-66266-4_14"},{"doi-asserted-by":"crossref","unstructured":"Nori, A.V., Rajamani, S.K., Tetali, S., Thakur, A.V.: The YOGI Project: Software Property Checking via Static Analysis and Testing. In: Tools and Algorithms for the Construction and Analysis of Systems (TACAS) (2009)","key":"3_CR66","DOI":"10.1007\/978-3-642-00768-2_17"},{"doi-asserted-by":"crossref","unstructured":"Panchekha, P., Sanchez-Stern, A., Wilcox, J.R., Tatlock, Z.: Automatically Improving Accuracy for Floating Point Expressions. In: Programming Language Design and Implementation (PLDI) (2015)","key":"3_CR67","DOI":"10.1145\/2737924.2737959"},{"doi-asserted-by":"crossref","unstructured":"Rubio-Gonz\u00e1lez, C., Nguyen, C., Nguyen, H.D., Demmel, J., Kahan, W., Sen, K., Bailey, D.H., Iancu, C., Hough, D.: Precimonious: Tuning Assistant for Floating-point Precision. In: High Performance Computing, Networking, Storage and Analysis (SC) (2013)","key":"3_CR68","DOI":"10.1145\/2503210.2503296"},{"doi-asserted-by":"crossref","unstructured":"Sanchez-Stern, A., Panchekha, P., Lerner, S., Tatlock, Z.: Finding Root Causes of Floating Point Error. In: Programming Language Design and Implementation (PLDI) (2018)","key":"3_CR69","DOI":"10.1145\/3192366.3192411"},{"doi-asserted-by":"crossref","unstructured":"Schkufza, E., Sharma, R., Aiken, A.: Stochastic Optimization of Floating-Point Programs with Tunable Precision. In: Programming Language Design and Implementation (PLDI) (2014)","key":"3_CR70","DOI":"10.1145\/2594291.2594302"},{"doi-asserted-by":"crossref","unstructured":"Singh, G., P\u00fcschel, M., Vechev, M.T.: Fast polyhedra abstract domain. In: Principles of Programming Languages (POPL) (2017)","key":"3_CR71","DOI":"10.1145\/3009837.3009885"},{"doi-asserted-by":"crossref","unstructured":"Solovyev, A., Jacobsen, C., Rakamaric, Z., Gopalakrishnan, G.: Rigorous Estimation of Floating-Point Round-off Errors with Symbolic Taylor Expansions. In: Formal Methods (FM) (2015)","key":"3_CR72","DOI":"10.1007\/978-3-319-19249-9_33"},{"doi-asserted-by":"crossref","unstructured":"Wang, M., Liang, J., Chen, Y., Jiang, Y., Jiao, X., Liu, H., Zhao, X., Sun, J.: SAFL: Increasing and Accelerating Testing Coverage with Symbolic Execution and Guided Fuzzing. In: International Conference on Software Engineering: Companion (ICSE Companion) (2018)","key":"3_CR73","DOI":"10.1145\/3183440.3183494"},{"doi-asserted-by":"crossref","unstructured":"Wang, X., Wang, H., Su, Z., Tang, E., Chen, X., Shen, W., Chen, Z., Wang, L., Zhang, X., Li, X.: Global Optimization of Numerical Programs via Prioritized Stochastic Algebraic Transformations. In: International Conference on Software Engineering (ICSE) (2019)","key":"3_CR74","DOI":"10.1109\/ICSE.2019.00116"},{"doi-asserted-by":"crossref","unstructured":"W\u00fcstholz, V., Christakis, M.: Targeted Greybox Fuzzing with Static Lookahead Analysis. In: International Conference on Software Engineering (ICSE) (2020), to appear.","key":"3_CR75","DOI":"10.1145\/3377811.3380388"},{"doi-asserted-by":"crossref","unstructured":"Yi, X., Chen, L., Mao, X., Ji, T.: Efficient Automated Repair of High Floating-Point Errors in Numerical Libraries. Proceedings of the ACM on Programming Languages 3(POPL) (2019)","key":"3_CR76","DOI":"10.1145\/3290369"},{"doi-asserted-by":"crossref","unstructured":"Zou, D., Wang, R., Xiong, Y., Zhang, L., Su, Z., Mei, H.: A Genetic Algorithm for Detecting Significant Floating-Point Inaccuracies. In: International Conference on Software Engineering (ICSE) (2015)","key":"3_CR77","DOI":"10.1109\/ICSE.2015.70"},{"doi-asserted-by":"crossref","unstructured":"Zou, D., Zeng, M., Xiong, Y., Fu, Z., Zhang, L., Su, Z.: Detecting Floating-Point Errors via Atomic Conditions. PACMPL 4(POPL) (2020)","key":"3_CR78","DOI":"10.1145\/3371128"}],"container-title":["Lecture Notes in Computer Science","Tools and Algorithms for the Construction and Analysis of Systems"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-72013-1_3","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,3,22]],"date-time":"2021-03-22T18:11:44Z","timestamp":1616436704000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-030-72013-1_3"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021]]},"ISBN":["9783030720124","9783030720131"],"references-count":78,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-72013-1_3","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2021]]},"assertion":[{"value":"23 March 2021","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":"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":"2021","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"27 March 2021","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"1 April 2021","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":"tacas2021","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/etaps.org\/2021\/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":"141","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":"41","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":"21","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":"12","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 changed to an online format due to the COVID-19 pandemic","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)"}}]}}