{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,17]],"date-time":"2026-07-17T11:07:34Z","timestamp":1784286454034,"version":"3.55.0"},"publisher-location":"Cham","reference-count":33,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783032323569","type":"print"},{"value":"9783032323576","type":"electronic"}],"license":[{"start":{"date-parts":[[2026,7,18]],"date-time":"2026-07-18T00:00:00Z","timestamp":1784332800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2026,7,18]],"date-time":"2026-07-18T00:00:00Z","timestamp":1784332800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2027]]},"DOI":"10.1007\/978-3-032-32357-6_15","type":"book-chapter","created":{"date-parts":[[2026,7,17]],"date-time":"2026-07-17T10:35:23Z","timestamp":1784284523000},"page":"317-330","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Verification of\u00a0LTL Properties on\u00a0Neural Networks for\u00a0Chemical Process Monitoring"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-6374-3694","authenticated-orcid":false,"given":"Julien","family":"Girard-Satabin","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-6006-6325","authenticated-orcid":false,"given":"Simon","family":"Lutz","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-9276-6342","authenticated-orcid":false,"given":"Daniel","family":"Neider","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2026,7,18]]},"reference":[{"key":"15_CR1","doi-asserted-by":"crossref","unstructured":"Alberti, M., Bobot, F., Chihani, Z., Grastien, A., Girard-Satabin, J.: The CAISAR platform: extending the reach of machine learning specification and verification. In: International Conference on Integrated Formal Methods (IFM), pp. 290\u2013309 (2025)","DOI":"10.1007\/978-3-032-10794-7_15"},{"key":"15_CR2","doi-asserted-by":"crossref","unstructured":"Athavale, A., Bartocci, E., Christakis, M., Maffei, M., Nickovic, D., Weissenbacher, G.: Verifying global two-safety properties in neural networks with confidence. In: International Conference on Computer Aided Verification (CAV), pp. 329\u2013351 (2024)","DOI":"10.1007\/978-3-031-65630-9_17"},{"key":"15_CR3","doi-asserted-by":"crossref","unstructured":"Bak, S.: NNENUM: verification of RELU neural networks with optimized abstraction refinement. In: NASA Formal Methods Symposium (NFM), pp. 19\u201336","DOI":"10.1007\/978-3-030-76384-8_2"},{"key":"15_CR4","doi-asserted-by":"crossref","unstructured":"Barrett, C., Sebastiani, R., Seshia, S., Tinelli, C.: Satisfiability modulo theories. In: Biere, A., Heule, M.J.H., van Maaren, H., Walsh, T. (eds.) Handbook of Satisfiability, Second Edition, Frontiers in Artificial Intelligence and Applications, vol.\u00a0336, chap.\u00a033, pp. 825\u2013885. IOS Press (2021). http:\/\/theory.stanford.edu\/~barrett\/pubs\/BSST21.pdf","DOI":"10.3233\/FAIA201017"},{"issue":"1","key":"15_CR5","doi-asserted-by":"publisher","first-page":"55","DOI":"10.1007\/s44230-022-00004-0","volume":"2","author":"R Bin Sulaiman","year":"2022","unstructured":"Bin Sulaiman, R., Schetinin, V., Sant, P.: Review of machine learning approach on credit card fraud detection. Human-Centric Intell. Syst. 2(1), 55\u201368 (2022)","journal-title":"Human-Centric Intell. Syst."},{"key":"15_CR6","unstructured":"Boetius, D., Leue, S.: Verifying global neural network specifications using hyperproperties (2023)"},{"key":"15_CR7","unstructured":"Brix, C., Bak, S., Johnson, T.T., Wu, H.: The fifth international verification of neural networks competition (VNN-COMP 2024): summary and results (2024)"},{"key":"15_CR8","doi-asserted-by":"crossref","unstructured":"Casadio, M., et al.: Neural network robustness as a verification property: a principled case study. In: International Conference on Computer Aided Verification, pp. 219\u2013231. Springer (2022)","DOI":"10.1007\/978-3-031-13185-1_11"},{"key":"15_CR9","unstructured":"Community: ONNX: open neural network exchange format standard for machine learning interoperability (2022)"},{"key":"15_CR10","doi-asserted-by":"publisher","unstructured":"Cordeiro, L.C., et al.: Neural Network Verification is a Programming Language Challenge. In: Vafeiadis, V. (ed.) Programming Languages and Systems, pp. 206\u2013235. Springer Nature Switzerland (2025). https:\/\/doi.org\/10.1007\/978-3-031-91118-7_9","DOI":"10.1007\/978-3-031-91118-7_9"},{"key":"15_CR11","doi-asserted-by":"publisher","unstructured":"Daggitt, M.L., Kokke, W., Atkey, R., Slusarz, N., Arnaboldi, L., Komendantskaya, E.: Vehicle: bridging the embedding gap in the verification of neuro-symbolic programs (2024). https:\/\/doi.org\/10.48550\/ARXIV.2401.06379","DOI":"10.48550\/ARXIV.2401.06379"},{"key":"15_CR12","doi-asserted-by":"crossref","unstructured":"Demarchi, S., Guidotti, D., Pulina, L., Tacchella, A.: Supporting standardization of neural networks verification with VNN-LIB and CoCoNet. In: Workshop on Formal Methods for ML-Enabled Autonomous Systems (FoMLAS), pp. 47\u201358 (2023)","DOI":"10.29007\/5pdh"},{"key":"15_CR13","doi-asserted-by":"publisher","unstructured":"Filli\u00e2tre, J.C., Paskevich, A.: Why3 - where programs meet provers. In: Felleisen, M., Gardner, P. (eds.) Programming Languages and Systems, pp. 125\u2013128. Lecture Notes in Computer Science, Springer, Berlin, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-37036-6_8","DOI":"10.1007\/978-3-642-37036-6_8"},{"key":"15_CR14","doi-asserted-by":"crossref","unstructured":"Geatti, L., Gianola, A., Gigante, N., et al.: Linear temporal logic modulo theories over finite traces. In: IJCAI. vol. 22, pp. 2641\u20132647 (2022)","DOI":"10.24963\/ijcai.2022\/366"},{"key":"15_CR15","doi-asserted-by":"publisher","unstructured":"Goodfellow, I., et al.: Generative adversarial networks 63(11), 139\u2013144 (2020). https:\/\/doi.org\/10.1145\/3422622","DOI":"10.1145\/3422622"},{"key":"15_CR16","unstructured":"Goodfellow, I.J., Shlens, J., Szegedy, C.: Explaining and harnessing adversarial examples. In: International Conference on Learning Representations (2015)"},{"key":"15_CR17","doi-asserted-by":"crossref","unstructured":"Halbwachs, N., Caspi, P., Pilaud, D.: The synchronous dataflow programming language LUSTRE. Another Look at Real Time Programming, Proceedings of the IEEE (1991)","DOI":"10.1109\/5.97300"},{"key":"15_CR18","doi-asserted-by":"publisher","unstructured":"Hosseini, M., Lomuscio, A., Paoletti, N.: LTL verification of memoryful neural agents. https:\/\/doi.org\/10.48550\/arXiv.2503.02512. http:\/\/arxiv.org\/abs\/2503.02512","DOI":"10.48550\/arXiv.2503.02512"},{"key":"15_CR19","unstructured":"Huang, Y., Chen, Y.: Autonomous driving with deep learning: a survey of state-of-art technologies (2020). https:\/\/arxiv.org\/abs\/2006.06091"},{"key":"15_CR20","doi-asserted-by":"publisher","unstructured":"Katz, G., Barrett, C., Dill, D.L., Julian, K., Kochenderfer, M.J.: Reluplex: an efficient SMT solver for verifying deep neural networks. In: Computer Aided Verification, pp. 97\u2013117. Springer International Publishing (2017). https:\/\/doi.org\/10.1007\/978-3-319-63387-9_5","DOI":"10.1007\/978-3-319-63387-9_5"},{"key":"15_CR21","doi-asserted-by":"publisher","unstructured":"Kuo, Y.L., Katz, B., Barbu, A.: Encoding formulas as deep networks: reinforcement learning for zero-shot execution of LTL formulas. In: 2020 IEEE\/RSJ International Conference on Intelligent Robots and Systems (IROS), pp. 5604\u20135610 (2020). https:\/\/doi.org\/10.1109\/IROS45743.2020.9341325. https:\/\/ieeexplore.ieee.org\/abstract\/document\/9341325","DOI":"10.1109\/IROS45743.2020.9341325"},{"key":"15_CR22","doi-asserted-by":"crossref","unstructured":"Lemesle, A., Lehmann, J., Gall, T.L., Chihani, Z.: Neural network verification with PYRAT. In: International Static Analysis Symposium (SAS), pp. 11\u201333 (2025)","DOI":"10.1007\/978-3-032-07106-4_2"},{"key":"15_CR23","doi-asserted-by":"publisher","first-page":"290","DOI":"10.1007\/978-3-032-25305-7_20","volume-title":"Machine learning and principles and practice of knowledge discovery in databases","author":"S Lutz","year":"2026","unstructured":"Lutz, S., et al.: A benchmark suite for verifying neural anomaly detectors in distillation processes. In: Cerrato, M., Kalinauskait\u0117, D., Luko\u0161evi\u010dius, M., Pechenizkiy, M., \u0160utien\u0117, K. (eds.) Machine learning and principles and practice of knowledge discovery in databases, pp. 290\u2013306. Springer Nature Switzerland, Cham (2026)"},{"key":"15_CR24","unstructured":"Malhotra, P., Vig, L., Shroff, G., Agarwal, P.: Long short term memory networks for anomaly detection in time series (2015)"},{"key":"15_CR25","doi-asserted-by":"publisher","unstructured":"Neider, D., Roy, R.: What is formal verification without specifications? a survey on mining LTL specifications (2025).https:\/\/doi.org\/10.48550\/arXiv.2501.16274. http:\/\/arxiv.org\/abs\/2501.16274","DOI":"10.48550\/arXiv.2501.16274"},{"key":"15_CR26","doi-asserted-by":"publisher","unstructured":"Pnueli, A.: The temporal logic of programs. In: 18th Annual Symposium on Foundations of Computer Science (Sfcs 1977), pp. 46\u201357. IEEE (1977). https:\/\/doi.org\/10.1109\/sfcs.1977.32","DOI":"10.1109\/sfcs.1977.32"},{"key":"15_CR27","doi-asserted-by":"crossref","unstructured":"Pnueli, A.: Applications of temporal logic to the specification and verification of reactive systems: a survey of current trends. In: Current Trends in Concurrency: Overviews and Tutorials, pp. 510\u2013584 Springer (2005)","DOI":"10.1007\/BFb0027047"},{"key":"15_CR28","doi-asserted-by":"publisher","unstructured":"Pulina, L., Tacchella, A.: Never: a tool for artificial neural networks verification. Ann. Math. Artif. Intell. 62(3\u20134), 403\u2013425 (2011). https:\/\/doi.org\/10.1007\/s10472-011-9243-0","DOI":"10.1007\/s10472-011-9243-0"},{"key":"15_CR29","unstructured":"Wagner, D., et al.: NOBOOM: chemical process datasets for industrial anomaly detection. In: NeurIPS (2025). https:\/\/neurips.cc\/virtual\/2025\/loc\/san-diego\/poster\/121442"},{"key":"15_CR30","doi-asserted-by":"publisher","unstructured":"Wang, C., Li, Y., Smith, S.L., Liu, J.: Continuous motion planning with temporal logic specifications using deep neural networks (2020). https:\/\/doi.org\/10.48550\/arXiv.2004.02610. http:\/\/arxiv.org\/abs\/2004.02610","DOI":"10.48550\/arXiv.2004.02610"},{"key":"15_CR31","unstructured":"Wang, S., et al.: Beta-CROWN: efficient bound propagation with per-neuron split constraints for complete and incomplete neural network robustness verification. In: Advances in Neural Information Processing Systems (NeurIPS), pp. 29909\u201329921. (2021)"},{"key":"15_CR32","doi-asserted-by":"crossref","unstructured":"Wu, H., et al.: Marabou 2.0: a versatile formal analyzer of neural networks. In: International Conference on Computer Aided Verification (CAV), pp. 249\u2013264 (2024)","DOI":"10.1007\/978-3-031-65630-9_13"},{"key":"15_CR33","doi-asserted-by":"publisher","unstructured":"Yuan, H., Yu, K., Xie, F., Liu, M., Sun, S.: Automated machine learning with interpretation: a systematic review of methodologies and applications in healthcare. Med. Adv. 2(3), 205\u2013237 (2024). https:\/\/doi.org\/10.1002\/med4.75. https:\/\/onlinelibrary.wiley.com\/doi\/abs\/10.1002\/med4.75","DOI":"10.1002\/med4.75"}],"container-title":["Lecture Notes in Computer Science","AI Verification"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-032-32357-6_15","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,7,17]],"date-time":"2026-07-17T10:35:31Z","timestamp":1784284531000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-032-32357-6_15"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2026,7,18]]},"ISBN":["9783032323569","9783032323576"],"references-count":33,"URL":"https:\/\/doi.org\/10.1007\/978-3-032-32357-6_15","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2026,7,18]]},"assertion":[{"value":"18 July 2026","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"The authors have no competing interests to declare that are relevant to the content of this article.","order":1,"name":"Ethics","label":"Disclosure of Interest","group":{"name":"EthicsHeading","label":"Ethics"}},{"value":"SAIV","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Symposium on AI Verification","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Lisbon","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Portugal","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2026","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"24 July 2026","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"25 July 2026","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"3","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"saiv2026","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/aiverification.org\/2026","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}