[{"date_updated":"2023-04-25T07:19:06Z","status":"public","oa_version":"Published Version","page":"38","publication_status":"published","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)"},"day":"27","ec_funded":1,"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\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."}],"project":[{"grant_number":"101020093","call_identifier":"H2020","_id":"62781420-2b32-11ec-9570-8d9b63373d4d","name":"Vigilant Algorithmic Monitoring of Software"}],"citation":{"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>","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.","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>.","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>"},"alternative_title":["IST Austria Technical Report"],"has_accepted_license":"1","related_material":{"record":[{"status":"public","id":"12856","relation":"later_version"}]},"title":"VAMOS: Middleware for Best-Effort Third-Party Monitoring","file":[{"file_size":662409,"file_name":"main.pdf","success":1,"date_updated":"2023-01-27T03:18:34Z","date_created":"2023-01-27T03:18:34Z","checksum":"55426e463fdeafe9777fc3ff635154c7","file_id":"12408","creator":"fmuehlbo","content_type":"application/pdf","relation":"main_file","access_level":"open_access"}],"language":[{"iso":"eng"}],"doi":"10.15479/AT:ISTA:12407","publisher":"Institute of Science and Technology Austria","year":"2023","type":"technical_report","author":[{"last_name":"Chalupa","id":"87e34708-d6c6-11ec-9f5b-9391e7be2463","full_name":"Chalupa, Marek","first_name":"Marek"},{"id":"6395C5F6-89DF-11E9-9C97-6BDFE5697425","last_name":"Mühlböck","orcid":"0000-0003-1548-0177","full_name":"Mühlböck, Fabian","first_name":"Fabian"},{"first_name":"Stefanie","full_name":"Muroya Lei, Stefanie","id":"a376de31-8972-11ed-ae7b-d0251c13c8ff","last_name":"Muroya Lei"},{"orcid":"0000-0002-2985-7724","last_name":"Henzinger","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","first_name":"Thomas A","full_name":"Henzinger, Thomas A"}],"oa":1,"_id":"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.","department":[{"_id":"ToHe"}],"ddc":["005"],"article_processing_charge":"No","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","file_date_updated":"2023-01-27T03:18:34Z","keyword":["runtime monitoring","best effort","third party"],"month":"01","publication_identifier":{"eissn":["2664-1690"]}},{"project":[{"name":"Vigilant Algorithmic Monitoring of Software","_id":"62781420-2b32-11ec-9570-8d9b63373d4d","call_identifier":"H2020","grant_number":"101020093"}],"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>.","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>","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.","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 <i>Fundamental Approaches to Software Engineering</i>, Paris, France, 2023, vol. 13991, pp. 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 <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>."},"alternative_title":["LNCS"],"has_accepted_license":"1","publication":"Fundamental Approaches to Software Engineering","related_material":{"record":[{"status":"public","id":"12407","relation":"earlier_version"}]},"file":[{"file_name":"2023_LNCS_ChalupaM.pdf","file_size":580828,"date_created":"2023-04-25T07:16:36Z","checksum":"17a7c8e08be609cf2408d37ea55e322c","file_id":"12865","date_updated":"2023-04-25T07:16:36Z","success":1,"creator":"dernst","access_level":"open_access","relation":"main_file","content_type":"application/pdf"}],"title":"Vamos: Middleware for best-effort third-party monitoring","date_updated":"2023-04-25T07:19:07Z","status":"public","page":"260-281","oa_version":"Published Version","publication_status":"published","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)"},"day":"20","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\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"}],"date_created":"2023-04-20T08:29:42Z","department":[{"_id":"ToHe"}],"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.","article_processing_charge":"No","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","ddc":["000"],"conference":{"name":"FASE: Fundamental Approaches to Software Engineering","start_date":"2023-04-22","end_date":"2023-04-27","location":"Paris, France"},"file_date_updated":"2023-04-25T07:16:36Z","intvolume":"     13991","month":"04","quality_controlled":"1","publication_identifier":{"eissn":["1611-3349"],"issn":["0302-9743"],"eisbn":["9783031308260"],"isbn":["9783031308253"]},"volume":13991,"language":[{"iso":"eng"}],"doi":"10.1007/978-3-031-30826-0_15","publisher":"Springer Nature","year":"2023","type":"conference","author":[{"last_name":"Chalupa","id":"87e34708-d6c6-11ec-9f5b-9391e7be2463","first_name":"Marek","full_name":"Chalupa, Marek"},{"orcid":"0000-0003-1548-0177","id":"6395C5F6-89DF-11E9-9C97-6BDFE5697425","last_name":"Mühlböck","full_name":"Mühlböck, Fabian","first_name":"Fabian"},{"last_name":"Muroya Lei","id":"a376de31-8972-11ed-ae7b-d0251c13c8ff","full_name":"Muroya Lei, Stefanie","first_name":"Stefanie"},{"id":"40876CD8-F248-11E8-B48F-1D18A9856A87","last_name":"Henzinger","orcid":"0000-0002-2985-7724","full_name":"Henzinger, Thomas A","first_name":"Thomas A"}],"oa":1,"_id":"12856","date_published":"2023-04-20T00:00:00Z"},{"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","article_processing_charge":"No","project":[{"call_identifier":"H2020","grant_number":"754411","name":"ISTplus - Postdoctoral Fellowships","_id":"260C2330-B435-11E9-9278-68D0E5697425"}],"department":[{"_id":"LaEr"},{"_id":"ToHe"}],"arxiv":1,"citation":{"ista":"Dubach G, Mühlböck F. Formal verification of Zagier’s one-sentence proof. arXiv, 2103.11389.","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>.","short":"G. Dubach, F. Mühlböck, ArXiv (n.d.).","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>","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>","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>.","ieee":"G. Dubach and F. Mühlböck, “Formal verification of Zagier’s one-sentence proof,” <i>arXiv</i>. ."},"article_number":"2103.11389","date_created":"2021-03-23T05:38:48Z","external_id":{"arxiv":["2103.11389"]},"related_material":{"record":[{"relation":"other","status":"public","id":"9946"}]},"title":"Formal verification of Zagier's one-sentence proof","publication":"arXiv","main_file_link":[{"url":"https://arxiv.org/abs/2103.11389","open_access":"1"}],"month":"03","type":"preprint","status":"public","date_updated":"2023-05-03T10:26:45Z","year":"2021","language":[{"iso":"eng"}],"doi":"10.48550/arXiv.2103.11389","ec_funded":1,"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."}],"publication_status":"submitted","date_published":"2021-03-21T00:00:00Z","oa_version":"Preprint","day":"21","oa":1,"_id":"9281","author":[{"orcid":"0000-0001-6892-8137","id":"D5C6A458-10C4-11EA-ABF4-A4B43DDC885E","last_name":"Dubach","first_name":"Guillaume","full_name":"Dubach, Guillaume"},{"id":"6395C5F6-89DF-11E9-9C97-6BDFE5697425","last_name":"Mühlböck","orcid":"0000-0003-1548-0177","first_name":"Fabian","full_name":"Mühlböck, Fabian"}]},{"month":"10","quality_controlled":"1","publication_identifier":{"issn":["0302-9743"],"isbn":["978-3-030-88493-2"],"eisbn":["978-3-030-88494-9"],"eissn":["1611-3349"]},"isi":1,"volume":12974,"date_created":"2021-10-07T23:30:10Z","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.","department":[{"_id":"ToHe"}],"ddc":["005"],"article_processing_charge":"No","user_id":"4359f0d1-fa6c-11eb-b949-802e58b17ae8","file_date_updated":"2021-10-07T23:32:18Z","conference":{"name":"RV: Runtime Verification","end_date":"2021-10-14","start_date":"2021-10-11","location":"Virtual"},"place":"Cham","keyword":["run-time verification","software engineering","implicit specification"],"intvolume":"     12974","author":[{"full_name":"Mühlböck, Fabian","first_name":"Fabian","id":"6395C5F6-89DF-11E9-9C97-6BDFE5697425","last_name":"Mühlböck","orcid":"0000-0003-1548-0177"},{"first_name":"Thomas A","full_name":"Henzinger, Thomas A","orcid":"0000-0002-2985-7724","last_name":"Henzinger","id":"40876CD8-F248-11E8-B48F-1D18A9856A87"}],"oa":1,"_id":"10108","date_published":"2021-10-06T00:00:00Z","language":[{"iso":"eng"}],"doi":"10.1007/978-3-030-88494-9_12","publisher":"Springer Nature","year":"2021","type":"conference","publication":"International Conference on Runtime Verification","external_id":{"isi":["000719383800012"]},"related_material":{"record":[{"id":"9946","status":"public","relation":"extended_version"}]},"title":"Differential monitoring","file":[{"creator":"fmuehlbo","relation":"main_file","content_type":"application/pdf","access_level":"open_access","file_size":350632,"file_name":"differentialmonitoring-cameraready-openaccess.pdf","date_updated":"2021-10-07T23:32:18Z","success":1,"file_id":"10109","checksum":"554c7fdb259eda703a8b6328a6dad55a","date_created":"2021-10-07T23:32:18Z"}],"project":[{"call_identifier":"FWF","grant_number":"Z211","name":"The Wittgenstein Prize","_id":"25F42A32-B435-11E9-9278-68D0E5697425"}],"citation":{"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.","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>.","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>","ista":"Mühlböck F, Henzinger TA. 2021. Differential monitoring. International Conference on Runtime Verification. RV: Runtime Verification, LNCS, vol. 12974, 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>.","short":"F. Mühlböck, T.A. Henzinger, in:, International Conference on Runtime Verification, Springer Nature, Cham, 2021, pp. 231–243.","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>"},"scopus_import":"1","alternative_title":["LNCS"],"has_accepted_license":"1","publication_status":"published","page":"231-243","oa_version":"Preprint","day":"06","abstract":[{"lang":"eng","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."}],"date_updated":"2023-08-14T07:20:30Z","status":"public"},{"publication":"Proceedings of the ACM on Programming Languages","file":[{"creator":"fmuehlbo","relation":"main_file","content_type":"application/pdf","access_level":"open_access","file_size":770269,"file_name":"monnom-oopsla21.pdf","date_updated":"2021-10-19T12:52:23Z","success":1,"file_id":"10154","checksum":"71011efd2da771cafdec7f0d9693f8c1","date_created":"2021-10-19T12:52:23Z"}],"title":"Transitioning from structural to nominal code with efficient gradual typing","has_accepted_license":"1","project":[{"grant_number":"Z211","call_identifier":"FWF","_id":"25F42A32-B435-11E9-9278-68D0E5697425","name":"The Wittgenstein Prize"}],"citation":{"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>.","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.","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>.","short":"F. Mühlböck, R. Tate, Proceedings of the ACM on Programming Languages 5 (2021).","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.","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>","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>"},"oa_version":"Published Version","publication_status":"published","tmp":{"short":"CC BY-ND (4.0)","image":"/image/cc_by_nd.png","name":"Creative Commons Attribution-NoDerivatives 4.0 International (CC BY-ND 4.0)","legal_code_url":"https://creativecommons.org/licenses/by-nd/4.0/legalcode"},"day":"15","abstract":[{"lang":"eng","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."}],"status":"public","date_updated":"2021-11-12T11:30:07Z","volume":5,"article_type":"original","month":"10","quality_controlled":"1","publication_identifier":{"eissn":["2475-1421"]},"user_id":"8b945eb4-e2f2-11eb-945a-df72226e66a9","article_processing_charge":"No","ddc":["005"],"conference":{"end_date":"2021-10-23","start_date":"2021-10-17","name":"OOPSLA: Object-Oriented Programming, Systems, Languages, and Applications","location":"Chicago, IL, United States"},"file_date_updated":"2021-10-19T12:52:23Z","keyword":["gradual typing","gradual guarantee","nominal","structural","call tags"],"intvolume":"         5","date_created":"2021-10-19T12:48:44Z","article_number":"127","department":[{"_id":"ToHe"}],"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.","date_published":"2021-10-15T00:00:00Z","author":[{"first_name":"Fabian","full_name":"Mühlböck, Fabian","last_name":"Mühlböck","id":"6395C5F6-89DF-11E9-9C97-6BDFE5697425","orcid":"0000-0003-1548-0177"},{"full_name":"Tate, Ross","first_name":"Ross","last_name":"Tate"}],"oa":1,"_id":"10153","type":"journal_article","language":[{"iso":"eng"}],"doi":"10.1145/3485504","publisher":"Association for Computing Machinery","year":"2021"},{"status":"public","date_updated":"2023-08-14T07:20:29Z","day":"01","page":"17","oa_version":"Published Version","publication_status":"published","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"}],"has_accepted_license":"1","alternative_title":["IST Austria Technical Report"],"citation":{"ieee":"F. Mühlböck and T. A. Henzinger, <i>Differential monitoring</i>. IST Austria, 2021.","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>.","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>","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>","ista":"Mühlböck F, Henzinger TA. 2021. Differential monitoring, IST Austria, 17p.","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>.","short":"F. Mühlböck, T.A. Henzinger, Differential Monitoring, IST Austria, 2021."},"project":[{"_id":"25F42A32-B435-11E9-9278-68D0E5697425","name":"The Wittgenstein Prize","call_identifier":"FWF","grant_number":"Z211"}],"title":"Differential monitoring","file":[{"creator":"fmuehlbo","access_level":"open_access","relation":"main_file","content_type":"application/pdf","file_name":"differentialmonitoring-techreport.pdf","file_size":"320453","date_created":"2021-08-20T19:59:44Z","checksum":"0f9aafd59444cb6bdca6925d163ab946","file_id":"9948","date_updated":"2021-09-03T12:34:28Z"}],"related_material":{"record":[{"id":"9281","status":"public","relation":"other"},{"status":"public","id":"10108","relation":"shorter_version"}]},"type":"technical_report","doi":"10.15479/AT:ISTA:9946","language":[{"iso":"eng"}],"year":"2021","publisher":"IST Austria","date_published":"2021-09-01T00:00:00Z","author":[{"id":"6395C5F6-89DF-11E9-9C97-6BDFE5697425","last_name":"Mühlböck","orcid":"0000-0003-1548-0177","full_name":"Mühlböck, Fabian","first_name":"Fabian"},{"first_name":"Thomas A","full_name":"Henzinger, Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","last_name":"Henzinger","orcid":"0000-0002-2985-7724"}],"_id":"9946","oa":1,"file_date_updated":"2021-09-03T12:34:28Z","ddc":["005"],"user_id":"8b945eb4-e2f2-11eb-945a-df72226e66a9","article_processing_charge":"No","keyword":["run-time verification","software engineering","implicit specification"],"date_created":"2021-08-20T20:00:37Z","department":[{"_id":"ToHe"}],"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.","month":"09","publication_identifier":{"issn":["2664-1690"]}}]