{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,26]],"date-time":"2025-03-26T04:58:18Z","timestamp":1742965098444,"version":"3.40.3"},"publisher-location":"Cham","reference-count":70,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783030816841"},{"type":"electronic","value":"9783030816858"}],"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,7,15]],"date-time":"2021-07-15T00:00:00Z","timestamp":1626307200000},"content-version":"vor","delay-in-days":195,"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>State-of-the-art program-analysis techniques are not yet able to effectively verify safety properties of heterogeneous systems, that is, systems with components implemented using diverse technologies. This shortcoming is pinpointed by programs invoking neural networks despite their acclaimed role as innovation drivers across many application areas. In this paper, we embark on the verification of system-level properties for systems characterized by interaction between programs and neural networks. Our technique provides a tight two-way integration of a program and a neural-network analysis and is formalized in a general framework based on abstract interpretation. We evaluate its effectiveness on 26 variants of a widely used, restricted autonomous-driving benchmark.<\/jats:p>","DOI":"10.1007\/978-3-030-81685-8_9","type":"book-chapter","created":{"date-parts":[[2021,7,17]],"date-time":"2021-07-17T00:02:35Z","timestamp":1626480155000},"page":"201-224","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":9,"title":["Automated Safety Verification of Programs Invoking Neural Networks"],"prefix":"10.1007","author":[{"given":"Maria","family":"Christakis","sequence":"first","affiliation":[]},{"given":"Hasan Ferit","family":"Eniser","sequence":"additional","affiliation":[]},{"given":"Holger","family":"Hermanns","sequence":"additional","affiliation":[]},{"given":"J\u00f6rg","family":"Hoffmann","sequence":"additional","affiliation":[]},{"given":"Yugesh","family":"Kothari","sequence":"additional","affiliation":[]},{"given":"Jianlin","family":"Li","sequence":"additional","affiliation":[]},{"given":"Jorge A.","family":"Navas","sequence":"additional","affiliation":[]},{"given":"Valentin","family":"W\u00fcstholz","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2021,7,15]]},"reference":[{"key":"9_CR1","doi-asserted-by":"crossref","unstructured":"Albarghouthi, A., Li, Y., Gurfinkel, A., Chechik, M.: UFO: A framework for abstraction- and interpolation-based software verification. In: CAV. LNCS, vol. 7358, pp. 672\u2013678. Springer (2012)","DOI":"10.1007\/978-3-642-31424-7_48"},{"key":"9_CR2","doi-asserted-by":"crossref","unstructured":"Alshiekh, M., Bloem, R., Ehlers, R., K\u00f6nighofer, B., Niekum, S., Topcu, U.: Safe reinforcement learning via shielding. In: AAAI. pp. 2669\u20132678. AAAI (2018)","DOI":"10.1609\/aaai.v32i1.11797"},{"key":"9_CR3","doi-asserted-by":"crossref","unstructured":"Babaev, D., Savchenko, M., Tuzhilin, A., Umerenkov, D.: E.T.-RNN: Applying deep learning to credit loan applications. In: KDD. pp. 2183\u20142190. ACM (2019)","DOI":"10.1145\/3292500.3330693"},{"key":"9_CR4","doi-asserted-by":"crossref","unstructured":"Baier, C., Christakis, M., Gros, T.P., Gro\u00df, D., Gumhold, S., Hermanns, H., Hoffmann, J., Klauck, M.: Lab conditions for research on explainable automated decisions. In: TAILOR. LNCS, vol. 12641, pp. 83\u201390. Springer (2020)","DOI":"10.1007\/978-3-030-73959-1_8"},{"key":"9_CR5","doi-asserted-by":"crossref","unstructured":"Barto, A.G., Bradtke, S.J., Singh, S.P.: Learning to act using real-time dynamic programming. Artif. Intell. 72, 81\u2013138 (1995)","DOI":"10.1016\/0004-3702(94)00011-O"},{"key":"9_CR6","unstructured":"Beyer, D., Chlipala, A.J., Majumdar, R.: Generating tests from counterexamples. In: ICSE. pp. 326\u2013335. IEEE Computer Society (2004)"},{"key":"9_CR7","doi-asserted-by":"crossref","unstructured":"Beyer, D., Henzinger, T.A., Keremoglu, M.E., Wendler, P.: Conditional model checking: A technique to pass information between verifiers. In: FSE. pp. 57\u201367. ACM (2012)","DOI":"10.1145\/2393596.2393664"},{"key":"9_CR8","doi-asserted-by":"crossref","unstructured":"Biere, A., Cimatti, A., Clarke, E.M., Zhu, Y.: Symbolic model checking without BDDs. In: TACAS. LNCS, vol. 1579, pp. 193\u2013207. Springer (1999)","DOI":"10.1007\/3-540-49059-0_14"},{"key":"9_CR9","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: PLDI. pp. 196\u2013207. ACM (2003)","DOI":"10.1145\/780822.781153"},{"key":"9_CR10","doi-asserted-by":"crossref","unstructured":"Cadar, C., Engler, D.R.: Execution generated test cases: How to make systems code crash itself. In: SPIN. LNCS, vol. 3639, pp. 2\u201323. Springer (2005)","DOI":"10.1007\/11537328_2"},{"key":"9_CR11","doi-asserted-by":"crossref","unstructured":"Calcagno, C., Distefano, D., Dubreil, J., Gabi, D., Hooimeijer, P., Luca, M., O\u2019Hearn, P.W., Papakonstantinou, I., Purbrick, J., Rodriguez, D.: Moving fast with software verification. In: NFM. LNCS, vol. 9058, pp. 3\u201311. Springer (2015)","DOI":"10.1007\/978-3-319-17524-9_1"},{"key":"9_CR12","unstructured":"Carlini, N., Wagner, D.A.: Defensive distillation is not robust to adversarial examples. CoRR abs\/1607.04311 (2016)"},{"key":"9_CR13","doi-asserted-by":"crossref","unstructured":"Christakis, M., M\u00fcller, P., W\u00fcstholz, V.: Collaborative verification and testing with explicit assumptions. In: FM. LNCS, vol. 7436, pp. 132\u2013146. Springer (2012)","DOI":"10.1007\/978-3-642-32759-9_13"},{"key":"9_CR14","doi-asserted-by":"crossref","unstructured":"Christakis, M., M\u00fcller, P., W\u00fcstholz, V.: Guiding dynamic symbolic execution toward unverified program executions. In: ICSE. pp. 144\u2013155. ACM (2016)","DOI":"10.1145\/2884781.2884843"},{"key":"9_CR15","doi-asserted-by":"crossref","unstructured":"Clarke, E.M., Biere, A., Raimi, R., Zhu, Y.: Bounded model checking using satisfiability solving. FMSD 19, 7\u201334 (2001)","DOI":"10.1023\/A:1011276507260"},{"key":"9_CR16","unstructured":"Cobbe, K., Hesse, C., Hilton, J., Schulman, J.: Leveraging procedural generation to benchmark reinforcement learning. In: ICML. PMLR, vol. 119, pp. 2048\u20132056. PMLR (2020)"},{"key":"9_CR17","doi-asserted-by":"crossref","unstructured":"Cousot, P., Cousot, R.: Static determination of dynamic properties of programs. In: ISOP. pp. 106\u2013130. Dunod (1976)","DOI":"10.1145\/800022.808314"},{"key":"9_CR18","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: POPL. pp. 238\u2013252. ACM (1977)","DOI":"10.1145\/512950.512973"},{"key":"9_CR19","doi-asserted-by":"crossref","unstructured":"Cousot, P., Halbwachs, N.: Automatic discovery of linear restraints among variables of a program. In: POPL. pp. 84\u201396. ACM (1978)","DOI":"10.1145\/512760.512770"},{"key":"9_CR20","doi-asserted-by":"crossref","unstructured":"Csallner, C., Smaragdakis, Y.: Check \u2019n\u2019 Crash: Combining static checking and testing. In: ICSE. pp. 422\u2013431. ACM (2005)","DOI":"10.1145\/1062455.1062533"},{"key":"9_CR21","doi-asserted-by":"crossref","unstructured":"Csallner, C., Smaragdakis, Y., Xie, T.: DSD-Crasher: A hybrid analysis tool for bug finding. TOSEM 17, 1\u201337 (2008)","DOI":"10.1145\/1348250.1348254"},{"key":"9_CR22","doi-asserted-by":"crossref","unstructured":"Czech, M., Jakobs, M.C., Wehrheim, H.: Just test what you cannot verify! In: FASE. LNCS, vol. 9033, pp. 100\u2013114. Springer (2015)","DOI":"10.1007\/978-3-662-46675-9_7"},{"key":"9_CR23","doi-asserted-by":"crossref","unstructured":"Dreossi, T., Donz\u00e9, A., Seshia, S.A.: Compositional falsification of cyber-physical systems with machine learning components. In: NFM. LNCS, vol. 10227, pp. 357\u2013372. Springer (2017)","DOI":"10.1007\/978-3-319-57288-8_26"},{"key":"9_CR24","doi-asserted-by":"crossref","unstructured":"Dutta, S., Chen, X., Sankaranarayanan, S.: Reachability analysis for neural feedback systems using regressive polynomial rule inference. In: HSCC. pp. 157\u2013168. ACM (2019)","DOI":"10.1145\/3302504.3311807"},{"key":"9_CR25","doi-asserted-by":"crossref","unstructured":"Dutta, S., Jha, S., Sankaranarayanan, S., Tiwari, A.: Learning and verification of feedback control systems using feedforward neural networks. In: ADHS. IFAC-PapersOnLine, vol. 51, pp. 151\u2013156. Elsevier (2018)","DOI":"10.1016\/j.ifacol.2018.08.026"},{"key":"9_CR26","doi-asserted-by":"crossref","unstructured":"F\u00e4hndrich, M., Logozzo, F.: Static contract checking with abstract interpretation. In: FoVeOOS. LNCS, vol. 6528, pp. 10\u201330. Springer (2010)","DOI":"10.1007\/978-3-642-18070-5_2"},{"key":"9_CR27","doi-asserted-by":"crossref","unstructured":"Gehr, T., Mirman, M., Drachsler-Cohen, D., Tsankov, P., Chaudhuri, S., Vechev, M.T.: AI2: Safety and robustness certification of neural networks with abstract interpretation. In: S&P. pp. 3\u201318. IEEE Computer Society (2018)","DOI":"10.1109\/SP.2018.00058"},{"key":"9_CR28","doi-asserted-by":"crossref","unstructured":"Ghorbal, K., Goubault, E., Putot, S.: The Zonotope abstract domain Taylor1+. In: CAV. LNCS, vol. 5643, pp. 627\u2013633. Springer (2009)","DOI":"10.1007\/978-3-642-02658-4_47"},{"key":"9_CR29","doi-asserted-by":"crossref","unstructured":"Godefroid, P., Klarlund, N., Sen, K.: DART: Directed automated random testing. In: PLDI. pp. 213\u2013223. ACM (2005)","DOI":"10.1145\/1064978.1065036"},{"key":"9_CR30","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: POPL. pp. 43\u201356. ACM (2010)","DOI":"10.1145\/1707801.1706307"},{"key":"9_CR31","unstructured":"Goodfellow, I.J., Shlens, J., Szegedy, C.: Explaining and harnessing adversarial examples. In: ICLR (2015)"},{"key":"9_CR32","doi-asserted-by":"crossref","unstructured":"Gros, T.P., Hermanns, H., Hoffmann, J., Klauck, M., Steinmetz, M.: Deep statistical model checking. In: FORTE. LNCS, vol. 12136, p. 12136. Springer (2020)","DOI":"10.1007\/978-3-030-50086-3_6"},{"key":"9_CR33","doi-asserted-by":"crossref","unstructured":"Gurfinkel, A., Chaki, S.: Boxes: A symbolic abstract domain of boxes. In: SAS. LNCS, vol. 6337, pp. 287\u2013303. Springer (2010)","DOI":"10.1007\/978-3-642-15769-1_18"},{"key":"9_CR34","doi-asserted-by":"crossref","unstructured":"Gurfinkel, A., Kahsai, T., Komuravelli, A., Navas, J.A.: The SeaHorn verification framework. In: CAV. LNCS, vol. 9206, pp. 343\u2013361. Springer (2015)","DOI":"10.1007\/978-3-319-21690-4_20"},{"key":"9_CR35","doi-asserted-by":"crossref","unstructured":"Horn, R.A., Johnson, C.R.: Matrix Analysis. Cambridge University Press (2012)","DOI":"10.1017\/CBO9781139020411"},{"key":"9_CR36","doi-asserted-by":"crossref","unstructured":"Huang, X., Kwiatkowska, M., Wang, S., Wu, M.: Safety verification of deep neural networks. In: CAV. LNCS, vol. 10426, pp. 3\u201329. Springer (2017)","DOI":"10.1007\/978-3-319-63387-9_1"},{"key":"9_CR37","doi-asserted-by":"crossref","unstructured":"Katz, G., Barrett, C.W., Dill, D.L., Julian, K., Kochenderfer, M.J.: Reluplex: An efficient SMT solver for verifying deep neural networks. In: CAV. LNCS, vol. 10426, pp. 97\u2013117. Springer (2017)","DOI":"10.1007\/978-3-319-63387-9_5"},{"key":"9_CR38","doi-asserted-by":"crossref","unstructured":"Katz, G., Huang, D.A., Ibeling, D., Julian, K., Lazarus, C., Lim, R., Shah, P., Thakoor, S., Wu, H., Zeljic, A., Dill, D.L., Kochenderfer, M.J., Barrett, C.W.: The Marabou framework for verification and analysis of deep neural networks. In: CAV. LNCS, vol. 11561, pp. 443\u2013452. Springer (2019)","DOI":"10.1007\/978-3-030-25540-4_26"},{"key":"9_CR39","doi-asserted-by":"crossref","unstructured":"Kazak, Y., Barrett, C.W., Katz, G., Schapira, M.: Verifying deep-RL-driven systems. In: NetAI@SIGCOMM. pp. 83\u201389. ACM (2019)","DOI":"10.1145\/3341216.3342218"},{"key":"9_CR40","doi-asserted-by":"crossref","unstructured":"Larus, J., Hankin, C., Carson, S.G., Christen, M., Crafa, S., Grau, O., Kirchner, C., Knowles, B., McGettrick, A., Tamburri, D.A., Werthner, H.: When computers decide: European recommendations on machine-learned automated decision making. Tech. rep. (2018)","DOI":"10.1145\/3185595"},{"key":"9_CR41","doi-asserted-by":"crossref","unstructured":"Li, J., Liu, J., Yang, P., Chen, L., Huang, X., Zhang, L.: Analyzing deep neural networks with symbolic propagation: Towards higher precision and faster verification. In: SAS. LNCS, vol. 11822, pp. 296\u2013319. Springer (2019)","DOI":"10.1007\/978-3-030-32304-2_15"},{"key":"9_CR42","unstructured":"Lomuscio, A., Maganti, L.: An approach to reachability analysis for feed-forward ReLU neural networks. CoRR abs\/1706.07351 (2017)"},{"key":"9_CR43","doi-asserted-by":"crossref","unstructured":"Luo, H., Yang, Y., Tong, B., Wu, F., Fan, B.: Traffic sign recognition using a multi-task convolutional neural network. Trans. Intell. Transp. Syst. 19, 1100\u20131111 (2018)","DOI":"10.1109\/TITS.2017.2714691"},{"key":"9_CR44","unstructured":"Madry, A., Makelov, A., Schmidt, L., Tsipras, D., Vladu, A.: Towards deep learning models resistant to adversarial attacks. In: ICLR. OpenReview.net (2018)"},{"key":"9_CR45","doi-asserted-by":"crossref","unstructured":"Majumdar, R., Sen, K.: Hybrid concolic testing. In: ICSE. pp. 416\u2013426. IEEE Computer Society (2007)","DOI":"10.1109\/ICSE.2007.41"},{"key":"9_CR46","unstructured":"McMahan, H.B., Gordon, G.J.: Fast exact planning in Markov decision processes. In: ICAPS. pp. 151\u2013160. AAAI (2005)"},{"key":"9_CR47","unstructured":"Mnih, V., Kavukcuoglu, K., Silver, D., Graves, A., Antonoglou, I., Wierstra, D., Riedmiller, M.A.: Playing Atari with deep reinforcement learning. CoRR abs\/1312.5602 (2013)"},{"key":"9_CR48","doi-asserted-by":"crossref","unstructured":"Nassi, B., Mirsky, Y., Nassi, D., Ben-Netanel, R., Drokin, O., Elovici, Y.: Phantom of the ADAS: Securing advanced driver-assistance systems from split-second phantom attacks. In: CCS. pp. 293\u2013308. ACM (2020)","DOI":"10.1145\/3372297.3423359"},{"key":"9_CR49","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: TACAS. LNCS, vol. 5505, pp. 178\u2013181. Springer (2009)","DOI":"10.1007\/978-3-642-00768-2_17"},{"key":"9_CR50","doi-asserted-by":"crossref","unstructured":"Papernot, N., McDaniel, P.D., Jha, S., Fredrikson, M., Celik, Z.B., Swami, A.: The limitations of deep learning in adversarial settings. In: EuroS&P. pp. 372\u2013387. IEEE Computer Society (2016)","DOI":"10.1109\/EuroSP.2016.36"},{"key":"9_CR51","doi-asserted-by":"crossref","unstructured":"Pham, T., Tran, T., Phung, D.Q., Venkatesh, S.: Predicting healthcare trajectories from medical records: A deep learning approach. J. Biomed. Informatics 69, 218\u2013229 (2017)","DOI":"10.1016\/j.jbi.2017.04.001"},{"key":"9_CR52","unstructured":"Pineda, L.E., Lu, Y., Zilberstein, S., Goldman, C.V.: Fault-tolerant planning under uncertainty. In: IJCAI. pp. 2350\u20132356. IJCAI\/AAAI (2013)"},{"key":"9_CR53","doi-asserted-by":"crossref","unstructured":"Pineda, L.E., Zilberstein, S.: Planning under uncertainty using reduced models: Revisiting determinization. In: ICAPS. pp. 217\u2013225. AAAI (2014)","DOI":"10.1609\/icaps.v24i1.13636"},{"key":"9_CR54","doi-asserted-by":"crossref","unstructured":"Ruan, W., Huang, X., Kwiatkowska, M.: Reachability analysis of deep neural networks with provable guarantees. In: IJCAI. pp. 2651\u20132659. ijcai.org (2018)","DOI":"10.24963\/ijcai.2018\/368"},{"key":"9_CR55","unstructured":"Schulman, J., Wolski, F., Dhariwal, P., Radford, A., Klimov, O.: Proximal policy optimization algorithms. CoRR abs\/1707.06347 (2017)"},{"key":"9_CR56","unstructured":"Singh, G., Gehr, T., Mirman, M., P\u00fcschel, M., Vechev, M.T.: Fast and effective robustness certification. In: NeurIPS. pp. 10825\u201310836 (2018)"},{"key":"9_CR57","doi-asserted-by":"crossref","unstructured":"Singh, G., Gehr, T., P\u00fcschel, M., Vechev, M.T.: An abstract domain for certifying neural networks. PACMPL 3, 41:1\u201341:30 (2019)","DOI":"10.1145\/3290354"},{"key":"9_CR58","doi-asserted-by":"crossref","unstructured":"Stephens, N., Grosen, J., Salls, C., Dutcher, A., Wang, R., Corbetta, J., Shoshitaishvili, Y., Kruegel, C., Vigna, G.: Driller: Augmenting fuzzing through selective symbolic execution. In: NDSS. The Internet Society (2016)","DOI":"10.14722\/ndss.2016.23368"},{"key":"9_CR59","doi-asserted-by":"crossref","unstructured":"Sun, X., Khedr, H., Shoukry, Y.: Formal verification of neural network controlled autonomous systems. In: HSCC. pp. 147\u2013156. ACM (2019)","DOI":"10.1145\/3302504.3311802"},{"key":"9_CR60","unstructured":"Sutton, R.S., Barto, A.G.: Reinforcement Learning: An Introduction. MIT Press (2018)"},{"key":"9_CR61","doi-asserted-by":"crossref","unstructured":"Toman, J., Grossman, D.: CONCERTO: A framework for combined concrete and abstract interpretation. PACMPL 3(POPL), 43:1\u201343:29 (2019)","DOI":"10.1145\/3290356"},{"key":"9_CR62","doi-asserted-by":"crossref","unstructured":"Tuncali, C.E., Fainekos, G., Ito, H., Kapinski, J.: Simulation-based adversarial test generation for autonomous vehicles with machine learning components. In: IV. pp. 1555\u20131562. IEEE Computer Society (2018)","DOI":"10.1109\/IVS.2018.8500421"},{"key":"9_CR63","doi-asserted-by":"crossref","unstructured":"Urban, C., Christakis, M., W\u00fcstholz, V., Zhang, F.: Perfectly parallel fairness certification of neural networks. PACMPL 4, 185:1\u2013185:30 (2020)","DOI":"10.1145\/3428253"},{"key":"9_CR64","unstructured":"Wang, S., Pei, K., Whitehouse, J., Yang, J., Jana, S.: Efficient formal safety analysis of neural networks. In: NeurIPS. pp. 6369\u20136379 (2018)"},{"key":"9_CR65","unstructured":"Wang, S., Pei, K., Whitehouse, J., Yang, J., Jana, S.: Formal security analysis of neural networks using symbolic intervals. In: Security. pp. 1599\u20131614. USENIX (2018)"},{"key":"9_CR66","doi-asserted-by":"crossref","unstructured":"Wicker, M., Huang, X., Kwiatkowska, M.: Feature-guided black-box safety testing of deep neural networks. In: TACAS. LNCS, vol. 10805, pp. 408\u2013426. Springer (2018)","DOI":"10.1007\/978-3-319-89960-2_22"},{"key":"9_CR67","doi-asserted-by":"crossref","unstructured":"Xiang, W., Tran, H., Johnson, T.T.: Output reachable set estimation and verification for multilayer neural networks. TNNLS 29, 5777\u20135783 (2018)","DOI":"10.1109\/TNNLS.2018.2808470"},{"key":"9_CR68","doi-asserted-by":"crossref","unstructured":"Xiang, W., Tran, H., Rosenfeld, J.A., Johnson, T.T.: Reachable set estimation and safety verification for piecewise linear systems with neural network controllers. In: ACC. pp. 1574\u20131579. IEEE Computer Society (2018)","DOI":"10.23919\/ACC.2018.8431048"},{"key":"9_CR69","unstructured":"Yun, I., Lee, S., Xu, M., Jang, Y., Kim, T.: QSYM: A practical concolic execution engine tailored for hybrid fuzzing. In: Security. pp. 745\u2013761. USENIX (2018)"},{"key":"9_CR70","doi-asserted-by":"crossref","unstructured":"Zhang, Z., Ernst, G., Sedwards, S., Arcaini, P., Hasuo, I.: Two-layered falsification of hybrid systems guided by monte carlo tree search. Trans. Comput. Aided Des. Integr. Circuits Syst. 37, 2894\u20132905 (2018)","DOI":"10.1109\/TCAD.2018.2858463"}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-81685-8_9","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,1,4]],"date-time":"2023-01-04T18:43:54Z","timestamp":1672857834000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-030-81685-8_9"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021]]},"ISBN":["9783030816841","9783030816858"],"references-count":70,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-81685-8_9","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":"15 July 2021","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"CAV","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Computer Aided Verification","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2021","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"20 July 2021","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"23 July 2021","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"33","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"cav2021","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"http:\/\/i-cav.org\/2021\/","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":"290","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":"63","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":"22% - 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":"16 tool papers and 5 invited papers are also included.","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)"}}]}}