{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,17]],"date-time":"2026-07-17T22:43:34Z","timestamp":1784328214354,"version":"3.55.0"},"publisher-location":"Cham","reference-count":57,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783030720124","type":"print"},{"value":"9783030720131","type":"electronic"}],"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>Deep learning has emerged as an effective approach for creating modern software systems, with neural networks often surpassing hand-crafted systems. Unfortunately, neural networks are known to suffer from various safety and security issues. Formal verification is a promising avenue for tackling this difficulty, by formally certifying that networks are correct. We propose an SMT-based technique for verifying<jats:italic>binarized neural networks<\/jats:italic>\u2014 a popular kind of neural network, where some weights have been binarized in order to render the neural network more memory and energy efficient, and quicker to evaluate. One novelty of our technique is that it allows the verification of neural networks that include both binarized and non-binarized components. Neural network verification is computationally very difficult, and so we propose here various optimizations, integrated into our SMT procedure as deduction steps, as well as an approach for parallelizing verification queries. We implement our technique as an extension to the Marabou framework, and use it to evaluate the approach on popular binarized neural network architectures.<\/jats:p>","DOI":"10.1007\/978-3-030-72013-1_11","type":"book-chapter","created":{"date-parts":[[2021,3,22]],"date-time":"2021-03-22T18:03:10Z","timestamp":1616436190000},"page":"203-222","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":36,"title":["An SMT-Based Approach for Verifying Binarized Neural Networks"],"prefix":"10.1007","author":[{"given":"Guy","family":"Amir","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Haoze","family":"Wu","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Clark","family":"Barrett","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Guy","family":"Katz","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2021,3,23]]},"reference":[{"key":"11_CR1","unstructured":"Artifact repository. https:\/\/github.com\/guyam2\/BNN_Verification_Artifact."},{"key":"11_CR2","unstructured":"Marabou repository. https:\/\/github.com\/NeuralNetworkVerification\/Marabou."},{"key":"11_CR3","doi-asserted-by":"crossref","unstructured":"P.\u00a0Ashok, V.\u00a0Hashemi, J.\u00a0Kretinsky, and S.\u00a0M\u00fchlberger. DeepAbstract: Neural Network Abstraction for Accelerating Verification. In Proc. 18th Int. Symposium on Automated Technology for Verification and Analysis (ATVA), 2020.","DOI":"10.1007\/978-3-030-59152-6_5"},{"key":"11_CR4","doi-asserted-by":"crossref","unstructured":"P.\u00a0Bacchus, R.\u00a0Stewart, and E.\u00a0Komendantskaya. Accuracy, Training Time and Hardware Efficiency Trade-Offs for Quantized Neural Networks on FPGAs. In Proc. 16th Int. Symposium on Applied Reconfigurable Computing (ARC), pages 121\u2013135, 2020.","DOI":"10.1007\/978-3-030-44534-8_10"},{"key":"11_CR5","doi-asserted-by":"crossref","unstructured":"C.\u00a0Barrett and C.\u00a0Tinelli. Satisfiability modulo theories. Springer, 2018.","DOI":"10.1007\/978-3-319-10575-8_11"},{"key":"11_CR6","unstructured":"O.\u00a0Bastani, Y.\u00a0Ioannou, L.\u00a0Lampropoulos, D.\u00a0Vytiniotis, A.\u00a0Nori, and A.\u00a0Criminisi. Measuring Neural Net Robustness with Constraints. In Proc. 30th Conf. on Neural Information Processing Systems (NIPS), 2016."},{"key":"11_CR7","unstructured":"M. Bojarski, D. Del Testa, D. Dworakowski, B. Firner, B. Flepp, P. Goyal, L. Jackel, M. Monfort, U. Muller, J. Zhang, X. Zhang, J. Zhao, and K. Zieba. End to End Learning for Self-Driving Cars, 2016. Technical Report. http:\/\/arxiv.org\/abs\/1604.07316."},{"key":"11_CR8","unstructured":"R.\u00a0Bunel, I.\u00a0Turkaslan, P.\u00a0Torr, P.\u00a0Kohli, and P.\u00a0Mudigonda. A Unified View of Piecewise Linear Neural Network Verification. In Proc. 32nd Conf. on Neural Information Processing Systems (NeurIPS), pages 4795\u20134804, 2018."},{"key":"11_CR9","unstructured":"N. Carlini, G. Katz, C. Barrett, and D. Dill. Provably Minimally-Distorted Adversarial Examples, 2017. Technical Report. https:\/\/arxiv.org\/abs\/1709.10207."},{"key":"11_CR10","unstructured":"H. Chen, L. Zhuo, B. Zhang, X. Zheng, J. Liu, R. Ji, D. D., and G. Guo. Binarized Neural Architecture Search for Efficient Object Recognition, 2020. Technical Report. http:\/\/arxiv.org\/abs\/2009.04247."},{"key":"11_CR11","unstructured":"C.-H. Cheng, G. N\u00fchrenberg, C.-H. Huang, and H. Ruess. Verification of Binarized Neural Networks via Inter-Neuron Factoring, 2017. Technical Report. http:\/\/arxiv.org\/abs\/1710.03107."},{"key":"11_CR12","doi-asserted-by":"crossref","unstructured":"D.\u00a0Ciregan, U.\u00a0Meier, and J.\u00a0Schmidhuber. Multi-Column Deep Neural Networks for Image Classification. In Proc. IEEE Conf. on Computer Vision and Pattern Recognition (CVPR), pages 3642\u20133649, 2012.","DOI":"10.1109\/CVPR.2012.6248110"},{"key":"11_CR13","doi-asserted-by":"crossref","unstructured":"G.\u00a0Dantzig. Linear Programming and Extensions. Princeton University Press, 1963.","DOI":"10.7249\/R366"},{"key":"11_CR14","doi-asserted-by":"crossref","unstructured":"R.\u00a0Ehlers. Formal Verification of Piece-Wise Linear Feed-Forward Neural Networks. In Proc. 15th Int. Symp. on Automated Technology for Verification and Analysis (ATVA), pages 269\u2013286, 2017.","DOI":"10.1007\/978-3-319-68167-2_19"},{"key":"11_CR15","doi-asserted-by":"crossref","unstructured":"Y.\u00a0Elboher, J.\u00a0Gottschlich, and G.\u00a0Katz. An Abstraction-Based Framework for Neural Network Verification. In Proc. 32nd Int. Conf. on Computer Aided Verification (CAV), pages 43\u201365, 2020.","DOI":"10.1007\/978-3-030-53288-8_3"},{"key":"11_CR16","doi-asserted-by":"crossref","unstructured":"T.\u00a0Gehr, M.\u00a0Mirman, D.\u00a0Drachsler-Cohen, E.\u00a0Tsankov, S.\u00a0Chaudhuri, and M.\u00a0Vechev. AI2: Safety and Robustness Certification of Neural Networks with Abstract Interpretation. In Proc. 39th IEEE Symposium on Security and Privacy (S&P), 2018.","DOI":"10.1109\/SP.2018.00058"},{"key":"11_CR17","unstructured":"L.\u00a0Geiger and P.\u00a0Team. Larq: An Open-Source Library for Training Binarized Neural Networks. Journal of Open Source Software, 5(45):1746, 2020."},{"key":"11_CR18","doi-asserted-by":"crossref","unstructured":"M.\u00a0Giacobbe, T.\u00a0Henzinger, and M.\u00a0Lechner. How Many Bits Does it Take to Quantize Your Neural Network? In Proc. 26th Int. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), pages 79\u201397, 2020.","DOI":"10.1007\/978-3-030-45237-7_5"},{"key":"11_CR19","doi-asserted-by":"crossref","unstructured":"S.\u00a0Gokulanathan, A.\u00a0Feldsher, A.\u00a0Malca, C.\u00a0Barrett, and G.\u00a0Katz. Simplifying Neural Networks using Formal Verification. In Proc. 12th NASA Formal Methods Symposium (NFM), pages 85\u201393, 2020.","DOI":"10.1007\/978-3-030-55754-6_5"},{"key":"11_CR20","unstructured":"B.\u00a0Goldberger, Y.\u00a0Adi, J.\u00a0Keshet, and G.\u00a0Katz. Minimal Modifications of Deep Neural Networks using Verification. In Proc. 23rd Int. Conf. on Logic for Programming, Artificial Intelligence and Reasoning (LPAR), pages 260\u2013278, 2020."},{"key":"11_CR21","unstructured":"I.\u00a0Goodfellow, Y.\u00a0Bengio, A.\u00a0Courville, and Y.\u00a0Bengio. Deep learning, volume\u00a01. MIT press Cambridge, 2016."},{"key":"11_CR22","doi-asserted-by":"crossref","unstructured":"D.\u00a0Gopinath, G.\u00a0Katz, C.\u00a0P\u01ces\u01cereanu, and C.\u00a0Barrett. DeepSafe: A Data-driven Approach for Assessing Robustness of Neural Networks. In Proc. 16th. Int. Symposium on on Automated Technology for Verification and Analysis (ATVA), pages 3\u201319, 2018.","DOI":"10.1007\/978-3-030-01090-4_1"},{"key":"11_CR23","unstructured":"S.\u00a0Han, H.\u00a0Mao, and W.\u00a0Dally. Deep Compression: Compressing Deep Neural Networks with Pruning, Trained Quantization and Huffman Coding. In Proc. 4th Int. Conf. on Learning Representations (ICLR), 2016."},{"key":"11_CR24","unstructured":"T.\u00a0Henzinger, M.\u00a0Lechner, and D.\u00a0Zikelic. Scalable Verification of Quantized Neural Networks (Technical Report), 2020. Technical Report. https:\/\/arxiv.org\/abs\/2012.08185."},{"key":"11_CR25","doi-asserted-by":"crossref","unstructured":"X.\u00a0Huang, M.\u00a0Kwiatkowska, S.\u00a0Wang, and M.\u00a0Wu. Safety Verification of Deep Neural Networks. In Proc. 29th Int. Conf. on Computer Aided Verification (CAV), pages 3\u201329, 2017.","DOI":"10.1007\/978-3-319-63387-9_1"},{"key":"11_CR26","unstructured":"I.\u00a0Hubara, M.\u00a0Courbariaux, D.\u00a0Soudry, R.\u00a0El-Yaniv, and Y.\u00a0Bengio. Binarized Neural Networks. In Proc. 30th Conf. on Neural Information Processing Systems (NIPS), pages 4107\u20134115, 2016."},{"key":"11_CR27","unstructured":"I.\u00a0Hubara, M.\u00a0Courbariaux, D.\u00a0Soudry, R.\u00a0El-Yaniv, and Y.\u00a0Bengio. Quantized Neural Networks: Training Neural Networks with Low Precision Weights and Activations. The Journal of Machine Learning Research, 18(1):6869\u20136898, 2017."},{"key":"11_CR28","doi-asserted-by":"crossref","unstructured":"Y.\u00a0Jacoby, C.\u00a0Barrett, and G.\u00a0Katz. Verifying Recurrent Neural Networks using Invariant Inference. In Proc. 18th Int. Symposium on Automated Technology for Verification and Analysis (ATVA), 2020.","DOI":"10.1007\/978-3-030-59152-6_3"},{"key":"11_CR29","unstructured":"K. Jia and M. Rinard. Efficient Exact Verification of Binarized Neural Networks, 2020. Technical Report. http:\/\/arxiv.org\/abs\/2005.03597."},{"key":"11_CR30","doi-asserted-by":"crossref","unstructured":"K.\u00a0Julian, J.\u00a0Lopez, J.\u00a0Brush, M.\u00a0Owen, and M.\u00a0Kochenderfer. Policy Compression for Aircraft Collision Avoidance Systems. In Proc. 35th Digital Avionics Systems Conf. (DASC), pages 1\u201310, 2016.","DOI":"10.1109\/DASC.2016.7778091"},{"key":"11_CR31","doi-asserted-by":"crossref","unstructured":"G.\u00a0Katz, C.\u00a0Barrett, D.\u00a0Dill, K.\u00a0Julian, and M.\u00a0Kochenderfer. Reluplex: An Efficient SMT Solver for Verifying Deep Neural Networks. In Proc. 29th Int. Conf. on Computer Aided Verification (CAV), pages 97\u2013117, 2017.","DOI":"10.1007\/978-3-319-63387-9_5"},{"key":"11_CR32","doi-asserted-by":"crossref","unstructured":"G.\u00a0Katz, C.\u00a0Barrett, D.\u00a0Dill, K.\u00a0Julian, and M.\u00a0Kochenderfer. Towards Proving the Adversarial Robustness of Deep Neural Networks. In Proc. 1st Workshop on Formal Verification of Autonomous Vehicles (FVAV), pages 19\u201326, 2017.","DOI":"10.4204\/EPTCS.257.3"},{"key":"11_CR33","doi-asserted-by":"crossref","unstructured":"G. Katz, C. Barrett, D. Dill, K. Julian, and M. Kochenderfer. Reluplex: a Calculus for Reasoning about Deep Neural Networks, 2021. Submitted, preprint avaialble upon request.","DOI":"10.1007\/s10703-021-00363-7"},{"key":"11_CR34","doi-asserted-by":"crossref","unstructured":"G.\u00a0Katz, D.\u00a0Huang, D.\u00a0Ibeling, K.\u00a0Julian, C.\u00a0Lazarus, R.\u00a0Lim, P.\u00a0Shah, S.\u00a0Thakoor, H.\u00a0Wu, A.\u00a0Zelji\u0107, D.\u00a0Dill, M.\u00a0Kochenderfer, and C.\u00a0Barrett. The Marabou Framework for Verification and Analysis of Deep Neural Networks. In Proc. 31st Int. Conf. on Computer Aided Verification (CAV), pages 443\u2013452, 2019.","DOI":"10.1007\/978-3-030-25540-4_26"},{"key":"11_CR35","doi-asserted-by":"crossref","unstructured":"Y.\u00a0Kazak, C.\u00a0Barrett, G.\u00a0Katz, and M.\u00a0Schapira. Verifying Deep-RL-Driven Systems. In Proc. 1st ACM SIGCOMM Workshop on Network Meets AI & ML (NetAI), pages 83\u201389, 2019.","DOI":"10.1145\/3341216.3342218"},{"key":"11_CR36","unstructured":"D. Kingma and J. Ba. Adam: a Method for Stochastic Optimization, 2014. Technical Report. http:\/\/arxiv.org\/abs\/1412.6980."},{"key":"11_CR37","unstructured":"A.\u00a0Krizhevsky, I.\u00a0Sutskever, and G.\u00a0Hinton. Imagenet Classification with Deep Convolutional Neural Networks. In Proc. 26th Conf. on Neural Information Processing Systems (NIPS), pages 1097\u20131105, 2012."},{"key":"11_CR38","unstructured":"L. Kuper, G. Katz, J. Gottschlich, K. Julian, C. Barrett, and M. Kochenderfer. Toward Scalable Verification for Safety-Critical Deep Networks, 2018. Technical Report. https:\/\/arxiv.org\/abs\/1801.05950."},{"key":"11_CR39","doi-asserted-by":"crossref","unstructured":"S.\u00a0Lai, L.\u00a0Xu, K.\u00a0Liu, and J.\u00a0Zhao. Recurrent Convolutional Neural Networks for Text Classification. In Proc. 29th AAAI Conf. on Artificial Intelligence, 2015.","DOI":"10.1609\/aaai.v29i1.9513"},{"key":"11_CR40","unstructured":"D.\u00a0Lin, S.\u00a0Talathi, and S.\u00a0Annapureddy. Fixed Point Quantization of Deep Convolutional Networks. In Proc. 33rd Int. Conf. on Machine Learning (ICML), pages 2849\u20132858, 2016."},{"key":"11_CR41","unstructured":"A. Lomuscio and L. Maganti. An Approach to Reachability Analysis for Feed-Forward ReLU Neural Networks, 2017. Technical Report. http:\/\/arxiv.org\/abs\/1706.07351."},{"key":"11_CR42","unstructured":"P. Molchanov, S. Tyree, T. Karras, T. Aila, and J. Kautz. Pruning Convolutional Neural Networks for Resource Efficient Inference, 2016. Technical Report. http:\/\/arxiv.org\/abs\/1611.06440."},{"key":"11_CR43","doi-asserted-by":"crossref","unstructured":"N. Narodytska, S. Kasiviswanathan, L. Ryzhyk, M. Sagiv, and T. Walsh. Verifying Properties of Binarized Deep Neural Networks, 2017. Technical Report. http:\/\/arxiv.org\/abs\/1709.06662.","DOI":"10.1609\/aaai.v32i1.12206"},{"key":"11_CR44","unstructured":"N.\u00a0Narodytska, H.\u00a0Zhang, A.\u00a0Gupta, and T.\u00a0Walsh. In Search for a SAT-friendly Binarized Neural Network Architecture. In Proc. 7th Int. Conf. on Learning Representations (ICLR), 2019."},{"key":"11_CR45","doi-asserted-by":"crossref","unstructured":"M.\u00a0Rastegari, V.\u00a0Ordonez, J.\u00a0Redmon, and A.\u00a0Farhadi. XNOR-Net: Imagenet Classification using Binary Convolutional Neural Networks. In Proc. 14th European Conf. on Computer Vision (ECCV), pages 525\u2013542, 2016.","DOI":"10.1007\/978-3-319-46493-0_32"},{"key":"11_CR46","unstructured":"K.\u00a0Simonyan and A.\u00a0Zisserman. Very Deep Convolutional Networks for Large-Scale Image Recognition. In Proc. 3rd Int. Conf. on Learning Representations (ICLR), 2015."},{"key":"11_CR47","doi-asserted-by":"crossref","unstructured":"C. Strong, H. Wu, A. Zelji\u0107, K. Julian, G. Katz, C. Barrett, and M. Kochenderfer. Global Optimization of Objective Functions Represented by ReLU networks, 2020. Technical Report. http:\/\/arxiv.org\/abs\/2010.03258.","DOI":"10.1007\/s10994-021-06050-2"},{"key":"11_CR48","unstructured":"C. Szegedy, W. Zaremba, I. Sutskever, J. Bruna, D. Erhan, I. Goodfellow, and R. Fergus. Intriguing Properties of Neural Networks, 2013. Technical Report. http:\/\/arxiv.org\/abs\/1312.6199."},{"key":"11_CR49","unstructured":"V.\u00a0Tjeng, K.\u00a0Xiao, and R.\u00a0Tedrake. Evaluating Robustness of Neural Networks with Mixed Integer Programming. In Proc. 7th Int. Conf. on Learning Representations (ICLR), 2019."},{"key":"11_CR50","doi-asserted-by":"crossref","unstructured":"H.\u00a0Tran, S.\u00a0Bak, and T.\u00a0Johnson. Verification of Deep Convolutional Neural Networks Using ImageStars. In Proc. 32nd Int. Conf. on Computer Aided Verification (CAV), pages 18\u201342, 2020.","DOI":"10.1007\/978-3-030-53288-8_2"},{"key":"11_CR51","unstructured":"S. Wang, K. Pei, J. Whitehouse, J. Yang, and S. Jana. Efficient Formal Safety Analysis of Neural Networks, 2018. Technical Report. https:\/\/arxiv.org\/abs\/1809.08098."},{"key":"11_CR52","unstructured":"S.\u00a0Wang, K.\u00a0Pei, J.\u00a0Whitehouse, J.\u00a0Yang, and S.\u00a0Jana. Formal Security Analysis of Neural Networks using Symbolic Intervals. In Proc. 27th USENIX Security Symposium, pages 1599\u20131614, 2018."},{"key":"11_CR53","unstructured":"T.-W. Weng, H. Zhang, H. Chen, Z. Song, C.-J. Hsieh, D. Boning, I. Dhillon, and L. Daniel. Towards Fast Computation of Certified Robustness for ReLU Networks, 2018. Technical Report. http:\/\/arxiv.org\/abs\/1804.09699."},{"key":"11_CR54","unstructured":"H.\u00a0Wu, A.\u00a0Ozdemir, A.\u00a0Zelji\u0107, A.\u00a0Irfan, K.\u00a0Julian, D.\u00a0Gopinath, S.\u00a0Fouladi, G.\u00a0Katz, C.\u00a0P\u0103s\u0103reanu, and C.\u00a0Barrett. Parallelization Techniques for Verifying Neural Networks. In Proc. 20th Int. Conf. on Formal Methods in Computer-Aided Design (FMCAD), pages 128\u2013137, 2020."},{"key":"11_CR55","unstructured":"H. Xiao, K. Rasul, and R. Vollgraf. Fashion-Mnist: a Novel Image Dataset for Benchmarking Machine Learning Algorithms, 2017. Technical Report. http:\/\/arxiv.org\/abs\/1708.07747."},{"key":"11_CR56","doi-asserted-by":"crossref","unstructured":"J.\u00a0Yang, X.\u00a0Shen, J.\u00a0Xing, X.\u00a0Tian, H.\u00a0Li, B.\u00a0Deng, J.\u00a0Huang, and X.-S. Hua. Quantization Networks. In Proc. IEEE Conf. on Computer Vision and Pattern Recognition (CVPR), pages 7308\u20137316, 2019.","DOI":"10.1109\/CVPR.2019.00748"},{"key":"11_CR57","doi-asserted-by":"crossref","unstructured":"Y. Zhou, S.-M. Moosavi-Dezfooli, N.-M. Cheung, and P. Frossard. Adaptive Quantization for Deep Neural Network, 2017. Technical Report. http:\/\/arxiv.org\/abs\/1712.01048.","DOI":"10.1609\/aaai.v32i1.11623"}],"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_11","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,12,22]],"date-time":"2022-12-22T04:47:52Z","timestamp":1671684472000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-030-72013-1_11"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021]]},"ISBN":["9783030720124","9783030720131"],"references-count":57,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-72013-1_11","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"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)"}}]}}