{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T04:16:00Z","timestamp":1750220160323,"version":"3.41.0"},"publisher-location":"New York, NY, USA","reference-count":41,"publisher":"ACM","license":[{"start":{"date-parts":[[2022,9,20]],"date-time":"2022-09-20T00:00:00Z","timestamp":1663632000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2022,9,20]]},"DOI":"10.1145\/3551357.3551372","type":"proceedings-article","created":{"date-parts":[[2022,9,20]],"date-time":"2022-09-20T15:37:25Z","timestamp":1663688245000},"page":"1-14","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":3,"title":["CheckINN: Wide Range Neural Network Verification in Imandra"],"prefix":"10.1145","author":[{"given":"Remi","family":"Desmartin","sequence":"first","affiliation":[{"name":"Heriot-Watt University, United Kingdom"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Grant","family":"Passmore","sequence":"additional","affiliation":[{"name":"Imandra Inc., USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Ekaterina","family":"Komendantskaya","sequence":"additional","affiliation":[{"name":"Heriot-Watt University, United Kingdom"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Matthew","family":"Daggit","sequence":"additional","affiliation":[{"name":"Heriot-Watt University, United Kingdom"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2022,9,20]]},"reference":[{"key":"e_1_3_2_1_1_1","volume-title":"NFM 2020, Moffett Field, CA, USA, May 11-15, 2020, Proceedings(LNCS, Vol.\u00a012229)","author":"Ayers W.","year":"2020","unstructured":"Edward\u00a0 W. Ayers , Francisco Eiras , Majd Hawasly , and Iain Whiteside . 2020 . PaRoT: A Practical Framework for Robust Deep Neural Network Training. In NASA Formal Methods - 12th International Symposium , NFM 2020, Moffett Field, CA, USA, May 11-15, 2020, Proceedings(LNCS, Vol.\u00a012229) . Springer, 63\u201384. Edward\u00a0W. Ayers, Francisco Eiras, Majd Hawasly, and Iain Whiteside. 2020. PaRoT: A Practical Framework for Robust Deep Neural Network Training. In NASA Formal Methods - 12th International Symposium, NFM 2020, Moffett Field, CA, USA, May 11-15, 2020, Proceedings(LNCS, Vol.\u00a012229). Springer, 63\u201384."},{"doi-asserted-by":"crossref","unstructured":"A. Bagnall and G. Stewart. 2019. Certifying True Error: Machine Learning in Coq with Verified Generalisation Guarantees. AAAI (2019).  A. Bagnall and G. Stewart. 2019. Certifying True Error: Machine Learning in Coq with Verified Generalisation Guarantees. AAAI (2019).","key":"e_1_3_2_1_2_1","DOI":"10.1609\/aaai.v33i01.33012662"},{"unstructured":"R. Boyer and J. Moore. 1979. A Computational Logic. ACM Monograph Series. Academic Press New York.  R. Boyer and J. Moore. 1979. A Computational Logic. ACM Monograph Series. Academic Press New York.","key":"e_1_3_2_1_3_1"},{"key":"e_1_3_2_1_4_1","volume-title":"Boyer and J\u00a0Strother Moore","author":"S.","year":"1988","unstructured":"Robert\u00a0 S. Boyer and J\u00a0Strother Moore . 1988 . Integrating decision procedures into heuristic theorem provers: a case study of linear arithmetic. Machine intelligence(1988), 83\u2013124. Robert\u00a0S. Boyer and J\u00a0Strother Moore. 1988. Integrating decision procedures into heuristic theorem provers: a case study of linear arithmetic. Machine intelligence(1988), 83\u2013124."},{"volume-title":"Computer Aided Verification (CAV 2022)(Lecture Notes in Computer Science)","author":"Casadio Marco","unstructured":"Marco Casadio , Ekaterina Komendantskaya , Matthew\u00a0 L. Daggitt , Wen Kokke , Guy Katz , Guy Amir , and Idan Refaeli . 2022. Neural Network Robustness as a Verification Property: A Principled Case Study . In Computer Aided Verification (CAV 2022)(Lecture Notes in Computer Science) . Springer . Marco Casadio, Ekaterina Komendantskaya, Matthew\u00a0L. Daggitt, Wen Kokke, Guy Katz, Guy Amir, and Idan Refaeli. 2022. Neural Network Robustness as a Verification Property: A Principled Case Study. In Computer Aided Verification (CAV 2022)(Lecture Notes in Computer Science). Springer.","key":"e_1_3_2_1_5_1"},{"unstructured":"Fran\u00e7ois Chollet 2015. Keras. https:\/\/keras.io.  Fran\u00e7ois Chollet 2015. Keras. https:\/\/keras.io.","key":"e_1_3_2_1_6_1"},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_7_1","DOI":"10.1145\/351240.351266"},{"doi-asserted-by":"crossref","unstructured":"Leonardo de Moura and Grant\u00a0Olney Passmore. 2013. Computation in Real Closed Infinitesimal and Transcendental Extensions of the Rationals. In CADE.  Leonardo de Moura and Grant\u00a0Olney Passmore. 2013. Computation in Real Closed Infinitesimal and Transcendental Extensions of the Rationals. In CADE.","key":"e_1_3_2_1_8_1","DOI":"10.1007\/978-3-642-38574-2_12"},{"unstructured":"Remi Desmartin Grant Passmore Ekaterina Kmendantskaya and Matthew\u00a0L. Daggitt. 2022. CNN Library in Imandra. https:\/\/github.com\/aisec-private\/ImandraNN.  Remi Desmartin Grant Passmore Ekaterina Kmendantskaya and Matthew\u00a0L. Daggitt. 2022. CNN Library in Imandra. https:\/\/github.com\/aisec-private\/ImandraNN.","key":"e_1_3_2_1_9_1"},{"unstructured":"Remi Desmartin Grant Passmore and Ekaterina Komendantskaya. 2022. Neural Networks in Imandra: Matrix Representation as a Verification Choice. https:\/\/arxiv.org\/abs\/2205.09556.  Remi Desmartin Grant Passmore and Ekaterina Komendantskaya. 2022. Neural Networks in Imandra: Matrix Representation as a Verification Choice. https:\/\/arxiv.org\/abs\/2205.09556.","key":"e_1_3_2_1_10_1"},{"doi-asserted-by":"crossref","unstructured":"Remi Desmartin Grant Passmore Ekaterina Komendantskaya and Matthew Daggitt. 2022. CheckINN: Wide Range Neural Network Verification in Imandra (Extended). https:\/\/doi.org\/10.48550\/arXiv.2207.10562 arXiv:2207.10562 [cs]. 10.48550\/arXiv.2207.10562","key":"#cr-split#-e_1_3_2_1_11_1.1","DOI":"10.1145\/3551357.3551372"},{"doi-asserted-by":"crossref","unstructured":"Remi Desmartin Grant Passmore Ekaterina Komendantskaya and Matthew Daggitt. 2022. CheckINN: Wide Range Neural Network Verification in Imandra (Extended). https:\/\/doi.org\/10.48550\/arXiv.2207.10562 arXiv:2207.10562 [cs].","key":"#cr-split#-e_1_3_2_1_11_1.2","DOI":"10.1145\/3551357.3551372"},{"key":"e_1_3_2_1_12_1","volume-title":"Relative Robustness of Quantized Neural Networks Against Adversarial Attacks. In 2020 International Joint Conference on Neural Networks, IJCNN 2020","author":"Duncan Kirsty","year":"2020","unstructured":"Kirsty Duncan , Ekaterina Komendantskaya , Robert\u00a0 J. Stewart , and Michael\u00a0 A. Lones . 2020 . Relative Robustness of Quantized Neural Networks Against Adversarial Attacks. In 2020 International Joint Conference on Neural Networks, IJCNN 2020 , Glasgow, United Kingdom , July 19-24, 2020. 1\u20138. https:\/\/doi.org\/10.1109\/IJCNN48605.2020.9207596 10.1109\/IJCNN48605.2020.9207596 Kirsty Duncan, Ekaterina Komendantskaya, Robert\u00a0J. Stewart, and Michael\u00a0A. Lones. 2020. Relative Robustness of Quantized Neural Networks Against Adversarial Attacks. In 2020 International Joint Conference on Neural Networks, IJCNN 2020, Glasgow, United Kingdom, July 19-24, 2020. 1\u20138. https:\/\/doi.org\/10.1109\/IJCNN48605.2020.9207596"},{"volume-title":"Computer Aided Verification","author":"Dutertre Bruno","unstructured":"Bruno Dutertre and Leonardo de Moura . 2006. A Fast Linear-Arithmetic Solver for DPLL(T) . In Computer Aided Verification . Springer Berlin Heidelberg , 81\u201394. Bruno Dutertre and Leonardo de Moura. 2006. A Fast Linear-Arithmetic Solver for DPLL(T). In Computer Aided Verification. Springer Berlin Heidelberg, 81\u201394.","key":"e_1_3_2_1_13_1"},{"key":"e_1_3_2_1_14_1","volume-title":"Proceedings of the 36th International Conference on Machine Learning, ICML 2019","author":"Fischer Marc","year":"2019","unstructured":"Marc Fischer , Mislav Balunovic , Dana Drachsler-Cohen , Timon Gehr , Ce Zhang , and Martin\u00a0 T. Vechev . 2019 . DL2: Training and Querying Neural Networks with Logic . In Proceedings of the 36th International Conference on Machine Learning, ICML 2019 , 9-15 June 2019, Long Beach, California, USA(Proceedings of Machine Learning Research, Vol.\u00a097), Kamalika Chaudhuri and Ruslan Salakhutdinov (Eds.). PMLR , 1931\u20131941. http:\/\/proceedings.mlr.press\/v97\/fischer19a.html Marc Fischer, Mislav Balunovic, Dana Drachsler-Cohen, Timon Gehr, Ce Zhang, and Martin\u00a0T. Vechev. 2019. DL2: Training and Querying Neural Networks with Logic. In Proceedings of the 36th International Conference on Machine Learning, ICML 2019, 9-15 June 2019, Long Beach, California, USA(Proceedings of Machine Learning Research, Vol.\u00a097), Kamalika Chaudhuri and Ruslan Salakhutdinov (Eds.). PMLR, 1931\u20131941. http:\/\/proceedings.mlr.press\/v97\/fischer19a.html"},{"doi-asserted-by":"crossref","unstructured":"T. Gehr M. Mirman D. Drachsler-Cohen E. Tsankov S. Chaudhuri and M. Vechev. 2018. AI2: Safety and Robustness Certification of Neural Networks with Abstract Interpretation. In S&P.  T. Gehr M. Mirman D. Drachsler-Cohen E. Tsankov S. Chaudhuri and M. Vechev. 2018. AI2: Safety and Robustness Certification of Neural Networks with Abstract Interpretation. In S&P.","key":"e_1_3_2_1_15_1","DOI":"10.1109\/SP.2018.00058"},{"key":"e_1_3_2_1_16_1","volume-title":"Global Optimisation with Constructive Reals. In 36th Annual ACM\/IEEE Symposium on Logic in Computer Science, LICS 2021","author":"R.","year":"2021","unstructured":"Dan\u00a0 R. Ghica and Todd\u00a0Waugh Ambridge. 2021 . Global Optimisation with Constructive Reals. In 36th Annual ACM\/IEEE Symposium on Logic in Computer Science, LICS 2021 , Rome, Italy, June 29 - July 2, 2021 . 1\u201313. Dan\u00a0R. Ghica and Todd\u00a0Waugh Ambridge. 2021. Global Optimisation with Constructive Reals. In 36th Annual ACM\/IEEE Symposium on Logic in Computer Science, LICS 2021, Rome, Italy, June 29 - July 2, 2021. 1\u201313."},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_17_1","DOI":"10.1017\/S095679680000160X"},{"volume-title":"Intelligent Computer Mathematics(Lecture Notes in Computer Science), James\u00a0H","author":"Heras J\u00f3nathan","unstructured":"J\u00f3nathan Heras , Mar\u00eda Poza , Maxime D\u00e9n\u00e8s , and Laurence Rideau . 2011. Incidence Simplicial Matrices Formalized in Coq\/SSReflect . In Intelligent Computer Mathematics(Lecture Notes in Computer Science), James\u00a0H . Davenport, William\u00a0M. Farmer, Josef Urban, and Florian Rabe (Eds.). Springer , Berlin, Heidelberg , 30\u201344. https:\/\/doi.org\/10.1007\/978-3-642-22673-1_3 10.1007\/978-3-642-22673-1_3 J\u00f3nathan Heras, Mar\u00eda Poza, Maxime D\u00e9n\u00e8s, and Laurence Rideau. 2011. Incidence Simplicial Matrices Formalized in Coq\/SSReflect. In Intelligent Computer Mathematics(Lecture Notes in Computer Science), James\u00a0H. Davenport, William\u00a0M. Farmer, Josef Urban, and Florian Rabe (Eds.). Springer, Berlin, Heidelberg, 30\u201344. https:\/\/doi.org\/10.1007\/978-3-642-22673-1_3","key":"e_1_3_2_1_18_1"},{"key":"e_1_3_2_1_19_1","volume-title":"CAV 2017, Heidelberg, Germany, July 24-28, 2017, Proceedings, Part I(Lecture Notes in Computer Science, Vol.\u00a010426)","author":"Huang Xiaowei","year":"2017","unstructured":"Xiaowei Huang , Marta Kwiatkowska , Sen Wang , and Min Wu . 2017 . Safety Verification of Deep Neural Networks. In Computer Aided Verification - 29th International Conference , CAV 2017, Heidelberg, Germany, July 24-28, 2017, Proceedings, Part I(Lecture Notes in Computer Science, Vol.\u00a010426) . 3\u201329. Xiaowei Huang, Marta Kwiatkowska, Sen Wang, and Min Wu. 2017. Safety Verification of Deep Neural Networks. In Computer Aided Verification - 29th International Conference, CAV 2017, Heidelberg, Germany, July 24-28, 2017, Proceedings, Part I(Lecture Notes in Computer Science, Vol.\u00a010426). 3\u201329."},{"key":"e_1_3_2_1_20_1","volume-title":"SAS 2021, Chicago, IL, USA, October 17-19, 2021, Proceedings(Lecture Notes in Computer Science, Vol.\u00a012913)","author":"Jia Kai","year":"2021","unstructured":"Kai Jia and Martin Rinard . 2021 . Exploiting Verified Neural Networks via Floating Point Numerical Error. In Static Analysis - 28th International Symposium , SAS 2021, Chicago, IL, USA, October 17-19, 2021, Proceedings(Lecture Notes in Computer Science, Vol.\u00a012913) . Springer, 191\u2013205. Kai Jia and Martin Rinard. 2021. Exploiting Verified Neural Networks via Floating Point Numerical Error. In Static Analysis - 28th International Symposium, SAS 2021, Chicago, IL, USA, October 17-19, 2021, Proceedings(Lecture Notes in Computer Science, Vol.\u00a012913). Springer, 191\u2013205."},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_21_1","DOI":"10.1145\/2429135.2429155"},{"key":"e_1_3_2_1_22_1","volume-title":"Reluplex: An Efficient SMT Solver for Verifying Deep Neural Networks. In CAV.","author":"Katz G.","year":"2017","unstructured":"G. Katz , C. Barrett , D. Dill , K. Julian , and M. Kochenderfer . 2017 . Reluplex: An Efficient SMT Solver for Verifying Deep Neural Networks. In CAV. G. Katz, C. Barrett, D. Dill, K. Julian, and M. Kochenderfer. 2017. Reluplex: An Efficient SMT Solver for Verifying Deep Neural Networks. In CAV."},{"key":"e_1_3_2_1_23_1","volume-title":"Reluplex: An Efficient SMT Solver for Verifying Deep Neural Networks. arXiv:1702.01135 [cs] (May","author":"Katz Guy","year":"2017","unstructured":"Guy Katz , Clark Barrett , David Dill , Kyle Julian , and Mykel Kochenderfer . 2017 . Reluplex: An Efficient SMT Solver for Verifying Deep Neural Networks. arXiv:1702.01135 [cs] (May 2017). http:\/\/arxiv.org\/abs\/1702.01135 arXiv:1702.01135. Guy Katz, Clark Barrett, David Dill, Kyle Julian, and Mykel Kochenderfer. 2017. Reluplex: An Efficient SMT Solver for Verifying Deep Neural Networks. arXiv:1702.01135 [cs] (May 2017). http:\/\/arxiv.org\/abs\/1702.01135 arXiv:1702.01135."},{"key":"e_1_3_2_1_24_1","volume-title":"CAV","author":"Katz Guy","year":"2019","unstructured":"Guy Katz , Derek\u00a0 A. Huang , Duligur Ibeling , Kyle Julian , Christopher Lazarus , Rachel Lim , Parth Shah , Shantanu Thakoor , Haoze Wu , Aleksandar Zeljic , David\u00a0 L. Dill , Mykel\u00a0 J. Kochenderfer , and Clark\u00a0 W. Barrett . 2019. The Marabou Framework for Verification and Analysis of Deep Neural Networks . In CAV 2019 , Part I(LNCS, Vol .\u00a011561). Springer , 443\u2013452. Guy Katz, Derek\u00a0A. Huang, Duligur Ibeling, Kyle Julian, Christopher Lazarus, Rachel Lim, Parth Shah, Shantanu Thakoor, Haoze Wu, Aleksandar Zeljic, David\u00a0L. Dill, Mykel\u00a0J. Kochenderfer, and Clark\u00a0W. Barrett. 2019. The Marabou Framework for Verification and Analysis of Deep Neural Networks. In CAV 2019, Part I(LNCS, Vol.\u00a011561). Springer, 443\u2013452."},{"key":"e_1_3_2_1_25_1","volume-title":"APLAS 2020, Fukuoka, Japan, November 30 - December 2, 2020, Proceedings(Lecture Notes in Computer Science, Vol.\u00a012470)","author":"Kokke Wen","year":"2020","unstructured":"Wen Kokke , Ekaterina Komendantskaya , Daniel Kienitz , Robert Atkey , and David Aspinall . 2020 . Neural Networks, Secure by Construction - An Exploration of Refinement Types. In Programming Languages and Systems - 18th Asian Symposium , APLAS 2020, Fukuoka, Japan, November 30 - December 2, 2020, Proceedings(Lecture Notes in Computer Science, Vol.\u00a012470) . Springer, 67\u201385. Wen Kokke, Ekaterina Komendantskaya, Daniel Kienitz, Robert Atkey, and David Aspinall. 2020. Neural Networks, Secure by Construction - An Exploration of Refinement Types. In Programming Languages and Systems - 18th Asian Symposium, APLAS 2020, Fukuoka, Japan, November 30 - December 2, 2020, Proceedings(Lecture Notes in Computer Science, Vol.\u00a012470). Springer, 67\u201385."},{"volume-title":"Neural Network Compression Framework for Fast Model Inference","author":"Kozlov Alexander","unstructured":"Alexander Kozlov , Ivan Lazarevich , Vasily Shamporov , Nikolay Lyalyushkin , and Yury Gorbachev . 2021. Neural Network Compression Framework for Fast Model Inference . In Intelligent Computing, Kohei Arai (Ed.). Springer International Publishing , Cham , 213\u2013232. Alexander Kozlov, Ivan Lazarevich, Vasily Shamporov, Nikolay Lyalyushkin, and Yury Gorbachev. 2021. Neural Network Compression Framework for Fast Model Inference. In Intelligent Computing, Kohei Arai (Ed.). Springer International Publishing, Cham, 213\u2013232.","key":"e_1_3_2_1_26_1"},{"unstructured":"Raghuraman Krishnamoorthi. 2018. Quantizing deep convolutional networks for efficient inference: A whitepaper. CoRR abs\/1806.08342(2018). arXiv:1806.08342http:\/\/arxiv.org\/abs\/1806.08342  Raghuraman Krishnamoorthi. 2018. Quantizing deep convolutional networks for efficient inference: A whitepaper. CoRR abs\/1806.08342(2018). arXiv:1806.08342http:\/\/arxiv.org\/abs\/1806.08342","key":"e_1_3_2_1_27_1"},{"key":"e_1_3_2_1_28_1","volume-title":"FMCAD 2021","author":"Lahav Ori","year":"2021","unstructured":"Ori Lahav and Guy Katz . 2021 . Pruning and Slicing Neural Networks using Formal Verification. In Formal Methods in Computer Aided Design , FMCAD 2021 , New Haven, CT, USA , October 19-22, 2021. 1\u201310. https:\/\/doi.org\/10.34727\/2021\/isbn.978-3-85448-046-4_27 10.34727\/2021 Ori Lahav and Guy Katz. 2021. Pruning and Slicing Neural Networks using Formal Verification. In Formal Methods in Computer Aided Design, FMCAD 2021, New Haven, CT, USA, October 19-22, 2021. 1\u201310. https:\/\/doi.org\/10.34727\/2021\/isbn.978-3-85448-046-4_27"},{"key":"e_1_3_2_1_29_1","volume-title":"6th International Conference on Learning Representations, ICLR","author":"Madry Aleksander","year":"2018","unstructured":"Aleksander Madry , Aleksandar Makelov , Ludwig Schmidt , Dimitris Tsipras , and Adrian Vladu . 2018. Towards Deep Learning Models Resistant to Adversarial Attacks . In 6th International Conference on Learning Representations, ICLR 2018 , Vancouver, BC , Canada, April 30 - May 3, 2018, Conference Track Proceedings. OpenReview .net. https:\/\/openreview.net\/forum?id=rJzIBfZAb Aleksander Madry, Aleksandar Makelov, Ludwig Schmidt, Dimitris Tsipras, and Adrian Vladu. 2018. Towards Deep Learning Models Resistant to Adversarial Attacks. In 6th International Conference on Learning Representations, ICLR 2018, Vancouver, BC, Canada, April 30 - May 3, 2018, Conference Track Proceedings. OpenReview.net. https:\/\/openreview.net\/forum?id=rJzIBfZAb"},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_30_1","DOI":"10.1007\/s11704-020-0029-6"},{"key":"e_1_3_2_1_31_1","volume-title":"FM 2021, Virtual Event, November 20-26, 2021, Proceedings(Lecture Notes in Computer Science, Vol.\u00a013047)","author":"Passmore Grant\u00a0Olney","year":"2021","unstructured":"Grant\u00a0Olney Passmore . 2021 . Some Lessons Learned in the Industrialization of Formal Methods for Financial Algorithms. In Formal Methods - 24th International Symposium , FM 2021, Virtual Event, November 20-26, 2021, Proceedings(Lecture Notes in Computer Science, Vol.\u00a013047) . Springer, 717\u2013721. Grant\u00a0Olney Passmore. 2021. Some Lessons Learned in the Industrialization of Formal Methods for Financial Algorithms. In Formal Methods - 24th International Symposium, FM 2021, Virtual Event, November 20-26, 2021, Proceedings(Lecture Notes in Computer Science, Vol.\u00a013047). Springer, 717\u2013721."},{"key":"e_1_3_2_1_32_1","volume-title":"IJCAR 2020, Paris, France, July 1-4, 2020, Proceedings, Part II, Vol.\u00a012167","author":"Passmore O.","year":"2020","unstructured":"Grant\u00a0 O. Passmore , Simon Cruanes , Denis Ignatovich , Dave Aitken , Matt Bray , Elijah Kagan , Kostya Kanishev , Ewen Maclean , and Nicola Mometto . 2020 . The Imandra Automated Reasoning System (System Description). In Automated Reasoning - 10th International Joint Conference , IJCAR 2020, Paris, France, July 1-4, 2020, Proceedings, Part II, Vol.\u00a012167 . Springer, 464\u2013471. Grant\u00a0O. Passmore, Simon Cruanes, Denis Ignatovich, Dave Aitken, Matt Bray, Elijah Kagan, Kostya Kanishev, Ewen Maclean, and Nicola Mometto. 2020. The Imandra Automated Reasoning System (System Description). In Automated Reasoning - 10th International Joint Conference, IJCAR 2020, Paris, France, July 1-4, 2020, Proceedings, Part II, Vol.\u00a012167. Springer, 464\u2013471."},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_33_1","DOI":"10.1186\/s40537-019-0197-0"},{"volume-title":"Monotonic Networks","author":"Sill Joseph","unstructured":"Joseph Sill . 1998. Monotonic Networks . California Institute of Technology . Joseph Sill. 1998. Monotonic Networks. California Institute of Technology.","key":"e_1_3_2_1_34_1"},{"key":"e_1_3_2_1_35_1","volume-title":"POPL","author":"Singh Gagandeep","year":"2019","unstructured":"Gagandeep Singh , Timon Gehr , Markus P\u00fcschel , and Martin\u00a0 T. Vechev . 2019. An abstract domain for certifying neural networks. PACMPL 3 , POPL ( 2019 ), 41:1\u201341:30. https:\/\/doi.org\/10.1145\/3290354 10.1145\/3290354 Gagandeep Singh, Timon Gehr, Markus P\u00fcschel, and Martin\u00a0T. Vechev. 2019. An abstract domain for certifying neural networks. PACMPL 3, POPL (2019), 41:1\u201341:30. https:\/\/doi.org\/10.1145\/3290354"},{"unstructured":"Natalia Slusarz Ekaterina Komendantskaya Matthew\u00a0L. Daggitt and Robert Stewart. 2022. Differentiable Logics for Neural Network Training and Verification. https:\/\/doi.org\/10.48550\/arXiv.2207.06741 arXiv:2207.06741 [cs]. 10.48550\/arXiv.2207.06741","key":"#cr-split#-e_1_3_2_1_36_1.1"},{"doi-asserted-by":"crossref","unstructured":"Natalia Slusarz Ekaterina Komendantskaya Matthew\u00a0L. Daggitt and Robert Stewart. 2022. Differentiable Logics for Neural Network Training and Verification. https:\/\/doi.org\/10.48550\/arXiv.2207.06741 arXiv:2207.06741 [cs].","key":"#cr-split#-e_1_3_2_1_36_1.2","DOI":"10.1007\/978-3-031-21222-2_5"},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_37_1","DOI":"10.1145\/3437992.3439917"},{"key":"e_1_3_2_1_38_1","volume-title":"Unconstrained Monotonic Neural Networks. In Advances in Neural Information Processing Systems 32: Annual Conference on Neural Information Processing Systems 2019","author":"Wehenkel Antoine","year":"2019","unstructured":"Antoine Wehenkel and Gilles Louppe . 2019 . Unconstrained Monotonic Neural Networks. In Advances in Neural Information Processing Systems 32: Annual Conference on Neural Information Processing Systems 2019 , NeurIPS 2019, December 8-14, 2019, Vancouver, BC, Canada. 1543\u20131553. Antoine Wehenkel and Gilles Louppe. 2019. Unconstrained Monotonic Neural Networks. In Advances in Neural Information Processing Systems 32: Annual Conference on Neural Information Processing Systems 2019, NeurIPS 2019, December 8-14, 2019, Vancouver, BC, Canada. 1543\u20131553."},{"unstructured":"James Wood. 2019. Vectors and Matrices in Agda. https:\/\/personal.cis.strath.ac.uk\/james.wood.100\/blog\/html\/VecMat.html  James Wood. 2019. Vectors and Matrices in Agda. https:\/\/personal.cis.strath.ac.uk\/james.wood.100\/blog\/html\/VecMat.html","key":"e_1_3_2_1_39_1"}],"event":{"acronym":"PPDP 2022","name":"PPDP 2022: 24th International Symposium on Principles and Practice of Declarative Programming","location":"Tbilisi Georgia"},"container-title":["Proceedings of the 24th International Symposium on Principles and Practice of Declarative Programming"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3551357.3551372","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3551357.3551372","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T19:00:24Z","timestamp":1750186824000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3551357.3551372"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022,9,20]]},"references-count":41,"alternative-id":["10.1145\/3551357.3551372","10.1145\/3551357"],"URL":"https:\/\/doi.org\/10.1145\/3551357.3551372","relation":{},"subject":[],"published":{"date-parts":[[2022,9,20]]},"assertion":[{"value":"2022-09-20","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}