[{"project":[{"grant_number":"101020093","name":"Vigilant Algorithmic Monitoring of Software","_id":"62781420-2b32-11ec-9570-8d9b63373d4d","call_identifier":"H2020"}],"citation":{"ista":"Chalupa M, Henzinger TA. 2023. Bubaak: Runtime monitoring of program verifiers. Tools and Algorithms for the Construction and Analysis of Systems. TACAS: Tools and Algorithms for the Construction and Analysis of Systems, LNCS, vol. 13994, 535–540.","chicago":"Chalupa, Marek, and Thomas A Henzinger. “Bubaak: Runtime Monitoring of Program Verifiers.” In Tools and Algorithms for the Construction and Analysis of Systems, 13994:535–40. Springer Nature, 2023. https://doi.org/10.1007/978-3-031-30820-8_32.","apa":"Chalupa, M., & Henzinger, T. A. (2023). Bubaak: Runtime monitoring of program verifiers. In Tools and Algorithms for the Construction and Analysis of Systems (Vol. 13994, pp. 535–540). Paris, France: Springer Nature. https://doi.org/10.1007/978-3-031-30820-8_32","ama":"Chalupa M, Henzinger TA. Bubaak: Runtime monitoring of program verifiers. In: Tools and Algorithms for the Construction and Analysis of Systems. Vol 13994. Springer Nature; 2023:535-540. doi:10.1007/978-3-031-30820-8_32","ieee":"M. Chalupa and T. A. Henzinger, “Bubaak: Runtime monitoring of program verifiers,” in Tools and Algorithms for the Construction and Analysis of Systems, Paris, France, 2023, vol. 13994, pp. 535–540.","short":"M. Chalupa, T.A. Henzinger, in:, Tools and Algorithms for the Construction and Analysis of Systems, Springer Nature, 2023, pp. 535–540.","mla":"Chalupa, Marek, and Thomas A. Henzinger. “Bubaak: Runtime Monitoring of Program Verifiers.” Tools and Algorithms for the Construction and Analysis of Systems, vol. 13994, Springer Nature, 2023, pp. 535–40, doi:10.1007/978-3-031-30820-8_32."},"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","author":[{"full_name":"Chalupa, Marek","last_name":"Chalupa","first_name":"Marek","id":"87e34708-d6c6-11ec-9f5b-9391e7be2463"},{"id":"40876CD8-F248-11E8-B48F-1D18A9856A87","first_name":"Thomas A","last_name":"Henzinger","orcid":"0000-0002-2985-7724","full_name":"Henzinger, Thomas A"}],"article_processing_charge":"No","title":"Bubaak: Runtime monitoring of program verifiers","acknowledgement":"This work was supported by the ERC-2020-AdG 10102009 grant.","publisher":"Springer Nature","quality_controlled":"1","oa":1,"has_accepted_license":"1","year":"2023","day":"20","publication":"Tools and Algorithms for the Construction and Analysis of Systems","page":"535-540","date_published":"2023-04-20T00:00:00Z","doi":"10.1007/978-3-031-30820-8_32","date_created":"2023-04-20T08:22:53Z","_id":"12854","type":"conference","conference":{"name":"TACAS: Tools and Algorithms for the Construction and Analysis of Systems","location":"Paris, France","end_date":"2023-04-27","start_date":"2023-04-22"},"tmp":{"legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","image":"/images/cc_by.png","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","short":"CC BY (4.0)"},"status":"public","date_updated":"2023-04-25T07:02:43Z","ddc":["000"],"department":[{"_id":"ToHe"}],"file_date_updated":"2023-04-25T06:58:36Z","abstract":[{"text":"The main idea behind BUBAAK is to run multiple program analyses in parallel and use runtime monitoring and enforcement to observe and control their progress in real time. The analyses send information about (un)explored states of the program and discovered invariants to a monitor. The monitor processes the received data and can force an analysis to stop the search of certain program parts (which have already been analyzed by other analyses), or to make it utilize a program invariant found by another analysis.\r\nAt SV-COMP 2023, the implementation of data exchange between the monitor and the analyses was not yet completed, which is why BUBAAK only ran several analyses in parallel, without any coordination. Still, BUBAAK won the meta-category FalsificationOverall and placed very well in several other (sub)-categories of the competition.","lang":"eng"}],"oa_version":"Published Version","alternative_title":["LNCS"],"month":"04","intvolume":" 13994","publication_identifier":{"eisbn":["9783031308208"],"issn":["0302-9743"],"isbn":["9783031308192"],"eissn":["1611-3349"]},"publication_status":"published","file":[{"date_created":"2023-04-25T06:58:36Z","file_name":"2023_LNCS_Chalupa.pdf","creator":"dernst","date_updated":"2023-04-25T06:58:36Z","file_size":16096413,"checksum":"120d2c2a38384058ad0630fdf8288312","file_id":"12864","success":1,"access_level":"open_access","relation":"main_file","content_type":"application/pdf"}],"language":[{"iso":"eng"}],"volume":13994,"license":"https://creativecommons.org/licenses/by/4.0/","ec_funded":1},{"file_date_updated":"2023-04-25T07:16:36Z","department":[{"_id":"ToHe"}],"date_updated":"2023-04-25T07:19:07Z","ddc":["000"],"conference":{"name":"FASE: Fundamental Approaches to Software Engineering","end_date":"2023-04-27","location":"Paris, France","start_date":"2023-04-22"},"tmp":{"legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","image":"/images/cc_by.png","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","short":"CC BY (4.0)"},"type":"conference","status":"public","_id":"12856","ec_funded":1,"volume":13991,"related_material":{"record":[{"status":"public","id":"12407","relation":"earlier_version"}]},"publication_status":"published","publication_identifier":{"eisbn":["9783031308260"],"issn":["0302-9743"],"eissn":["1611-3349"],"isbn":["9783031308253"]},"language":[{"iso":"eng"}],"file":[{"relation":"main_file","access_level":"open_access","content_type":"application/pdf","success":1,"file_id":"12865","checksum":"17a7c8e08be609cf2408d37ea55e322c","creator":"dernst","file_size":580828,"date_updated":"2023-04-25T07:16:36Z","file_name":"2023_LNCS_ChalupaM.pdf","date_created":"2023-04-25T07:16:36Z"}],"alternative_title":["LNCS"],"intvolume":" 13991","month":"04","abstract":[{"text":"As the complexity and criticality of software increase every year, so does the importance of run-time monitoring. Third-party monitoring, with limited knowledge of the monitored software, and best-effort monitoring, which keeps pace with the monitored software, are especially valuable, yet underexplored areas of run-time monitoring. Most existing monitoring frameworks do not support their combination because they either require access to the monitored code for instrumentation purposes or the processing of all observed events, or both.\r\n\r\nWe present a middleware framework, VAMOS, for the run-time monitoring of software which is explicitly designed to support third-party and best-effort scenarios. The design goals of VAMOS are (i) efficiency (keeping pace at low overhead), (ii) flexibility (the ability to monitor black-box code through a variety of different event channels, and the connectability to monitors written in different specification languages), and (iii) ease-of-use. To achieve its goals, VAMOS combines aspects of event broker and event recognition systems with aspects of stream processing systems.\r\nWe implemented a prototype toolchain for VAMOS and conducted experiments including a case study of monitoring for data races. The results indicate that VAMOS enables writing useful yet efficient monitors, is compatible with a variety of event sources and monitor specifications, and simplifies key aspects of setting up a monitoring system from scratch.","lang":"eng"}],"oa_version":"Published Version","article_processing_charge":"No","author":[{"first_name":"Marek","id":"87e34708-d6c6-11ec-9f5b-9391e7be2463","last_name":"Chalupa","full_name":"Chalupa, Marek"},{"last_name":"Mühlböck","orcid":"0000-0003-1548-0177","full_name":"Mühlböck, Fabian","first_name":"Fabian","id":"6395C5F6-89DF-11E9-9C97-6BDFE5697425"},{"id":"a376de31-8972-11ed-ae7b-d0251c13c8ff","first_name":"Stefanie","full_name":"Muroya Lei, Stefanie","last_name":"Muroya Lei"},{"id":"40876CD8-F248-11E8-B48F-1D18A9856A87","first_name":"Thomas A","last_name":"Henzinger","full_name":"Henzinger, Thomas A","orcid":"0000-0002-2985-7724"}],"title":"Vamos: Middleware for best-effort third-party monitoring","citation":{"ama":"Chalupa M, Mühlböck F, Muroya Lei S, Henzinger TA. Vamos: Middleware for best-effort third-party monitoring. In: Fundamental Approaches to Software Engineering. Vol 13991. Springer Nature; 2023:260-281. doi:10.1007/978-3-031-30826-0_15","apa":"Chalupa, M., Mühlböck, F., Muroya Lei, S., & Henzinger, T. A. (2023). Vamos: Middleware for best-effort third-party monitoring. In Fundamental Approaches to Software Engineering (Vol. 13991, pp. 260–281). Paris, France: Springer Nature. https://doi.org/10.1007/978-3-031-30826-0_15","short":"M. Chalupa, F. Mühlböck, S. Muroya Lei, T.A. Henzinger, in:, Fundamental Approaches to Software Engineering, Springer Nature, 2023, pp. 260–281.","ieee":"M. Chalupa, F. Mühlböck, S. Muroya Lei, and T. A. Henzinger, “Vamos: Middleware for best-effort third-party monitoring,” in Fundamental Approaches to Software Engineering, Paris, France, 2023, vol. 13991, pp. 260–281.","mla":"Chalupa, Marek, et al. “Vamos: Middleware for Best-Effort Third-Party Monitoring.” Fundamental Approaches to Software Engineering, vol. 13991, Springer Nature, 2023, pp. 260–81, doi:10.1007/978-3-031-30826-0_15.","ista":"Chalupa M, Mühlböck F, Muroya Lei S, Henzinger TA. 2023. Vamos: Middleware for best-effort third-party monitoring. Fundamental Approaches to Software Engineering. FASE: Fundamental Approaches to Software Engineering, LNCS, vol. 13991, 260–281.","chicago":"Chalupa, Marek, Fabian Mühlböck, Stefanie Muroya Lei, and Thomas A Henzinger. “Vamos: Middleware for Best-Effort Third-Party Monitoring.” In Fundamental Approaches to Software Engineering, 13991:260–81. Springer Nature, 2023. https://doi.org/10.1007/978-3-031-30826-0_15."},"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","project":[{"_id":"62781420-2b32-11ec-9570-8d9b63373d4d","call_identifier":"H2020","grant_number":"101020093","name":"Vigilant Algorithmic Monitoring of Software"}],"page":"260-281","date_created":"2023-04-20T08:29:42Z","date_published":"2023-04-20T00:00:00Z","doi":"10.1007/978-3-031-30826-0_15","year":"2023","has_accepted_license":"1","publication":"Fundamental Approaches to Software Engineering","day":"20","oa":1,"quality_controlled":"1","publisher":"Springer Nature","acknowledgement":"This work was supported in part by the ERC-2020-AdG 101020093. The authors would like to thank the anonymous FASE reviewers for their valuable feedback and suggestions."},{"publication_identifier":{"eissn":["2664-1690"]},"publication_status":"published","file":[{"date_created":"2023-01-27T03:18:34Z","file_name":"main.pdf","date_updated":"2023-01-27T03:18:34Z","file_size":662409,"creator":"fmuehlbo","file_id":"12408","checksum":"55426e463fdeafe9777fc3ff635154c7","success":1,"content_type":"application/pdf","access_level":"open_access","relation":"main_file"}],"language":[{"iso":"eng"}],"related_material":{"record":[{"status":"public","id":"12856","relation":"later_version"}]},"ec_funded":1,"abstract":[{"text":"As the complexity and criticality of software increase every year, so does the importance of run-time monitoring. Third-party monitoring, with limited knowledge of the monitored software, and best-effort monitoring, which keeps pace with the monitored software, are especially valuable, yet underexplored areas of run-time monitoring. Most existing monitoring frameworks do not support their combination because they either require access to the monitored code for instrumentation purposes or the processing of all observed events, or both.\r\n\r\nWe present a middleware framework, VAMOS, for the run-time monitoring of software which is explicitly designed to support third-party and best-effort scenarios. The design goals of VAMOS are (i) efficiency (keeping pace at low overhead), (ii) flexibility (the ability to monitor black-box code through a variety of different event channels, and the connectability to monitors written in different specification languages), and (iii) ease-of-use. To achieve its goals, VAMOS combines aspects of event broker and event recognition systems with aspects of stream processing systems.\r\n\r\nWe implemented a prototype toolchain for VAMOS and conducted experiments including a case study of monitoring for data races. The results indicate that VAMOS enables writing useful yet efficient monitors, is compatible with a variety of event sources and monitor specifications, and simplifies key aspects of setting up a monitoring system from scratch.","lang":"eng"}],"oa_version":"Published Version","alternative_title":["IST Austria Technical Report"],"month":"01","date_updated":"2023-04-25T07:19:06Z","ddc":["005"],"file_date_updated":"2023-01-27T03:18:34Z","department":[{"_id":"ToHe"}],"_id":"12407","type":"technical_report","tmp":{"legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","image":"/images/cc_by.png","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","short":"CC BY (4.0)"},"status":"public","keyword":["runtime monitoring","best effort","third party"],"has_accepted_license":"1","year":"2023","day":"27","page":"38","doi":"10.15479/AT:ISTA:12407","date_published":"2023-01-27T00:00:00Z","date_created":"2023-01-27T03:18:08Z","acknowledgement":"This work was supported in part by the ERC-2020-AdG 101020093. \r\nThe authors would like to thank the anonymous FASE reviewers for their valuable feedback and suggestions.","publisher":"Institute of Science and Technology Austria","oa":1,"citation":{"mla":"Chalupa, Marek, et al. VAMOS: Middleware for Best-Effort Third-Party Monitoring. Institute of Science and Technology Austria, 2023, doi:10.15479/AT:ISTA:12407.","apa":"Chalupa, M., Mühlböck, F., Muroya Lei, S., & Henzinger, T. A. (2023). VAMOS: Middleware for Best-Effort Third-Party Monitoring. Institute of Science and Technology Austria. https://doi.org/10.15479/AT:ISTA:12407","ama":"Chalupa M, Mühlböck F, Muroya Lei S, Henzinger TA. VAMOS: Middleware for Best-Effort Third-Party Monitoring. Institute of Science and Technology Austria; 2023. doi:10.15479/AT:ISTA:12407","ieee":"M. Chalupa, F. Mühlböck, S. Muroya Lei, and T. A. Henzinger, VAMOS: Middleware for Best-Effort Third-Party Monitoring. Institute of Science and Technology Austria, 2023.","short":"M. Chalupa, F. Mühlböck, S. Muroya Lei, T.A. Henzinger, VAMOS: Middleware for Best-Effort Third-Party Monitoring, Institute of Science and Technology Austria, 2023.","chicago":"Chalupa, Marek, Fabian Mühlböck, Stefanie Muroya Lei, and Thomas A Henzinger. VAMOS: Middleware for Best-Effort Third-Party Monitoring. Institute of Science and Technology Austria, 2023. https://doi.org/10.15479/AT:ISTA:12407.","ista":"Chalupa M, Mühlböck F, Muroya Lei S, Henzinger TA. 2023. VAMOS: Middleware for Best-Effort Third-Party Monitoring, Institute of Science and Technology Austria, 38p."},"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","author":[{"full_name":"Chalupa, Marek","last_name":"Chalupa","id":"87e34708-d6c6-11ec-9f5b-9391e7be2463","first_name":"Marek"},{"full_name":"Mühlböck, Fabian","orcid":"0000-0003-1548-0177","last_name":"Mühlböck","first_name":"Fabian","id":"6395C5F6-89DF-11E9-9C97-6BDFE5697425"},{"first_name":"Stefanie","id":"a376de31-8972-11ed-ae7b-d0251c13c8ff","full_name":"Muroya Lei, Stefanie","last_name":"Muroya Lei"},{"id":"40876CD8-F248-11E8-B48F-1D18A9856A87","first_name":"Thomas A","full_name":"Henzinger, Thomas A","orcid":"0000-0002-2985-7724","last_name":"Henzinger"}],"article_processing_charge":"No","title":"VAMOS: Middleware for Best-Effort Third-Party Monitoring","project":[{"_id":"62781420-2b32-11ec-9570-8d9b63373d4d","call_identifier":"H2020","grant_number":"101020093","name":"Vigilant Algorithmic Monitoring of Software"}]},{"file_date_updated":"2023-06-19T08:29:30Z","department":[{"_id":"KrCh"},{"_id":"ToHe"}],"date_updated":"2023-06-19T08:30:54Z","ddc":["000"],"tmp":{"legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","image":"/images/cc_by.png","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","short":"CC BY (4.0)"},"conference":{"start_date":"2023-04-22","end_date":"2023-04-27","location":"Paris, France","name":"TACAS: Tools and Algorithms for the Construction and Analysis of Systems"},"type":"conference","status":"public","_id":"13142","ec_funded":1,"volume":13993,"publication_status":"published","publication_identifier":{"eissn":["1611-3349"],"isbn":["9783031308222"],"issn":["0302-9743"]},"language":[{"iso":"eng"}],"file":[{"date_created":"2023-06-19T08:29:30Z","file_name":"2023_LNCS_Chatterjee.pdf","date_updated":"2023-06-19T08:29:30Z","file_size":528455,"creator":"dernst","file_id":"13150","checksum":"3d8a8bb24d211bc83360dfc2fd744307","success":1,"content_type":"application/pdf","access_level":"open_access","relation":"main_file"}],"alternative_title":["LNCS"],"scopus_import":"1","intvolume":" 13993","month":"04","abstract":[{"text":"Reinforcement learning has received much attention for learning controllers of deterministic systems. We consider a learner-verifier framework for stochastic control systems and survey recent methods that formally guarantee a conjunction of reachability and safety properties. Given a property and a lower bound on the probability of the property being satisfied, our framework jointly learns a control policy and a formal certificate to ensure the satisfaction of the property with a desired probability threshold. Both the control policy and the formal certificate are continuous functions from states to reals, which are learned as parameterized neural networks. While in the deterministic case, the certificates are invariant and barrier functions for safety, or Lyapunov and ranking functions for liveness, in the stochastic case the certificates are supermartingales. For certificate verification, we use interval arithmetic abstract interpretation to bound the expected values of neural network functions.","lang":"eng"}],"oa_version":"Published Version","article_processing_charge":"No","author":[{"first_name":"Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-4561-241X","full_name":"Chatterjee, Krishnendu","last_name":"Chatterjee"},{"full_name":"Henzinger, Thomas A","orcid":"0000-0002-2985-7724","last_name":"Henzinger","first_name":"Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87"},{"first_name":"Mathias","id":"3DC22916-F248-11E8-B48F-1D18A9856A87","last_name":"Lechner","full_name":"Lechner, Mathias"},{"full_name":"Zikelic, Dorde","last_name":"Zikelic","first_name":"Dorde","id":"294AA7A6-F248-11E8-B48F-1D18A9856A87"}],"title":"A learner-verifier framework for neural network controllers and certificates of stochastic systems","citation":{"ista":"Chatterjee K, Henzinger TA, Lechner M, Zikelic D. 2023. A learner-verifier framework for neural network controllers and certificates of stochastic systems. Tools and Algorithms for the Construction and Analysis of Systems . TACAS: Tools and Algorithms for the Construction and Analysis of Systems, LNCS, vol. 13993, 3–25.","chicago":"Chatterjee, Krishnendu, Thomas A Henzinger, Mathias Lechner, and Dorde Zikelic. “A Learner-Verifier Framework for Neural Network Controllers and Certificates of Stochastic Systems.” In Tools and Algorithms for the Construction and Analysis of Systems , 13993:3–25. Springer Nature, 2023. https://doi.org/10.1007/978-3-031-30823-9_1.","ieee":"K. Chatterjee, T. A. Henzinger, M. Lechner, and D. Zikelic, “A learner-verifier framework for neural network controllers and certificates of stochastic systems,” in Tools and Algorithms for the Construction and Analysis of Systems , Paris, France, 2023, vol. 13993, pp. 3–25.","short":"K. Chatterjee, T.A. Henzinger, M. Lechner, D. Zikelic, in:, Tools and Algorithms for the Construction and Analysis of Systems , Springer Nature, 2023, pp. 3–25.","ama":"Chatterjee K, Henzinger TA, Lechner M, Zikelic D. A learner-verifier framework for neural network controllers and certificates of stochastic systems. In: Tools and Algorithms for the Construction and Analysis of Systems . Vol 13993. Springer Nature; 2023:3-25. doi:10.1007/978-3-031-30823-9_1","apa":"Chatterjee, K., Henzinger, T. A., Lechner, M., & Zikelic, D. (2023). A learner-verifier framework for neural network controllers and certificates of stochastic systems. In Tools and Algorithms for the Construction and Analysis of Systems (Vol. 13993, pp. 3–25). Paris, France: Springer Nature. https://doi.org/10.1007/978-3-031-30823-9_1","mla":"Chatterjee, Krishnendu, et al. “A Learner-Verifier Framework for Neural Network Controllers and Certificates of Stochastic Systems.” Tools and Algorithms for the Construction and Analysis of Systems , vol. 13993, Springer Nature, 2023, pp. 3–25, doi:10.1007/978-3-031-30823-9_1."},"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","project":[{"grant_number":"863818","name":"Formal Methods for Stochastic Models: Algorithms and Applications","_id":"0599E47C-7A3F-11EA-A408-12923DDC885E","call_identifier":"H2020"},{"name":"International IST Doctoral Program","grant_number":"665385","call_identifier":"H2020","_id":"2564DBCA-B435-11E9-9278-68D0E5697425"}],"page":"3-25","date_created":"2023-06-18T22:00:47Z","date_published":"2023-04-22T00:00:00Z","doi":"10.1007/978-3-031-30823-9_1","year":"2023","has_accepted_license":"1","publication":"Tools and Algorithms for the Construction and Analysis of Systems ","day":"22","oa":1,"publisher":"Springer Nature","quality_controlled":"1","acknowledgement":"This work was supported in part by the ERC-2020-AdG 101020093, ERC CoG 863818 (FoRM-SMArt) and the European Union’s Horizon 2020 research and innovation programme under the Marie Skłodowska-Curie Grant Agreement No. 665385."},{"page":"211-228","date_created":"2023-06-18T22:00:47Z","date_published":"2023-04-20T00:00:00Z","doi":"10.1007/978-3-031-30820-8_15","year":"2023","has_accepted_license":"1","publication":"TACAS 2023: Tools and Algorithms for the Construction and Analysis of Systems","day":"20","oa":1,"quality_controlled":"1","publisher":"Springer Nature","article_processing_charge":"No","author":[{"last_name":"Anand","full_name":"Anand, Ashwani","first_name":"Ashwani"},{"last_name":"Mallik","full_name":"Mallik, Kaushik","orcid":"0000-0001-9864-7475","first_name":"Kaushik","id":"0834ff3c-6d72-11ec-94e0-b5b0a4fb8598"},{"first_name":"Satya Prakash","last_name":"Nayak","full_name":"Nayak, Satya Prakash"},{"first_name":"Anne Kathrin","full_name":"Schmuck, Anne Kathrin","last_name":"Schmuck"}],"title":"Computing adequately permissive assumptions for synthesis","citation":{"short":"A. Anand, K. Mallik, S.P. Nayak, A.K. Schmuck, in:, TACAS 2023: Tools and Algorithms for the Construction and Analysis of Systems, Springer Nature, 2023, pp. 211–228.","ieee":"A. Anand, K. Mallik, S. P. Nayak, and A. K. Schmuck, “Computing adequately permissive assumptions for synthesis,” in TACAS 2023: Tools and Algorithms for the Construction and Analysis of Systems, Paris, France, 2023, vol. 13994, pp. 211–228.","apa":"Anand, A., Mallik, K., Nayak, S. P., & Schmuck, A. K. (2023). Computing adequately permissive assumptions for synthesis. In TACAS 2023: Tools and Algorithms for the Construction and Analysis of Systems (Vol. 13994, pp. 211–228). Paris, France: Springer Nature. https://doi.org/10.1007/978-3-031-30820-8_15","ama":"Anand A, Mallik K, Nayak SP, Schmuck AK. Computing adequately permissive assumptions for synthesis. In: TACAS 2023: Tools and Algorithms for the Construction and Analysis of Systems. Vol 13994. Springer Nature; 2023:211-228. doi:10.1007/978-3-031-30820-8_15","mla":"Anand, Ashwani, et al. “Computing Adequately Permissive Assumptions for Synthesis.” TACAS 2023: Tools and Algorithms for the Construction and Analysis of Systems, vol. 13994, Springer Nature, 2023, pp. 211–28, doi:10.1007/978-3-031-30820-8_15.","ista":"Anand A, Mallik K, Nayak SP, Schmuck AK. 2023. Computing adequately permissive assumptions for synthesis. TACAS 2023: Tools and Algorithms for the Construction and Analysis of Systems. TACAS: Tools and Algorithms for the Construction and Analysis of Systems, LNCS, vol. 13994, 211–228.","chicago":"Anand, Ashwani, Kaushik Mallik, Satya Prakash Nayak, and Anne Kathrin Schmuck. “Computing Adequately Permissive Assumptions for Synthesis.” In TACAS 2023: Tools and Algorithms for the Construction and Analysis of Systems, 13994:211–28. Springer Nature, 2023. https://doi.org/10.1007/978-3-031-30820-8_15."},"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","volume":13994,"publication_status":"published","publication_identifier":{"issn":["0302-9743"],"isbn":["9783031308192"],"eissn":["1611-3349"]},"language":[{"iso":"eng"}],"file":[{"date_created":"2023-06-19T08:43:21Z","file_name":"2023_LNCS_Anand.pdf","creator":"dernst","date_updated":"2023-06-19T08:43:21Z","file_size":521425,"checksum":"60dcafc1b4f6f070be43bad3fe877974","file_id":"13151","success":1,"access_level":"open_access","relation":"main_file","content_type":"application/pdf"}],"scopus_import":"1","alternative_title":["LNCS"],"intvolume":" 13994","month":"04","abstract":[{"text":"We automatically compute a new class of environment assumptions in two-player turn-based finite graph games which characterize an “adequate cooperation” needed from the environment to allow the system player to win. Given an ω-regular winning condition Φ for the system player, we compute an ω-regular assumption Ψ for the environment player, such that (i) every environment strategy compliant with Ψ allows the system to fulfill Φ (sufficiency), (ii) Ψ\r\n can be fulfilled by the environment for every strategy of the system (implementability), and (iii) Ψ does not prevent any cooperative strategy choice (permissiveness).\r\nFor parity games, which are canonical representations of ω-regular games, we present a polynomial-time algorithm for the symbolic computation of adequately permissive assumptions and show that our algorithm runs faster and produces better assumptions than existing approaches—both theoretically and empirically. To the best of our knowledge, for ω\r\n-regular games, we provide the first algorithm to compute sufficient and implementable environment assumptions that are also permissive.","lang":"eng"}],"oa_version":"Published Version","file_date_updated":"2023-06-19T08:43:21Z","department":[{"_id":"ToHe"}],"date_updated":"2023-06-19T08:49:46Z","ddc":["000"],"tmp":{"legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","image":"/images/cc_by.png","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","short":"CC BY (4.0)"},"conference":{"start_date":"2023-04-22","end_date":"2023-04-27","location":"Paris, France","name":"TACAS: Tools and Algorithms for the Construction and Analysis of Systems"},"type":"conference","status":"public","_id":"13141"},{"department":[{"_id":"GradSch"},{"_id":"ToHe"}],"file_date_updated":"2023-06-19T10:28:09Z","date_updated":"2023-07-14T11:20:27Z","ddc":["000"],"tmp":{"legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","image":"/images/cc_by.png","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","short":"CC BY (4.0)"},"conference":{"name":"FOSSACS: Foundations of Software Science and Computation Structures","location":"Paris, France","end_date":"2023-04-27","start_date":"2023-04-22"},"type":"conference","status":"public","_id":"12467","ec_funded":1,"volume":13992,"publication_status":"published","publication_identifier":{"issn":["0302-9743"],"eissn":["1611-3349"],"isbn":["9783031308284"]},"language":[{"iso":"eng"}],"file":[{"date_created":"2023-01-31T07:22:21Z","file_name":"qsl.pdf","date_updated":"2023-01-31T07:22:21Z","file_size":449027,"creator":"esarac","file_id":"12468","checksum":"981025aed580b6b27c426cb8856cf63e","success":1,"content_type":"application/pdf","access_level":"open_access","relation":"main_file"},{"file_size":1048171,"date_updated":"2023-06-19T10:28:09Z","creator":"dernst","file_name":"2023_LNCS_HenzingerT.pdf","date_created":"2023-06-19T10:28:09Z","content_type":"application/pdf","relation":"main_file","access_level":"open_access","success":1,"checksum":"f16e2af1e0eb243158ab0f0fe74e7d5a","file_id":"13153"}],"alternative_title":["LNCS"],"scopus_import":"1","intvolume":" 13992","month":"04","abstract":[{"text":"Safety and liveness are elementary concepts of computation, and the foundation of many verification paradigms. The safety-liveness classification of boolean properties characterizes whether a given property can be falsified by observing a finite prefix of an infinite computation trace (always for safety, never for liveness). In quantitative specification and verification, properties assign not truth values, but quantitative values to infinite traces (e.g., a cost, or the distance to a boolean property). We introduce quantitative safety and liveness, and we prove that our definitions induce conservative quantitative generalizations of both (1)~the safety-progress hierarchy of boolean properties and (2)~the safety-liveness decomposition of boolean properties. In particular, we show that every quantitative property can be written as the pointwise minimum of a quantitative safety property and a quantitative liveness property. Consequently, like boolean properties, also quantitative properties can be min-decomposed into safety and liveness parts, or alternatively, max-decomposed into co-safety and co-liveness parts. Moreover, quantitative properties can be approximated naturally. We prove that every quantitative property that has both safe and co-safe approximations can be monitored arbitrarily precisely by a monitor that uses only a finite number of states.","lang":"eng"}],"oa_version":"Published Version","external_id":{"arxiv":["2301.11175"]},"article_processing_charge":"No","author":[{"last_name":"Henzinger","full_name":"Henzinger, Thomas A","orcid":"0000-0002-2985-7724","first_name":"Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87"},{"full_name":"Mazzocchi, Nicolas Adrien","last_name":"Mazzocchi","first_name":"Nicolas Adrien","id":"b26baa86-3308-11ec-87b0-8990f34baa85"},{"full_name":"Sarac, Naci E","last_name":"Sarac","first_name":"Naci E","id":"8C6B42F8-C8E6-11E9-A03A-F2DCE5697425"}],"title":"Quantitative safety and liveness","citation":{"ama":"Henzinger TA, Mazzocchi NA, Sarac NE. Quantitative safety and liveness. In: 26th International Conference Foundations of Software Science and Computation Structures. Vol 13992. Springer Nature; 2023:349-370. doi:10.1007/978-3-031-30829-1_17","apa":"Henzinger, T. A., Mazzocchi, N. A., & Sarac, N. E. (2023). Quantitative safety and liveness. In 26th International Conference Foundations of Software Science and Computation Structures (Vol. 13992, pp. 349–370). Paris, France: Springer Nature. https://doi.org/10.1007/978-3-031-30829-1_17","ieee":"T. A. Henzinger, N. A. Mazzocchi, and N. E. Sarac, “Quantitative safety and liveness,” in 26th International Conference Foundations of Software Science and Computation Structures, Paris, France, 2023, vol. 13992, pp. 349–370.","short":"T.A. Henzinger, N.A. Mazzocchi, N.E. Sarac, in:, 26th International Conference Foundations of Software Science and Computation Structures, Springer Nature, 2023, pp. 349–370.","mla":"Henzinger, Thomas A., et al. “Quantitative Safety and Liveness.” 26th International Conference Foundations of Software Science and Computation Structures, vol. 13992, Springer Nature, 2023, pp. 349–70, doi:10.1007/978-3-031-30829-1_17.","ista":"Henzinger TA, Mazzocchi NA, Sarac NE. 2023. Quantitative safety and liveness. 26th International Conference Foundations of Software Science and Computation Structures. FOSSACS: Foundations of Software Science and Computation Structures, LNCS, vol. 13992, 349–370.","chicago":"Henzinger, Thomas A, Nicolas Adrien Mazzocchi, and Naci E Sarac. “Quantitative Safety and Liveness.” In 26th International Conference Foundations of Software Science and Computation Structures, 13992:349–70. Springer Nature, 2023. https://doi.org/10.1007/978-3-031-30829-1_17."},"user_id":"8b945eb4-e2f2-11eb-945a-df72226e66a9","project":[{"_id":"62781420-2b32-11ec-9570-8d9b63373d4d","call_identifier":"H2020","grant_number":"101020093","name":"Vigilant Algorithmic Monitoring of Software"}],"page":"349-370","date_created":"2023-01-31T07:23:56Z","doi":"10.1007/978-3-031-30829-1_17","date_published":"2023-04-21T00:00:00Z","year":"2023","has_accepted_license":"1","publication":"26th International Conference Foundations of Software Science and Computation Structures","day":"21","oa":1,"publisher":"Springer Nature","quality_controlled":"1","acknowledgement":"We thank the anonymous reviewers for their helpful comments. This work was supported in part by the ERC-2020-AdG 101020093."},{"doi":"10.4230/LIPIcs.ICALP.2023.129","date_published":"2023-07-05T00:00:00Z","date_created":"2023-07-24T15:11:41Z","page":"129:1--129:20","day":"05","publication":"50th International Colloquium on Automata, Languages, and Programming","has_accepted_license":"1","year":"2023","publisher":"Schloss Dagstuhl - Leibniz-Zentrum für Informatik","quality_controlled":"1","oa":1,"acknowledgement":"This work was supported in part by the ERC-2020-AdG 101020093.\r\nWe thank Pierre Ganty for early discussions and the anonymous reviewers for their helpful comments.\r\n","title":"Regular methods for operator precedence languages","author":[{"id":"40876CD8-F248-11E8-B48F-1D18A9856A87","first_name":"Thomas A","orcid":"0000-0002-2985-7724","full_name":"Henzinger, Thomas A","last_name":"Henzinger"},{"last_name":"Kebis","full_name":"Kebis, Pavol","first_name":"Pavol"},{"id":"b26baa86-3308-11ec-87b0-8990f34baa85","first_name":"Nicolas Adrien","last_name":"Mazzocchi","full_name":"Mazzocchi, Nicolas Adrien"},{"id":"8C6B42F8-C8E6-11E9-A03A-F2DCE5697425","first_name":"Naci E","last_name":"Sarac","full_name":"Sarac, Naci E"}],"article_processing_charge":"Yes","external_id":{"arxiv":["2305.03447"]},"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","citation":{"mla":"Henzinger, Thomas A., et al. “Regular Methods for Operator Precedence Languages.” 50th International Colloquium on Automata, Languages, and Programming, vol. 261, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2023, p. 129:1--129:20, doi:10.4230/LIPIcs.ICALP.2023.129.","apa":"Henzinger, T. A., Kebis, P., Mazzocchi, N. A., & Sarac, N. E. (2023). Regular methods for operator precedence languages. In 50th International Colloquium on Automata, Languages, and Programming (Vol. 261, p. 129:1--129:20). Paderborn, Germany: Schloss Dagstuhl - Leibniz-Zentrum für Informatik. https://doi.org/10.4230/LIPIcs.ICALP.2023.129","ama":"Henzinger TA, Kebis P, Mazzocchi NA, Sarac NE. Regular methods for operator precedence languages. In: 50th International Colloquium on Automata, Languages, and Programming. Vol 261. Schloss Dagstuhl - Leibniz-Zentrum für Informatik; 2023:129:1--129:20. doi:10.4230/LIPIcs.ICALP.2023.129","short":"T.A. Henzinger, P. Kebis, N.A. Mazzocchi, N.E. Sarac, in:, 50th International Colloquium on Automata, Languages, and Programming, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2023, p. 129:1--129:20.","ieee":"T. A. Henzinger, P. Kebis, N. A. Mazzocchi, and N. E. Sarac, “Regular methods for operator precedence languages,” in 50th International Colloquium on Automata, Languages, and Programming, Paderborn, Germany, 2023, vol. 261, p. 129:1--129:20.","chicago":"Henzinger, Thomas A, Pavol Kebis, Nicolas Adrien Mazzocchi, and Naci E Sarac. “Regular Methods for Operator Precedence Languages.” In 50th International Colloquium on Automata, Languages, and Programming, 261:129:1--129:20. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2023. https://doi.org/10.4230/LIPIcs.ICALP.2023.129.","ista":"Henzinger TA, Kebis P, Mazzocchi NA, Sarac NE. 2023. Regular methods for operator precedence languages. 50th International Colloquium on Automata, Languages, and Programming. ICALP: International Colloquium on Automata, Languages, and Programming, LIPIcs, vol. 261, 129:1--129:20."},"project":[{"_id":"62781420-2b32-11ec-9570-8d9b63373d4d","call_identifier":"H2020","name":"Vigilant Algorithmic Monitoring of Software","grant_number":"101020093"}],"volume":261,"ec_funded":1,"file":[{"file_name":"icalp23.pdf","date_created":"2023-07-24T15:11:05Z","file_size":859379,"date_updated":"2023-07-24T15:11:05Z","creator":"esarac","success":1,"file_id":"13293","checksum":"5d4c8932ef3450615a53b9bb15d92eb2","content_type":"application/pdf","relation":"main_file","access_level":"open_access"}],"language":[{"iso":"eng"}],"publication_identifier":{"isbn":["9783959772785"],"eissn":["1868-8969"]},"publication_status":"published","month":"07","intvolume":" 261","alternative_title":["LIPIcs"],"oa_version":"Published Version","abstract":[{"lang":"eng","text":"The operator precedence languages (OPLs) represent the largest known subclass of the context-free languages which enjoys all desirable closure and decidability properties. This includes the decidability of language inclusion, which is the ultimate verification problem. Operator precedence grammars, automata, and logics have been investigated and used, for example, to verify programs with arithmetic expressions and exceptions (both of which are deterministic pushdown but lie outside the scope of the visibly pushdown languages). In this paper, we complete the picture and give, for the first time, an algebraic characterization of the class of OPLs in the form of a syntactic congruence that has finitely many equivalence classes exactly for the operator precedence languages. This is a generalization of the celebrated Myhill-Nerode theorem for the regular languages to OPLs. As one of the consequences, we show that universality and language inclusion for nondeterministic operator precedence automata can be solved by an antichain algorithm. Antichain algorithms avoid determinization and complementation through an explicit subset construction, by leveraging a quasi-order on words, which allows the pruning of the search space for counterexample words without sacrificing completeness. Antichain algorithms can be implemented symbolically, and these implementations are today the best-performing algorithms in practice for the inclusion of finite automata. We give a generic construction of the quasi-order needed for antichain algorithms from a finite syntactic congruence. This yields the first antichain algorithm for OPLs, an algorithm that solves the ExpTime-hard language inclusion problem for OPLs in exponential time."}],"department":[{"_id":"GradSch"},{"_id":"ToHe"}],"file_date_updated":"2023-07-24T15:11:05Z","ddc":["000"],"date_updated":"2023-07-31T08:38:38Z","status":"public","type":"conference","conference":{"name":"ICALP: International Colloquium on Automata, Languages, and Programming","location":"Paderborn, Germany","end_date":"2023-07-14","start_date":"2023-07-10"},"tmp":{"legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","image":"/images/cc_by.png","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","short":"CC BY (4.0)"},"_id":"13292"},{"citation":{"mla":"Lechner, Mathias, et al. “Revisiting the Adversarial Robustness-Accuracy Tradeoff in Robot Learning.” IEEE Robotics and Automation Letters, vol. 8, no. 3, Institute of Electrical and Electronics Engineers, 2023, pp. 1595–602, doi:10.1109/LRA.2023.3240930.","ieee":"M. Lechner, A. Amini, D. Rus, and T. A. Henzinger, “Revisiting the adversarial robustness-accuracy tradeoff in robot learning,” IEEE Robotics and Automation Letters, vol. 8, no. 3. Institute of Electrical and Electronics Engineers, pp. 1595–1602, 2023.","short":"M. Lechner, A. Amini, D. Rus, T.A. Henzinger, IEEE Robotics and Automation Letters 8 (2023) 1595–1602.","apa":"Lechner, M., Amini, A., Rus, D., & Henzinger, T. A. (2023). Revisiting the adversarial robustness-accuracy tradeoff in robot learning. IEEE Robotics and Automation Letters. Institute of Electrical and Electronics Engineers. https://doi.org/10.1109/LRA.2023.3240930","ama":"Lechner M, Amini A, Rus D, Henzinger TA. Revisiting the adversarial robustness-accuracy tradeoff in robot learning. IEEE Robotics and Automation Letters. 2023;8(3):1595-1602. doi:10.1109/LRA.2023.3240930","chicago":"Lechner, Mathias, Alexander Amini, Daniela Rus, and Thomas A Henzinger. “Revisiting the Adversarial Robustness-Accuracy Tradeoff in Robot Learning.” IEEE Robotics and Automation Letters. Institute of Electrical and Electronics Engineers, 2023. https://doi.org/10.1109/LRA.2023.3240930.","ista":"Lechner M, Amini A, Rus D, Henzinger TA. 2023. Revisiting the adversarial robustness-accuracy tradeoff in robot learning. IEEE Robotics and Automation Letters. 8(3), 1595–1602."},"user_id":"4359f0d1-fa6c-11eb-b949-802e58b17ae8","author":[{"id":"3DC22916-F248-11E8-B48F-1D18A9856A87","first_name":"Mathias","last_name":"Lechner","full_name":"Lechner, Mathias"},{"last_name":"Amini","full_name":"Amini, Alexander","first_name":"Alexander"},{"first_name":"Daniela","last_name":"Rus","full_name":"Rus, Daniela"},{"last_name":"Henzinger","full_name":"Henzinger, Thomas A","orcid":"0000-0002-2985-7724","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","first_name":"Thomas A"}],"external_id":{"isi":["000936534100012"],"arxiv":["2204.07373"]},"article_processing_charge":"No","title":"Revisiting the adversarial robustness-accuracy tradeoff in robot learning","has_accepted_license":"1","isi":1,"year":"2023","day":"01","publication":"IEEE Robotics and Automation Letters","page":"1595-1602","doi":"10.1109/LRA.2023.3240930","date_published":"2023-03-01T00:00:00Z","date_created":"2023-03-05T23:01:04Z","acknowledgement":"We thank Christoph Lampert for inspiring this work. The\r\nviews and conclusions contained in this document are those of\r\nthe authors and should not be interpreted as representing the\r\nofficial policies, either expressed or implied, of the United States\r\nAir Force or the U.S. Government. The U.S. Government is\r\nauthorized to reproduce and distribute reprints for Government\r\npurposes notwithstanding any copyright notation herein.","publisher":"Institute of Electrical and Electronics Engineers","quality_controlled":"1","oa":1,"date_updated":"2023-08-01T13:36:50Z","ddc":["000"],"department":[{"_id":"ToHe"}],"file_date_updated":"2023-03-07T12:22:23Z","_id":"12704","type":"journal_article","article_type":"original","tmp":{"legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","image":"/images/cc_by.png","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","short":"CC BY (4.0)"},"status":"public","publication_identifier":{"eissn":["2377-3766"]},"publication_status":"published","file":[{"checksum":"5a75dcd326ea66685de2b1aaec259e85","file_id":"12714","success":1,"access_level":"open_access","relation":"main_file","content_type":"application/pdf","date_created":"2023-03-07T12:22:23Z","file_name":"2023_IEEERobAutLetters_Lechner.pdf","creator":"cchlebak","date_updated":"2023-03-07T12:22:23Z","file_size":944052}],"language":[{"iso":"eng"}],"issue":"3","related_material":{"record":[{"relation":"earlier_version","id":"11366","status":"public"}]},"volume":8,"abstract":[{"text":"Adversarial training (i.e., training on adversarially perturbed input data) is a well-studied method for making neural networks robust to potential adversarial attacks during inference. However, the improved robustness does not come for free but rather is accompanied by a decrease in overall model accuracy and performance. Recent work has shown that, in practical robot learning applications, the effects of adversarial training do not pose a fair trade-off but inflict a net loss when measured in holistic robot performance. This work revisits the robustness-accuracy trade-off in robot learning by systematically analyzing if recent advances in robust training methods and theory in conjunction with adversarial robot learning, are capable of making adversarial training suitable for real-world robot applications. We evaluate three different robot learning tasks ranging from autonomous driving in a high-fidelity environment amenable to sim-to-real deployment to mobile robot navigation and gesture recognition. Our results demonstrate that, while these techniques make incremental improvements on the trade-off on a relative scale, the negative impact on the nominal accuracy caused by adversarial training still outweighs the improved robustness by an order of magnitude. We conclude that although progress is happening, further advances in robust learning methods are necessary before they can benefit robot learning tasks in practice.","lang":"eng"}],"oa_version":"Published Version","scopus_import":"1","month":"03","intvolume":" 8"},{"title":"Boolean network sketches: A unifying framework for logical model inference","article_processing_charge":"No","external_id":{"isi":["000976610800001"],"pmid":["37004199"]},"author":[{"first_name":"Nikola","last_name":"Beneš","full_name":"Beneš, Nikola"},{"full_name":"Brim, Luboš","last_name":"Brim","first_name":"Luboš"},{"last_name":"Huvar","full_name":"Huvar, Ondřej","first_name":"Ondřej"},{"first_name":"Samuel","id":"07c5ea74-f61c-11ec-a664-aa7c5d957b2b","full_name":"Pastva, Samuel","last_name":"Pastva"},{"first_name":"David","full_name":"Šafránek, David","last_name":"Šafránek"}],"user_id":"4359f0d1-fa6c-11eb-b949-802e58b17ae8","citation":{"chicago":"Beneš, Nikola, Luboš Brim, Ondřej Huvar, Samuel Pastva, and David Šafránek. “Boolean Network Sketches: A Unifying Framework for Logical Model Inference.” Bioinformatics. Oxford Academic, 2023. https://doi.org/10.1093/bioinformatics/btad158.","ista":"Beneš N, Brim L, Huvar O, Pastva S, Šafránek D. 2023. Boolean network sketches: A unifying framework for logical model inference. Bioinformatics. 39(4), btad158.","mla":"Beneš, Nikola, et al. “Boolean Network Sketches: A Unifying Framework for Logical Model Inference.” Bioinformatics, vol. 39, no. 4, btad158, Oxford Academic, 2023, doi:10.1093/bioinformatics/btad158.","ieee":"N. Beneš, L. Brim, O. Huvar, S. Pastva, and D. Šafránek, “Boolean network sketches: A unifying framework for logical model inference,” Bioinformatics, vol. 39, no. 4. Oxford Academic, 2023.","short":"N. Beneš, L. Brim, O. Huvar, S. Pastva, D. Šafránek, Bioinformatics 39 (2023).","ama":"Beneš N, Brim L, Huvar O, Pastva S, Šafránek D. Boolean network sketches: A unifying framework for logical model inference. Bioinformatics. 2023;39(4). doi:10.1093/bioinformatics/btad158","apa":"Beneš, N., Brim, L., Huvar, O., Pastva, S., & Šafránek, D. (2023). Boolean network sketches: A unifying framework for logical model inference. Bioinformatics. Oxford Academic. https://doi.org/10.1093/bioinformatics/btad158"},"project":[{"_id":"fc2ed2f7-9c52-11eb-aca3-c01059dda49c","call_identifier":"H2020","name":"IST-BRIDGE: International postdoctoral program","grant_number":"101034413"}],"article_number":"btad158","date_created":"2023-04-30T22:01:05Z","date_published":"2023-04-03T00:00:00Z","doi":"10.1093/bioinformatics/btad158","publication":"Bioinformatics","day":"03","year":"2023","has_accepted_license":"1","isi":1,"oa":1,"publisher":"Oxford Academic","quality_controlled":"1","acknowledgement":"This work was partially supported by GACR [grant No. GA22-10845S]; and Grant Agency of Masaryk University [grant No. MUNI/G/1771/2020]. This work was partially supported by European Union’s Horizon 2020 research and innovation programme under the Marie Skłodowska-Curie [Grant Agreement No. 101034413 to S.P.].","file_date_updated":"2023-05-02T07:39:04Z","department":[{"_id":"ToHe"}],"ddc":["000"],"date_updated":"2023-08-01T14:27:28Z","status":"public","tmp":{"legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","image":"/images/cc_by.png","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","short":"CC BY (4.0)"},"type":"journal_article","article_type":"original","_id":"12876","ec_funded":1,"issue":"4","volume":39,"related_material":{"link":[{"relation":"software","url":"https://doi.org/10.5281/zenodo.7688740"}]},"language":[{"iso":"eng"}],"file":[{"content_type":"application/pdf","access_level":"open_access","relation":"main_file","file_id":"12886","checksum":"2cb90ddf781baefddf47eac4b54e2a03","success":1,"date_updated":"2023-05-02T07:39:04Z","file_size":478740,"creator":"dernst","date_created":"2023-05-02T07:39:04Z","file_name":"2023_Bioinformatics_Benes.pdf"}],"publication_status":"published","publication_identifier":{"eissn":["1367-4811"]},"intvolume":" 39","month":"04","scopus_import":"1","pmid":1,"oa_version":"Published Version","abstract":[{"text":"Motivation: The problem of model inference is of fundamental importance to systems biology. Logical models (e.g. Boolean networks; BNs) represent a computationally attractive approach capable of handling large biological networks. The models are typically inferred from experimental data. However, even with a substantial amount of experimental data supported by some prior knowledge, existing inference methods often focus on a small sample of admissible candidate models only.\r\n\r\nResults: We propose Boolean network sketches as a new formal instrument for the inference of Boolean networks. A sketch integrates (typically partial) knowledge about the network’s topology and the update logic (obtained through, e.g. a biological knowledge base or a literature search), as well as further assumptions about the properties of the network’s transitions (e.g. the form of its attractor landscape), and additional restrictions on the model dynamics given by the measured experimental data. Our new BNs inference algorithm starts with an ‘initial’ sketch, which is extended by adding restrictions representing experimental data to a ‘data-informed’ sketch and subsequently computes all BNs consistent with the data-informed sketch. Our algorithm is based on a symbolic representation and coloured model-checking. Our approach is unique in its ability to cover a broad spectrum of knowledge and efficiently produce a compact representation of all inferred BNs. We evaluate the method on a non-trivial collection of real-world and simulated data.","lang":"eng"}]},{"language":[{"iso":"eng"}],"publication_identifier":{"isbn":["9781577358800"]},"publication_status":"published","volume":37,"issue":"12","ec_funded":1,"oa_version":"Preprint","abstract":[{"lang":"eng","text":"We study the problem of training and certifying adversarially robust quantized neural networks (QNNs). Quantization is a technique for making neural networks more efficient by running them using low-bit integer arithmetic and is therefore commonly adopted in industry. Recent work has shown that floating-point neural networks that have been verified to be robust can become vulnerable to adversarial attacks after quantization, and certification of the quantized representation is necessary to guarantee robustness. In this work, we present quantization-aware interval bound propagation (QA-IBP), a novel method for training robust QNNs. Inspired by advances in robust learning of non-quantized networks, our training algorithm computes the gradient of an abstract representation of the actual network. Unlike existing approaches, our method can handle the discrete semantics of QNNs. Based on QA-IBP, we also develop a complete verification procedure for verifying the adversarial robustness of QNNs, which is guaranteed to terminate and produce a correct answer. Compared to existing approaches, the key advantage of our verification procedure is that it runs entirely on GPU or other accelerator devices. We demonstrate experimentally that our approach significantly outperforms existing methods and establish the new state-of-the-art for training and certifying the robustness of QNNs."}],"month":"06","intvolume":" 37","scopus_import":"1","main_file_link":[{"open_access":"1","url":"https://doi.org/10.48550/arXiv.2211.16187"}],"date_updated":"2023-09-05T07:06:14Z","department":[{"_id":"ToHe"},{"_id":"KrCh"}],"_id":"14242","status":"public","type":"conference","conference":{"name":"AAAI: Conference on Artificial Intelligence","location":"Washington, DC, United States","end_date":"2023-02-14","start_date":"2023-02-07"},"day":"26","publication":"Proceedings of the 37th AAAI Conference on Artificial Intelligence","year":"2023","doi":"10.1609/aaai.v37i12.26747","date_published":"2023-06-26T00:00:00Z","date_created":"2023-08-27T22:01:17Z","page":"14964-14973","acknowledgement":"This work was supported in part by the ERC-2020-AdG 101020093, ERC CoG 863818 (FoRM-SMArt) and the European Union’s Horizon 2020 research and innovation programme under the Marie Skłodowska-Curie Grant Agreement No. 665385. Research was sponsored by the United\r\nStates Air Force Research Laboratory and the United States Air Force Artificial Intelligence Accelerator and was accomplished under Cooperative Agreement Number FA8750-19-2-\r\n1000. The views and conclusions contained in this document are those of the authors and should not be interpreted as representing the official policies, either expressed or implied,\r\nof the United States Air Force or the U.S. Government. The U.S. Government is authorized to reproduce and distribute reprints for Government purposes notwithstanding any copyright\r\nnotation herein. The research was also funded in part by the AI2050 program at Schmidt Futures (Grant G-22-63172) and Capgemini SE.","quality_controlled":"1","publisher":"Association for the Advancement of Artificial Intelligence","oa":1,"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","citation":{"chicago":"Lechner, Mathias, Dorde Zikelic, Krishnendu Chatterjee, Thomas A Henzinger, and Daniela Rus. “Quantization-Aware Interval Bound Propagation for Training Certifiably Robust Quantized Neural Networks.” In Proceedings of the 37th AAAI Conference on Artificial Intelligence, 37:14964–73. Association for the Advancement of Artificial Intelligence, 2023. https://doi.org/10.1609/aaai.v37i12.26747.","ista":"Lechner M, Zikelic D, Chatterjee K, Henzinger TA, Rus D. 2023. Quantization-aware interval bound propagation for training certifiably robust quantized neural networks. Proceedings of the 37th AAAI Conference on Artificial Intelligence. AAAI: Conference on Artificial Intelligence vol. 37, 14964–14973.","mla":"Lechner, Mathias, et al. “Quantization-Aware Interval Bound Propagation for Training Certifiably Robust Quantized Neural Networks.” Proceedings of the 37th AAAI Conference on Artificial Intelligence, vol. 37, no. 12, Association for the Advancement of Artificial Intelligence, 2023, pp. 14964–73, doi:10.1609/aaai.v37i12.26747.","ama":"Lechner M, Zikelic D, Chatterjee K, Henzinger TA, Rus D. Quantization-aware interval bound propagation for training certifiably robust quantized neural networks. In: Proceedings of the 37th AAAI Conference on Artificial Intelligence. Vol 37. Association for the Advancement of Artificial Intelligence; 2023:14964-14973. doi:10.1609/aaai.v37i12.26747","apa":"Lechner, M., Zikelic, D., Chatterjee, K., Henzinger, T. A., & Rus, D. (2023). Quantization-aware interval bound propagation for training certifiably robust quantized neural networks. In Proceedings of the 37th AAAI Conference on Artificial Intelligence (Vol. 37, pp. 14964–14973). Washington, DC, United States: Association for the Advancement of Artificial Intelligence. https://doi.org/10.1609/aaai.v37i12.26747","short":"M. Lechner, D. Zikelic, K. Chatterjee, T.A. Henzinger, D. Rus, in:, Proceedings of the 37th AAAI Conference on Artificial Intelligence, Association for the Advancement of Artificial Intelligence, 2023, pp. 14964–14973.","ieee":"M. Lechner, D. Zikelic, K. Chatterjee, T. A. Henzinger, and D. Rus, “Quantization-aware interval bound propagation for training certifiably robust quantized neural networks,” in Proceedings of the 37th AAAI Conference on Artificial Intelligence, Washington, DC, United States, 2023, vol. 37, no. 12, pp. 14964–14973."},"title":"Quantization-aware interval bound propagation for training certifiably robust quantized neural networks","author":[{"last_name":"Lechner","full_name":"Lechner, Mathias","id":"3DC22916-F248-11E8-B48F-1D18A9856A87","first_name":"Mathias"},{"last_name":"Zikelic","full_name":"Zikelic, Dorde","orcid":"0000-0002-4681-1699","first_name":"Dorde","id":"294AA7A6-F248-11E8-B48F-1D18A9856A87"},{"first_name":"Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-4561-241X","full_name":"Chatterjee, Krishnendu","last_name":"Chatterjee"},{"orcid":"0000-0002-2985-7724","full_name":"Henzinger, Thomas A","last_name":"Henzinger","first_name":"Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87"},{"last_name":"Rus","full_name":"Rus, Daniela","first_name":"Daniela"}],"article_processing_charge":"No","external_id":{"arxiv":["2211.16187"]},"project":[{"name":"Vigilant Algorithmic Monitoring of Software","grant_number":"101020093","call_identifier":"H2020","_id":"62781420-2b32-11ec-9570-8d9b63373d4d"},{"call_identifier":"H2020","_id":"0599E47C-7A3F-11EA-A408-12923DDC885E","name":"Formal Methods for Stochastic Models: Algorithms and Applications","grant_number":"863818"},{"_id":"2564DBCA-B435-11E9-9278-68D0E5697425","call_identifier":"H2020","name":"International IST Doctoral Program","grant_number":"665385"}]}]