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