[{"doi":"10.15479/AT:ISTA:12407","year":"2023","ec_funded":1,"title":"VAMOS: Middleware for Best-Effort Third-Party Monitoring","alternative_title":["IST Austria Technical Report"],"tmp":{"image":"/images/cc_by.png","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","short":"CC BY (4.0)"},"related_material":{"record":[{"status":"public","id":"12856","relation":"later_version"}]},"ddc":["005"],"publication_status":"published","citation":{"apa":"Chalupa, M., Mühlböck, F., Muroya Lei, S., &#38; Henzinger, T. A. (2023). <i>VAMOS: Middleware for Best-Effort Third-Party Monitoring</i>. Institute of Science and Technology Austria. <a href=\"https://doi.org/10.15479/AT:ISTA:12407\">https://doi.org/10.15479/AT:ISTA:12407</a>","ieee":"M. Chalupa, F. Mühlböck, S. Muroya Lei, and T. A. Henzinger, <i>VAMOS: Middleware for Best-Effort Third-Party Monitoring</i>. Institute of Science and Technology Austria, 2023.","chicago":"Chalupa, Marek, Fabian Mühlböck, Stefanie Muroya Lei, and Thomas A Henzinger. <i>VAMOS: Middleware for Best-Effort Third-Party Monitoring</i>. Institute of Science and Technology Austria, 2023. <a href=\"https://doi.org/10.15479/AT:ISTA:12407\">https://doi.org/10.15479/AT:ISTA:12407</a>.","ama":"Chalupa M, Mühlböck F, Muroya Lei S, Henzinger TA. <i>VAMOS: Middleware for Best-Effort Third-Party Monitoring</i>. Institute of Science and Technology Austria; 2023. doi:<a href=\"https://doi.org/10.15479/AT:ISTA:12407\">10.15479/AT:ISTA:12407</a>","mla":"Chalupa, Marek, et al. <i>VAMOS: Middleware for Best-Effort Third-Party Monitoring</i>. Institute of Science and Technology Austria, 2023, doi:<a href=\"https://doi.org/10.15479/AT:ISTA:12407\">10.15479/AT:ISTA:12407</a>.","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.","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."},"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"}],"keyword":["runtime monitoring","best effort","third party"],"author":[{"id":"87e34708-d6c6-11ec-9f5b-9391e7be2463","first_name":"Marek","full_name":"Chalupa, Marek","last_name":"Chalupa"},{"id":"6395C5F6-89DF-11E9-9C97-6BDFE5697425","first_name":"Fabian","orcid":"0000-0003-1548-0177","last_name":"Mühlböck","full_name":"Mühlböck, Fabian"},{"id":"a376de31-8972-11ed-ae7b-d0251c13c8ff","full_name":"Muroya Lei, Stefanie","last_name":"Muroya Lei","first_name":"Stefanie"},{"orcid":"0000-0002-2985-7724","full_name":"Henzinger, Thomas A","last_name":"Henzinger","first_name":"Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87"}],"oa":1,"date_updated":"2023-04-25T07:19:06Z","article_processing_charge":"No","_id":"12407","publication_identifier":{"eissn":["2664-1690"]},"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","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.","project":[{"grant_number":"101020093","_id":"62781420-2b32-11ec-9570-8d9b63373d4d","name":"Vigilant Algorithmic Monitoring of Software","call_identifier":"H2020"}],"oa_version":"Published Version","month":"01","date_published":"2023-01-27T00:00:00Z","publisher":"Institute of Science and Technology Austria","language":[{"iso":"eng"}],"license":"https://creativecommons.org/licenses/by/4.0/","has_accepted_license":"1","department":[{"_id":"ToHe"}],"date_created":"2023-01-27T03:18:08Z","file":[{"content_type":"application/pdf","relation":"main_file","creator":"fmuehlbo","file_id":"12408","success":1,"date_updated":"2023-01-27T03:18:34Z","access_level":"open_access","file_name":"main.pdf","file_size":662409,"date_created":"2023-01-27T03:18:34Z","checksum":"55426e463fdeafe9777fc3ff635154c7"}],"day":"27","type":"technical_report","status":"public","file_date_updated":"2023-01-27T03:18:34Z","page":"38"},{"tmp":{"image":"/images/cc_by.png","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","short":"CC BY (4.0)"},"alternative_title":["LNCS"],"related_material":{"record":[{"status":"public","relation":"earlier_version","id":"12407"}]},"ddc":["000"],"year":"2023","doi":"10.1007/978-3-031-30826-0_15","ec_funded":1,"title":"Vamos: Middleware for best-effort third-party monitoring","article_processing_charge":"No","oa":1,"date_updated":"2023-04-25T07:19:07Z","volume":13991,"publication_identifier":{"isbn":["9783031308253"],"issn":["0302-9743"],"eisbn":["9783031308260"],"eissn":["1611-3349"]},"_id":"12856","quality_controlled":"1","oa_version":"Published Version","project":[{"grant_number":"101020093","name":"Vigilant Algorithmic Monitoring of Software","_id":"62781420-2b32-11ec-9570-8d9b63373d4d","call_identifier":"H2020"}],"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.","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","citation":{"ama":"Chalupa M, Mühlböck F, Muroya Lei S, Henzinger TA. Vamos: Middleware for best-effort third-party monitoring. In: <i>Fundamental Approaches to Software Engineering</i>. Vol 13991. Springer Nature; 2023:260-281. doi:<a href=\"https://doi.org/10.1007/978-3-031-30826-0_15\">10.1007/978-3-031-30826-0_15</a>","mla":"Chalupa, Marek, et al. “Vamos: Middleware for Best-Effort Third-Party Monitoring.” <i>Fundamental Approaches to Software Engineering</i>, vol. 13991, Springer Nature, 2023, pp. 260–81, doi:<a href=\"https://doi.org/10.1007/978-3-031-30826-0_15\">10.1007/978-3-031-30826-0_15</a>.","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.","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.","ieee":"M. Chalupa, F. Mühlböck, S. Muroya Lei, and T. A. Henzinger, “Vamos: Middleware for best-effort third-party monitoring,” in <i>Fundamental Approaches to Software Engineering</i>, Paris, France, 2023, vol. 13991, pp. 260–281.","apa":"Chalupa, M., Mühlböck, F., Muroya Lei, S., &#38; Henzinger, T. A. (2023). Vamos: Middleware for best-effort third-party monitoring. In <i>Fundamental Approaches to Software Engineering</i> (Vol. 13991, pp. 260–281). Paris, France: Springer Nature. <a href=\"https://doi.org/10.1007/978-3-031-30826-0_15\">https://doi.org/10.1007/978-3-031-30826-0_15</a>","chicago":"Chalupa, Marek, Fabian Mühlböck, Stefanie Muroya Lei, and Thomas A Henzinger. “Vamos: Middleware for Best-Effort Third-Party Monitoring.” In <i>Fundamental Approaches to Software Engineering</i>, 13991:260–81. Springer Nature, 2023. <a href=\"https://doi.org/10.1007/978-3-031-30826-0_15\">https://doi.org/10.1007/978-3-031-30826-0_15</a>."},"publication_status":"published","abstract":[{"lang":"eng","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."}],"author":[{"last_name":"Chalupa","full_name":"Chalupa, Marek","first_name":"Marek","id":"87e34708-d6c6-11ec-9f5b-9391e7be2463"},{"full_name":"Mühlböck, Fabian","last_name":"Mühlböck","orcid":"0000-0003-1548-0177","first_name":"Fabian","id":"6395C5F6-89DF-11E9-9C97-6BDFE5697425"},{"id":"a376de31-8972-11ed-ae7b-d0251c13c8ff","last_name":"Muroya Lei","full_name":"Muroya Lei, Stefanie","first_name":"Stefanie"},{"id":"40876CD8-F248-11E8-B48F-1D18A9856A87","first_name":"Thomas A","orcid":"0000-0002-2985-7724","last_name":"Henzinger","full_name":"Henzinger, Thomas A"}],"has_accepted_license":"1","department":[{"_id":"ToHe"}],"conference":{"start_date":"2023-04-22","location":"Paris, France","name":"FASE: Fundamental Approaches to Software Engineering","end_date":"2023-04-27"},"file":[{"file_id":"12865","creator":"dernst","relation":"main_file","content_type":"application/pdf","success":1,"access_level":"open_access","date_updated":"2023-04-25T07:16:36Z","checksum":"17a7c8e08be609cf2408d37ea55e322c","date_created":"2023-04-25T07:16:36Z","file_size":580828,"file_name":"2023_LNCS_ChalupaM.pdf"}],"date_created":"2023-04-20T08:29:42Z","month":"04","date_published":"2023-04-20T00:00:00Z","publisher":"Springer Nature","language":[{"iso":"eng"}],"publication":"Fundamental Approaches to Software Engineering","page":"260-281","file_date_updated":"2023-04-25T07:16:36Z","day":"20","type":"conference","intvolume":"     13991","status":"public"},{"date_published":"2021-03-21T00:00:00Z","ec_funded":1,"doi":"10.48550/arXiv.2103.11389","month":"03","year":"2021","language":[{"iso":"eng"}],"external_id":{"arxiv":["2103.11389"]},"title":"Formal verification of Zagier's one-sentence proof","department":[{"_id":"LaEr"},{"_id":"ToHe"}],"article_number":"2103.11389","main_file_link":[{"url":"https://arxiv.org/abs/2103.11389","open_access":"1"}],"date_created":"2021-03-23T05:38:48Z","related_material":{"record":[{"id":"9946","relation":"other","status":"public"}]},"type":"preprint","publication_status":"submitted","citation":{"chicago":"Dubach, Guillaume, and Fabian Mühlböck. “Formal Verification of Zagier’s One-Sentence Proof.” <i>ArXiv</i>, n.d. <a href=\"https://doi.org/10.48550/arXiv.2103.11389\">https://doi.org/10.48550/arXiv.2103.11389</a>.","apa":"Dubach, G., &#38; Mühlböck, F. (n.d.). Formal verification of Zagier’s one-sentence proof. <i>arXiv</i>. <a href=\"https://doi.org/10.48550/arXiv.2103.11389\">https://doi.org/10.48550/arXiv.2103.11389</a>","ieee":"G. Dubach and F. Mühlböck, “Formal verification of Zagier’s one-sentence proof,” <i>arXiv</i>. .","ista":"Dubach G, Mühlböck F. Formal verification of Zagier’s one-sentence proof. arXiv, 2103.11389.","short":"G. Dubach, F. Mühlböck, ArXiv (n.d.).","ama":"Dubach G, Mühlböck F. Formal verification of Zagier’s one-sentence proof. <i>arXiv</i>. doi:<a href=\"https://doi.org/10.48550/arXiv.2103.11389\">10.48550/arXiv.2103.11389</a>","mla":"Dubach, Guillaume, and Fabian Mühlböck. “Formal Verification of Zagier’s One-Sentence Proof.” <i>ArXiv</i>, 2103.11389, doi:<a href=\"https://doi.org/10.48550/arXiv.2103.11389\">10.48550/arXiv.2103.11389</a>."},"day":"21","author":[{"first_name":"Guillaume","full_name":"Dubach, Guillaume","last_name":"Dubach","orcid":"0000-0001-6892-8137","id":"D5C6A458-10C4-11EA-ABF4-A4B43DDC885E"},{"id":"6395C5F6-89DF-11E9-9C97-6BDFE5697425","first_name":"Fabian","orcid":"0000-0003-1548-0177","last_name":"Mühlböck","full_name":"Mühlböck, Fabian"}],"status":"public","abstract":[{"lang":"eng","text":"We comment on two formal proofs of Fermat's sum of two squares theorem, written using the Mathematical Components libraries of the Coq proof assistant. The first one follows Zagier's celebrated one-sentence proof; the second follows David Christopher's recent new proof relying on partition-theoretic arguments. Both formal proofs rely on a general property of involutions of finite sets, of independent interest. The proof technique consists for the most part of automating recurrent tasks (such as case distinctions and computations on natural numbers) via ad hoc tactics."}],"oa":1,"date_updated":"2023-05-03T10:26:45Z","article_processing_charge":"No","arxiv":1,"publication":"arXiv","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","project":[{"grant_number":"754411","_id":"260C2330-B435-11E9-9278-68D0E5697425","name":"ISTplus - Postdoctoral Fellowships","call_identifier":"H2020"}],"oa_version":"Preprint","_id":"9281"},{"alternative_title":["LNCS"],"isi":1,"related_material":{"record":[{"status":"public","relation":"extended_version","id":"9946"}]},"ddc":["005"],"doi":"10.1007/978-3-030-88494-9_12","year":"2021","place":"Cham","external_id":{"isi":["000719383800012"]},"title":"Differential monitoring","oa":1,"date_updated":"2023-08-14T07:20:30Z","volume":12974,"article_processing_charge":"No","_id":"10108","publication_identifier":{"isbn":["978-3-030-88493-2"],"eisbn":["978-3-030-88494-9"],"issn":["0302-9743"],"eissn":["1611-3349"]},"user_id":"4359f0d1-fa6c-11eb-b949-802e58b17ae8","acknowledgement":"The authors would like to thank Borzoo Bonakdarpour, Derek Dreyer, Adrian Francalanza, Owolabi Legunsen, Mae Milano, Manuel Rigger, Cesar Sanchez, and the members of the IST Verification Seminar for their helpful comments and insights on various stages of this work, as well as the reviewers of RV’21 for their helpful suggestions on the actual paper.","project":[{"name":"The Wittgenstein Prize","_id":"25F42A32-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","grant_number":"Z211"}],"quality_controlled":"1","oa_version":"Preprint","publication_status":"published","citation":{"chicago":"Mühlböck, Fabian, and Thomas A Henzinger. “Differential Monitoring.” In <i>International Conference on Runtime Verification</i>, 12974:231–43. Cham: Springer Nature, 2021. <a href=\"https://doi.org/10.1007/978-3-030-88494-9_12\">https://doi.org/10.1007/978-3-030-88494-9_12</a>.","apa":"Mühlböck, F., &#38; Henzinger, T. A. (2021). Differential monitoring. In <i>International Conference on Runtime Verification</i> (Vol. 12974, pp. 231–243). Cham: Springer Nature. <a href=\"https://doi.org/10.1007/978-3-030-88494-9_12\">https://doi.org/10.1007/978-3-030-88494-9_12</a>","ieee":"F. Mühlböck and T. A. Henzinger, “Differential monitoring,” in <i>International Conference on Runtime Verification</i>, Virtual, 2021, vol. 12974, pp. 231–243.","ista":"Mühlböck F, Henzinger TA. 2021. Differential monitoring. International Conference on Runtime Verification. RV: Runtime Verification, LNCS, vol. 12974, 231–243.","short":"F. Mühlböck, T.A. Henzinger, in:, International Conference on Runtime Verification, Springer Nature, Cham, 2021, pp. 231–243.","mla":"Mühlböck, Fabian, and Thomas A. Henzinger. “Differential Monitoring.” <i>International Conference on Runtime Verification</i>, vol. 12974, Springer Nature, 2021, pp. 231–43, doi:<a href=\"https://doi.org/10.1007/978-3-030-88494-9_12\">10.1007/978-3-030-88494-9_12</a>.","ama":"Mühlböck F, Henzinger TA. Differential monitoring. In: <i>International Conference on Runtime Verification</i>. Vol 12974. Cham: Springer Nature; 2021:231-243. doi:<a href=\"https://doi.org/10.1007/978-3-030-88494-9_12\">10.1007/978-3-030-88494-9_12</a>"},"abstract":[{"text":"We argue that the time is ripe to investigate differential monitoring, in which the specification of a program's behavior is implicitly given by a second program implementing the same informal specification. Similar ideas have been proposed before, and are currently implemented in restricted form for testing and specialized run-time analyses, aspects of which we combine. We discuss the challenges of implementing differential monitoring as a general-purpose, black-box run-time monitoring framework, and present promising results of a preliminary implementation, showing low monitoring overheads for diverse programs.","lang":"eng"}],"author":[{"id":"6395C5F6-89DF-11E9-9C97-6BDFE5697425","first_name":"Fabian","full_name":"Mühlböck, Fabian","last_name":"Mühlböck","orcid":"0000-0003-1548-0177"},{"id":"40876CD8-F248-11E8-B48F-1D18A9856A87","first_name":"Thomas A","orcid":"0000-0002-2985-7724","last_name":"Henzinger","full_name":"Henzinger, Thomas A"}],"keyword":["run-time verification","software engineering","implicit specification"],"has_accepted_license":"1","department":[{"_id":"ToHe"}],"conference":{"end_date":"2021-10-14","location":"Virtual","name":"RV: Runtime Verification","start_date":"2021-10-11"},"date_created":"2021-10-07T23:30:10Z","file":[{"checksum":"554c7fdb259eda703a8b6328a6dad55a","date_created":"2021-10-07T23:32:18Z","file_size":350632,"file_name":"differentialmonitoring-cameraready-openaccess.pdf","access_level":"open_access","date_updated":"2021-10-07T23:32:18Z","success":1,"file_id":"10109","creator":"fmuehlbo","relation":"main_file","content_type":"application/pdf"}],"month":"10","date_published":"2021-10-06T00:00:00Z","publisher":"Springer Nature","scopus_import":"1","language":[{"iso":"eng"}],"publication":"International Conference on Runtime Verification","page":"231-243","file_date_updated":"2021-10-07T23:32:18Z","day":"06","type":"conference","intvolume":"     12974","status":"public"},{"file_date_updated":"2021-10-19T12:52:23Z","publication":"Proceedings of the ACM on Programming Languages","type":"journal_article","day":"15","status":"public","intvolume":"         5","department":[{"_id":"ToHe"}],"has_accepted_license":"1","license":"https://creativecommons.org/licenses/by-nd/4.0/","file":[{"success":1,"relation":"main_file","content_type":"application/pdf","creator":"fmuehlbo","file_id":"10154","file_size":770269,"file_name":"monnom-oopsla21.pdf","checksum":"71011efd2da771cafdec7f0d9693f8c1","date_created":"2021-10-19T12:52:23Z","access_level":"open_access","date_updated":"2021-10-19T12:52:23Z"}],"date_created":"2021-10-19T12:48:44Z","conference":{"start_date":"2021-10-17","name":"OOPSLA: Object-Oriented Programming, Systems, Languages, and Applications","end_date":"2021-10-23","location":"Chicago, IL, United States"},"date_published":"2021-10-15T00:00:00Z","article_type":"original","month":"10","language":[{"iso":"eng"}],"publisher":"Association for Computing Machinery","article_processing_charge":"No","date_updated":"2021-11-12T11:30:07Z","oa":1,"volume":5,"project":[{"grant_number":"Z211","call_identifier":"FWF","_id":"25F42A32-B435-11E9-9278-68D0E5697425","name":"The Wittgenstein Prize"}],"quality_controlled":"1","oa_version":"Published Version","user_id":"8b945eb4-e2f2-11eb-945a-df72226e66a9","acknowledgement":"We thank the reviewers for their valuable suggestions towards improving the paper. We also \r\nthank Mae Milano and Adrian Sampson, as well as the members of the Programming Languages Discussion Group at Cornell University and of the Programming Research Laboratory at Northeastern University, for their helpful feedback on preliminary findings of this work.\r\n\r\nThis material is based upon work supported in part by the National Science Foundation (NSF) through grant CCF-1350182 and the Austrian Science Fund (FWF) through grant Z211-N23 (Wittgenstein~Award).\r\nAny opinions, findings, and conclusions or recommendations expressed in this material are those of the authors and do not necessarily reflect the views of the NSF or the FWF.","publication_identifier":{"eissn":["2475-1421"]},"_id":"10153","citation":{"ama":"Mühlböck F, Tate R. Transitioning from structural to nominal code with efficient gradual typing. <i>Proceedings of the ACM on Programming Languages</i>. 2021;5. doi:<a href=\"https://doi.org/10.1145/3485504\">10.1145/3485504</a>","mla":"Mühlböck, Fabian, and Ross Tate. “Transitioning from Structural to Nominal Code with Efficient Gradual Typing.” <i>Proceedings of the ACM on Programming Languages</i>, vol. 5, 127, Association for Computing Machinery, 2021, doi:<a href=\"https://doi.org/10.1145/3485504\">10.1145/3485504</a>.","ista":"Mühlböck F, Tate R. 2021. Transitioning from structural to nominal code with efficient gradual typing. Proceedings of the ACM on Programming Languages. 5, 127.","short":"F. Mühlböck, R. Tate, Proceedings of the ACM on Programming Languages 5 (2021).","ieee":"F. Mühlböck and R. Tate, “Transitioning from structural to nominal code with efficient gradual typing,” <i>Proceedings of the ACM on Programming Languages</i>, vol. 5. Association for Computing Machinery, 2021.","apa":"Mühlböck, F., &#38; Tate, R. (2021). Transitioning from structural to nominal code with efficient gradual typing. <i>Proceedings of the ACM on Programming Languages</i>. Chicago, IL, United States: Association for Computing Machinery. <a href=\"https://doi.org/10.1145/3485504\">https://doi.org/10.1145/3485504</a>","chicago":"Mühlböck, Fabian, and Ross Tate. “Transitioning from Structural to Nominal Code with Efficient Gradual Typing.” <i>Proceedings of the ACM on Programming Languages</i>. Association for Computing Machinery, 2021. <a href=\"https://doi.org/10.1145/3485504\">https://doi.org/10.1145/3485504</a>."},"publication_status":"published","author":[{"orcid":"0000-0003-1548-0177","last_name":"Mühlböck","full_name":"Mühlböck, Fabian","first_name":"Fabian","id":"6395C5F6-89DF-11E9-9C97-6BDFE5697425"},{"first_name":"Ross","last_name":"Tate","full_name":"Tate, Ross"}],"keyword":["gradual typing","gradual guarantee","nominal","structural","call tags"],"abstract":[{"text":"Gradual typing is a principled means for mixing typed and untyped code. But typed and untyped code often exhibit different programming patterns. There is already substantial research investigating gradually giving types to code exhibiting typical untyped patterns, and some research investigating gradually removing types from code exhibiting typical typed patterns. This paper investigates how to extend these established gradual-typing concepts to give formal guarantees not only about how to change types as code evolves but also about how to change such programming patterns as well.\r\n\r\nIn particular, we explore mixing untyped \"structural\" code with typed \"nominal\" code in an object-oriented language. But whereas previous work only allowed \"nominal\" objects to be treated as \"structural\" objects, we also allow \"structural\" objects to dynamically acquire certain nominal types, namely interfaces. We present a calculus that supports such \"cross-paradigm\" code migration and interoperation in a manner satisfying both the static and dynamic gradual guarantees, and demonstrate that the calculus can be implemented efficiently.","lang":"eng"}],"article_number":"127","tmp":{"name":"Creative Commons Attribution-NoDerivatives 4.0 International (CC BY-ND 4.0)","short":"CC BY-ND (4.0)","legal_code_url":"https://creativecommons.org/licenses/by-nd/4.0/legalcode","image":"/image/cc_by_nd.png"},"ddc":["005"],"year":"2021","doi":"10.1145/3485504","title":"Transitioning from structural to nominal code with efficient gradual typing"},{"author":[{"id":"6395C5F6-89DF-11E9-9C97-6BDFE5697425","orcid":"0000-0003-1548-0177","last_name":"Mühlböck","full_name":"Mühlböck, Fabian","first_name":"Fabian"},{"id":"40876CD8-F248-11E8-B48F-1D18A9856A87","first_name":"Thomas A","orcid":"0000-0002-2985-7724","full_name":"Henzinger, Thomas A","last_name":"Henzinger"}],"keyword":["run-time verification","software engineering","implicit specification"],"abstract":[{"text":"We argue that the time is ripe to investigate differential monitoring, in which the specification of a program's behavior is implicitly given by a second program implementing the same informal specification. Similar ideas have been proposed before, and are currently implemented in restricted form for testing and specialized run-time analyses, aspects of which we combine. We discuss the challenges of implementing differential monitoring as a general-purpose, black-box run-time monitoring framework, and present promising results of a preliminary implementation, showing low monitoring overheads for diverse programs.","lang":"eng"}],"publication_status":"published","citation":{"ista":"Mühlböck F, Henzinger TA. 2021. Differential monitoring, IST Austria, 17p.","short":"F. Mühlböck, T.A. Henzinger, Differential Monitoring, IST Austria, 2021.","mla":"Mühlböck, Fabian, and Thomas A. Henzinger. <i>Differential Monitoring</i>. IST Austria, 2021, doi:<a href=\"https://doi.org/10.15479/AT:ISTA:9946\">10.15479/AT:ISTA:9946</a>.","ama":"Mühlböck F, Henzinger TA. <i>Differential Monitoring</i>. IST Austria; 2021. doi:<a href=\"https://doi.org/10.15479/AT:ISTA:9946\">10.15479/AT:ISTA:9946</a>","chicago":"Mühlböck, Fabian, and Thomas A Henzinger. <i>Differential Monitoring</i>. IST Austria, 2021. <a href=\"https://doi.org/10.15479/AT:ISTA:9946\">https://doi.org/10.15479/AT:ISTA:9946</a>.","apa":"Mühlböck, F., &#38; Henzinger, T. A. (2021). <i>Differential monitoring</i>. IST Austria. <a href=\"https://doi.org/10.15479/AT:ISTA:9946\">https://doi.org/10.15479/AT:ISTA:9946</a>","ieee":"F. Mühlböck and T. A. Henzinger, <i>Differential monitoring</i>. IST Austria, 2021."},"acknowledgement":"The authors would like to thank Borzoo Bonakdarpour, Derek Dreyer, Adrian Francalanza, Owolabi Legunsen, Matthew Milano, Manuel Rigger, Cesar Sanchez, and the members of the IST Verification Seminar for their helpful comments and insights on various stages of this work, as well as the reviewers of RV’21 for their helpful suggestions on the actual paper.","user_id":"8b945eb4-e2f2-11eb-945a-df72226e66a9","oa_version":"Published Version","project":[{"call_identifier":"FWF","name":"The Wittgenstein Prize","_id":"25F42A32-B435-11E9-9278-68D0E5697425","grant_number":"Z211"}],"_id":"9946","publication_identifier":{"issn":["2664-1690"]},"oa":1,"date_updated":"2023-08-14T07:20:29Z","article_processing_charge":"No","title":"Differential monitoring","doi":"10.15479/AT:ISTA:9946","year":"2021","ddc":["005"],"related_material":{"record":[{"relation":"other","id":"9281","status":"public"},{"id":"10108","relation":"shorter_version","status":"public"}]},"alternative_title":["IST Austria Technical Report"],"status":"public","type":"technical_report","day":"01","file_date_updated":"2021-09-03T12:34:28Z","page":"17","language":[{"iso":"eng"}],"publisher":"IST Austria","date_published":"2021-09-01T00:00:00Z","month":"09","date_created":"2021-08-20T20:00:37Z","file":[{"relation":"main_file","content_type":"application/pdf","creator":"fmuehlbo","file_id":"9948","access_level":"open_access","date_updated":"2021-09-03T12:34:28Z","file_size":"320453","file_name":"differentialmonitoring-techreport.pdf","checksum":"0f9aafd59444cb6bdca6925d163ab946","date_created":"2021-08-20T19:59:44Z"}],"department":[{"_id":"ToHe"}],"has_accepted_license":"1"}]