---
OA_place: publisher
OA_type: hybrid
_id: '22006'
abstract:
- lang: eng
text: Runtime monitoring checks, during execution, whether a partial signal produced
by a hybrid system satisfies its specification. Signal First-Order Logic (SFO)
offers expressive real-time specifications over such signals, but currently comes
only with Boolean semantics and has no tool support. We provide the first robustness-based
quantitative semantics for SFO, enabling the expression and evaluation of rich
real-time properties beyond the scope of existing formalisms such as Signal Temporal
Logic. To enable online monitoring, we identify a past-time fragment of SFO and
give a pastification procedure that transforms bounded-response SFO formulas into
equisatisfiable formulas in this fragment. We then develop an efficient runtime
monitoring algorithm for this past-time fragment and evaluate its performance
on a set of benchmarks, demonstrating the practicality and effectiveness of our
approach. To the best of our knowledge, this is the first publicly available prototype
for online quantitative monitoring of full SFO.
acknowledgement: We thank the anonymous reviewers for their helpful comments. This
work was supported by the European Research Council (ERC) Grants VAMOS (No. 101020093)
and HYPER (No. 101055412), and by the Advanced Research and Invention Agency under
the Safeguarded AI programme (MSAI-PR01-P047).
alternative_title:
- LNCS
article_processing_charge: No
arxiv: 1
author:
- first_name: Marek
full_name: Chalupa, Marek
id: 87e34708-d6c6-11ec-9f5b-9391e7be2463
last_name: Chalupa
- first_name: Thomas A
full_name: Henzinger, Thomas A
id: 40876CD8-F248-11E8-B48F-1D18A9856A87
last_name: Henzinger
orcid: 0000-0002-2985-7724
- first_name: Naci E
full_name: Sarac, Naci E
id: 8C6B42F8-C8E6-11E9-A03A-F2DCE5697425
last_name: Sarac
- first_name: Zhengqi
full_name: Yu, Zhengqi
id: 20aa2ae8-f2f1-11ed-bbfa-8205053f1342
last_name: Yu
orcid: 0000-0002-4993-773X
citation:
ama: 'Chalupa M, Henzinger TA, Sarac NE, Yu E. Quantitative monitoring of Signal
First-Order logic. In: 27th International Symposium on Formal Methods.
Vol 16557. Springer Nature; 2026:214-233. doi:10.1007/978-3-032-26220-2_11'
apa: 'Chalupa, M., Henzinger, T. A., Sarac, N. E., & Yu, E. (2026). Quantitative
monitoring of Signal First-Order logic. In 27th International Symposium on
Formal Methods (Vol. 16557, pp. 214–233). Tokyo, Japan: Springer Nature. https://doi.org/10.1007/978-3-032-26220-2_11'
chicago: Chalupa, Marek, Thomas A Henzinger, Naci E Sarac, and Emily Yu. “Quantitative
Monitoring of Signal First-Order Logic.” In 27th International Symposium on
Formal Methods, 16557:214–33. Springer Nature, 2026. https://doi.org/10.1007/978-3-032-26220-2_11.
ieee: M. Chalupa, T. A. Henzinger, N. E. Sarac, and E. Yu, “Quantitative monitoring
of Signal First-Order logic,” in 27th International Symposium on Formal Methods,
Tokyo, Japan, 2026, vol. 16557, pp. 214–233.
ista: 'Chalupa M, Henzinger TA, Sarac NE, Yu E. 2026. Quantitative monitoring of Signal
First-Order logic. 27th International Symposium on Formal Methods. FM: Formal
Methods, LNCS, vol. 16557, 214–233.'
mla: Chalupa, Marek, et al. “Quantitative Monitoring of Signal First-Order Logic.”
27th International Symposium on Formal Methods, vol. 16557, Springer Nature,
2026, pp. 214–33, doi:10.1007/978-3-032-26220-2_11.
short: M. Chalupa, T.A. Henzinger, N.E. Sarac, E. Yu, in:, 27th International Symposium
on Formal Methods, Springer Nature, 2026, pp. 214–233.
conference:
end_date: 2026-05-22
location: Tokyo, Japan
name: 'FM: Formal Methods'
start_date: 2026-05-18
das_tickbox: '0'
date_created: 2026-06-14T22:01:44Z
date_published: 2026-05-18T00:00:00Z
date_updated: 2026-06-22T08:21:09Z
day: '18'
ddc:
- '000'
department:
- _id: ToHe
doi: 10.1007/978-3-032-26220-2_11
ec_funded: 1
external_id:
arxiv:
- '2603.00728'
file:
- access_level: open_access
checksum: 7055199ecb985e9e2e272f4988827067
content_type: application/pdf
creator: dernst
date_created: 2026-06-22T08:18:41Z
date_updated: 2026-06-22T08:18:41Z
file_id: '22113'
file_name: 2026_LNCS_Chalupa.pdf
file_size: 849237
relation: main_file
success: 1
file_date_updated: 2026-06-22T08:18:41Z
fulldoi: https://doi.org/10.1007/978-3-032-26220-2_11
has_accepted_license: '1'
intvolume: ' 16557'
keyword:
- Signal first-order logic
- Robustness-based quantitative semantics
- Online runtime monitoring
language:
- iso: eng
license: https://creativecommons.org/licenses/by/4.0/
month: '05'
oa: 1
oa_version: Published Version
page: 214-233
project:
- _id: 62781420-2b32-11ec-9570-8d9b63373d4d
call_identifier: H2020
grant_number: '101020093'
name: Vigilant Algorithmic Monitoring of Software
publication: 27th International Symposium on Formal Methods
publication_identifier:
eissn:
- 1611-3349
isbn:
- '9783032262196'
issn:
- 0302-9743
publication_status: published
publisher: Springer Nature
quality_controlled: '1'
scopus_import: '1'
status: public
title: Quantitative monitoring of Signal First-Order logic
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: 16557
year: '2026'
...
---
OA_place: publisher
OA_type: hybrid
_id: '20866'
abstract:
- lang: eng
text: In this work, we present hypernode automata as a specification formalism for
hyperproperties of systems whose executions may be misaligned among themselves,
such as concurrent systems. These automata consist of nodes labeled with hypernode
logic formulas and transitions marked with synchronizing actions. Hypernode logic
formulas establish relations between sequences of variable values among different
system executions. This logic enables both synchronous and asynchronous analysis
of traces. In its asynchronous view on execution traces, hypernode formulas establish
relations on the order of value changes for each variable without correlating
their timing. In both views, the analysis of different execution traces is synchronized
through the transitions of hypernode automata. By combining logic’s declarative
nature with automata’s procedural power, hypernode automata seamlessly integrate
asynchronicity requirements at the node level with synchronicity between node
transitions. We show that the model-checking problem for hypernode automata is
decidable for specifications where each node specifies either a synchronous or
an asynchronous requirement for the system’s executions, but not both.
acknowledgement: This work was supported in part by the Austrian Science Fund (FWF)
SFB project SpyCoDe 10.55776/F85, by the FWF projects ZK-35 and W1255-N23, and by
the ERC Advanced Grant VAMOS 101020093. Open access funding provided by Institute
of Science and Technology (IST Austria).
article_number: '43'
article_processing_charge: Yes (via OA deal)
article_type: original
arxiv: 1
author:
- first_name: Ezio
full_name: Bartocci, Ezio
last_name: Bartocci
- first_name: Marek
full_name: Chalupa, Marek
id: 87e34708-d6c6-11ec-9f5b-9391e7be2463
last_name: Chalupa
- first_name: Thomas A
full_name: Henzinger, Thomas A
id: 40876CD8-F248-11E8-B48F-1D18A9856A87
last_name: Henzinger
orcid: 0000-0002-2985-7724
- first_name: Dejan
full_name: Nickovic, Dejan
id: 41BCEE5C-F248-11E8-B48F-1D18A9856A87
last_name: Nickovic
- first_name: Ana
full_name: Oliveira da Costa, Ana
id: f347ec37-6676-11ee-b395-a888cb7b4fb4
last_name: Oliveira da Costa
orcid: 0000-0002-8741-5799
citation:
ama: Bartocci E, Chalupa M, Henzinger TA, Nickovic D, Oliveira da Costa A. Hypernode
automata. Acta Informatica. 2025;62(4). doi:10.1007/s00236-025-00509-8
apa: Bartocci, E., Chalupa, M., Henzinger, T. A., Nickovic, D., & Oliveira da
Costa, A. (2025). Hypernode automata. Acta Informatica. Springer Nature.
https://doi.org/10.1007/s00236-025-00509-8
chicago: Bartocci, Ezio, Marek Chalupa, Thomas A Henzinger, Dejan Nickovic, and
Ana Oliveira da Costa. “Hypernode Automata.” Acta Informatica. Springer
Nature, 2025. https://doi.org/10.1007/s00236-025-00509-8.
ieee: E. Bartocci, M. Chalupa, T. A. Henzinger, D. Nickovic, and A. Oliveira da
Costa, “Hypernode automata,” Acta Informatica, vol. 62, no. 4. Springer
Nature, 2025.
ista: Bartocci E, Chalupa M, Henzinger TA, Nickovic D, Oliveira da Costa A. 2025.
Hypernode automata. Acta Informatica. 62(4), 43.
mla: Bartocci, Ezio, et al. “Hypernode Automata.” Acta Informatica, vol.
62, no. 4, 43, Springer Nature, 2025, doi:10.1007/s00236-025-00509-8.
short: E. Bartocci, M. Chalupa, T.A. Henzinger, D. Nickovic, A. Oliveira da Costa,
Acta Informatica 62 (2025).
corr_author: '1'
date_created: 2025-12-29T12:07:12Z
date_published: 2025-12-09T00:00:00Z
date_updated: 2026-01-05T12:27:41Z
day: '09'
ddc:
- '000'
department:
- _id: ToHe
doi: 10.1007/s00236-025-00509-8
ec_funded: 1
external_id:
arxiv:
- '2305.02836'
file:
- access_level: open_access
checksum: 06ed45a1218ad8464818803ae2968aaf
content_type: application/pdf
creator: dernst
date_created: 2026-01-05T12:26:43Z
date_updated: 2026-01-05T12:26:43Z
file_id: '20944'
file_name: 2025_ActaInformatica_Bartocci.pdf
file_size: 7117003
relation: main_file
success: 1
file_date_updated: 2026-01-05T12:26:43Z
fulldoi: https://doi.org/10.1007/s00236-025-00509-8
has_accepted_license: '1'
intvolume: ' 62'
issue: '4'
language:
- iso: eng
month: '12'
oa: 1
oa_version: Published Version
project:
- _id: 62781420-2b32-11ec-9570-8d9b63373d4d
call_identifier: H2020
grant_number: '101020093'
name: Vigilant Algorithmic Monitoring of Software
- _id: 34a1b658-11ca-11ed-8bc3-c75229f0241e
grant_number: F8502
name: Interface Theory for Security and Privacy
publication: Acta Informatica
publication_identifier:
eissn:
- 1432-0525
issn:
- 0001-5903
publication_status: published
publisher: Springer Nature
quality_controlled: '1'
related_material:
record:
- id: '14405'
relation: earlier_version
status: public
scopus_import: '1'
status: public
title: Hypernode automata
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: journal_article
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 62
year: '2025'
...
---
OA_place: publisher
OA_type: gold
_id: '21089'
abstract:
- lang: eng
text: 'Hypertrace logic is a sorted first-order logic with separate sorts for time
and execution traces. Its formulas specify hyperproperties, which are properties
relating multiple traces. In this work, we extend hypertrace logic by introducing
trace quantifiers that range over the set of all possible traces. In this extended
logic, formulas can quantify over two kinds of trace variables: constrained trace
variables, which range over a fixed set of traces defined by the model, and unconstrained
trace variables, which can be assigned to any trace. In comparison, hyperlogics
such as HyperLTL have only constrained trace quantifiers. We use hypertrace logic
to study how different quantifier patterns affect the decidability of the satisfiability
problem. We prove that hypertrace logic without constrained trace quantifiers
is equivalent to monadic second-order logic of one successor (S1S), and therefore
satisfiable, and that the trace-prefixed fragment (all trace quantifiers precede
all time quantifiers) is equivalent to HyperQPTL. Moreover, we show that all hypertrace
formulas where the only alternation between constrained trace quantifiers is from
an existential to a universal quantifier are equisatisfiable to formulas without
constraints on their trace variables and, therefore, decidable as well. Our framework
allows us to study also time-prefixed hyperlogics, for which we provide new decidability
and undecidability results.'
acknowledgement: This work was supported in part by the Austrian Science Fund (FWF)
SFB project SpyCoDe 10.55776/F85 and by the ERC Advanced Grant VAMOS 101020093.
alternative_title:
- LIPIcs
article_processing_charge: No
arxiv: 1
author:
- first_name: Marek
full_name: Chalupa, Marek
id: 87e34708-d6c6-11ec-9f5b-9391e7be2463
last_name: Chalupa
- first_name: Thomas A
full_name: Henzinger, Thomas A
id: 40876CD8-F248-11E8-B48F-1D18A9856A87
last_name: Henzinger
orcid: 0000-0002-2985-7724
- first_name: Ana A
full_name: Oliveira da Costa, Ana A
id: 8b282559-50b0-11ef-861e-d6ace0d92e9b
last_name: Oliveira da Costa
citation:
ama: 'Chalupa M, Henzinger TA, Oliveira da Costa AA. Flavors of quantifiers in hyperlogics.
In: 45th Annual Conference on Foundations of Software Technology and Theoretical
Computer Science. Vol 360. Schloss Dagstuhl - Leibniz-Zentrum für Informatik;
2025:20:1-20:18. doi:10.4230/LIPICS.FSTTCS.2025.20'
apa: 'Chalupa, M., Henzinger, T. A., & Oliveira da Costa, A. A. (2025). Flavors
of quantifiers in hyperlogics. In 45th Annual Conference on Foundations of
Software Technology and Theoretical Computer Science (Vol. 360, p. 20:1-20:18).
Pilani, India: Schloss Dagstuhl - Leibniz-Zentrum für Informatik. https://doi.org/10.4230/LIPICS.FSTTCS.2025.20'
chicago: Chalupa, Marek, Thomas A Henzinger, and Ana A Oliveira da Costa. “Flavors
of Quantifiers in Hyperlogics.” In 45th Annual Conference on Foundations of
Software Technology and Theoretical Computer Science, 360:20:1-20:18. Schloss
Dagstuhl - Leibniz-Zentrum für Informatik, 2025. https://doi.org/10.4230/LIPICS.FSTTCS.2025.20.
ieee: M. Chalupa, T. A. Henzinger, and A. A. Oliveira da Costa, “Flavors of quantifiers
in hyperlogics,” in 45th Annual Conference on Foundations of Software Technology
and Theoretical Computer Science, Pilani, India, 2025, vol. 360, p. 20:1-20:18.
ista: 'Chalupa M, Henzinger TA, Oliveira da Costa AA. 2025. Flavors of quantifiers
in hyperlogics. 45th Annual Conference on Foundations of Software Technology and
Theoretical Computer Science. FSTTCS: Conference on Foundations of Software Technology
and Theoretical Computer Science, LIPIcs, vol. 360, 20:1-20:18.'
mla: Chalupa, Marek, et al. “Flavors of Quantifiers in Hyperlogics.” 45th Annual
Conference on Foundations of Software Technology and Theoretical Computer Science,
vol. 360, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2025, p. 20:1-20:18,
doi:10.4230/LIPICS.FSTTCS.2025.20.
short: M. Chalupa, T.A. Henzinger, A.A. Oliveira da Costa, in:, 45th Annual Conference
on Foundations of Software Technology and Theoretical Computer Science, Schloss
Dagstuhl - Leibniz-Zentrum für Informatik, 2025, p. 20:1-20:18.
conference:
end_date: 2025-12-19
location: Pilani, India
name: 'FSTTCS: Conference on Foundations of Software Technology and Theoretical
Computer Science'
start_date: 2025-12-17
corr_author: '1'
date_created: 2026-01-29T15:39:15Z
date_published: 2025-12-09T00:00:00Z
date_updated: 2026-02-11T09:35:04Z
day: '09'
ddc:
- '000'
department:
- _id: ToHe
doi: 10.4230/LIPICS.FSTTCS.2025.20
ec_funded: 1
external_id:
arxiv:
- '2510.12298'
file:
- access_level: open_access
checksum: 8188ee5c7b14193d48eeb655e9bbdc47
content_type: application/pdf
creator: dernst
date_created: 2026-02-11T09:33:20Z
date_updated: 2026-02-11T09:33:20Z
file_id: '21213'
file_name: 2025_LIPIcS_Chalupa.pdf
file_size: 933970
relation: main_file
success: 1
file_date_updated: 2026-02-11T09:33:20Z
fulldoi: https://doi.org/10.4230/LIPICS.FSTTCS.2025.20
has_accepted_license: '1'
intvolume: ' 360'
language:
- iso: eng
month: '12'
oa: 1
oa_version: Published Version
page: 20:1-20:18
project:
- _id: 34a1b658-11ca-11ed-8bc3-c75229f0241e
grant_number: F8502
name: Interface Theory for Security and Privacy
- _id: 62781420-2b32-11ec-9570-8d9b63373d4d
call_identifier: H2020
grant_number: '101020093'
name: Vigilant Algorithmic Monitoring of Software
publication: 45th Annual Conference on Foundations of Software Technology and Theoretical
Computer Science
publication_status: published
publisher: Schloss Dagstuhl - Leibniz-Zentrum für Informatik
quality_controlled: '1'
scopus_import: '1'
status: public
title: Flavors of quantifiers in hyperlogics
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: 360
year: '2025'
...
---
OA_place: repository
OA_type: green
_id: '21093'
abstract:
- lang: eng
text: We propose a monitoring approach for hyperproperties where the system’s observations
range over infinite domains. The specifications are given as formulas of symbolic
hypernode logic, an extension of earlier versions of hypernode logic that supports
events with data. We demonstrate how to translate terms of symbolic hypernode
logic into multi-tape symbolic transducers and we present a monitoring algorithm
for universally quantified formulas that is based on this translation. We evaluate
our approach against the previous approach for monitoring hypernode logic, and
we also compare it to other monitors for hyperproperties.
acknowledgement: This work was supported in part by the ERC-2020-AdG 101020093 and
in part by the FWF-2022-SFB F8502 (SPyCoDe).
alternative_title:
- LNCS
article_processing_charge: No
arxiv: 1
author:
- first_name: Marek
full_name: Chalupa, Marek
id: 87e34708-d6c6-11ec-9f5b-9391e7be2463
last_name: Chalupa
- first_name: Thomas A
full_name: Henzinger, Thomas A
id: 40876CD8-F248-11E8-B48F-1D18A9856A87
last_name: Henzinger
orcid: 0000-0002-2985-7724
- first_name: Ana A
full_name: Oliveira da Costa, Ana A
id: 8b282559-50b0-11ef-861e-d6ace0d92e9b
last_name: Oliveira da Costa
citation:
ama: 'Chalupa M, Henzinger TA, Oliveira da Costa AA. Monitoring hypernode logic
over infinite domains. In: 25th International Conference on Runtime Verification.
Vol 16087. Springer Nature; 2025:417-437. doi:10.1007/978-3-032-05435-7_23'
apa: 'Chalupa, M., Henzinger, T. A., & Oliveira da Costa, A. A. (2025). Monitoring
hypernode logic over infinite domains. In 25th International Conference on
Runtime Verification (Vol. 16087, pp. 417–437). Graz, Austria: Springer Nature.
https://doi.org/10.1007/978-3-032-05435-7_23'
chicago: Chalupa, Marek, Thomas A Henzinger, and Ana A Oliveira da Costa. “Monitoring
Hypernode Logic over Infinite Domains.” In 25th International Conference on
Runtime Verification, 16087:417–37. Springer Nature, 2025. https://doi.org/10.1007/978-3-032-05435-7_23.
ieee: M. Chalupa, T. A. Henzinger, and A. A. Oliveira da Costa, “Monitoring hypernode
logic over infinite domains,” in 25th International Conference on Runtime Verification,
Graz, Austria, 2025, vol. 16087, pp. 417–437.
ista: 'Chalupa M, Henzinger TA, Oliveira da Costa AA. 2025. Monitoring hypernode
logic over infinite domains. 25th International Conference on Runtime Verification.
RV: Runtime Verification, LNCS, vol. 16087, 417–437.'
mla: Chalupa, Marek, et al. “Monitoring Hypernode Logic over Infinite Domains.”
25th International Conference on Runtime Verification, vol. 16087, Springer
Nature, 2025, pp. 417–37, doi:10.1007/978-3-032-05435-7_23.
short: M. Chalupa, T.A. Henzinger, A.A. Oliveira da Costa, in:, 25th International
Conference on Runtime Verification, Springer Nature, 2025, pp. 417–437.
conference:
end_date: 2025-09-19
location: Graz, Austria
name: 'RV: Runtime Verification'
start_date: 2025-09-15
corr_author: '1'
date_created: 2026-01-29T16:04:31Z
date_published: 2025-09-13T00:00:00Z
date_updated: 2026-02-16T11:59:20Z
day: '13'
department:
- _id: ToHe
doi: 10.1007/978-3-032-05435-7_23
ec_funded: 1
external_id:
arxiv:
- '2508.02301'
fulldoi: https://doi.org/10.1007/978-3-032-05435-7_23
intvolume: ' 16087'
language:
- iso: eng
main_file_link:
- open_access: '1'
url: https://doi.org/10.48550/arXiv.2508.02301
month: '09'
oa: 1
oa_version: Preprint
page: 417-437
project:
- _id: 62781420-2b32-11ec-9570-8d9b63373d4d
call_identifier: H2020
grant_number: '101020093'
name: Vigilant Algorithmic Monitoring of Software
- _id: 34a1b658-11ca-11ed-8bc3-c75229f0241e
grant_number: F8502
name: Interface Theory for Security and Privacy
publication: 25th International Conference on Runtime Verification
publication_identifier:
eisbn:
- '9783032054357'
eissn:
- 1611-3349
issn:
- 0302-9743
publication_status: published
publisher: Springer Nature
quality_controlled: '1'
status: public
title: Monitoring hypernode logic over infinite domains
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 16087
year: '2025'
...
---
OA_place: publisher
OA_type: hybrid
_id: '19739'
abstract:
- lang: eng
text: "Cooperative verification is gaining momentum in recent years. The usual setup
in cooperative verification is that a verifier A is run with some pre-defined
resources, and if it is not able to verify the program, the verification task
is passed to a verifier B together with information learned about the program
by verifier A, then the chain can continue to a verifier C, and so on. This scheme
is static: tools run one after another in a fixed pre-defined order and fixed
parameters and resource limits (the scheme may differ for properties to be analyzed,
though).\r\n\r\nBubaak is a program analysis tool that allows to run multiple
program verifiers in a dynamically changing combination of parallel and sequential
portfolios. Bubaak starts the verification process by invoking an initial set
of tasks; every task, when it is done (e.g., because of hitting a time limit or
finishing its job), rewrites itself into one or more successor tasks. New tasks
can be also spawned upon events generated by other tasks. This all happens dynamically
based on the information gathered by finished and running tasks. During their
execution, tasks that run in parallel can exchange (partial) verification artifacts,
either directly or with Bubaak as an intermediary."
acknowledgement: This work was in part supported by the ERC-2020-AdG 10102009 grant,
and in part by the German Research Foundation (DFG) - WE2290/13-2 (Coop2).
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: Cedric
full_name: Richter, Cedric
last_name: Richter
citation:
ama: 'Chalupa M, Richter C. BUBAAK: Dynamic cooperative verification. In: 31st
International Conference on Tools and Algorithms for the Construction and Analysis
of Systems. Vol 15698. Springer Nature; 2025:212-216. doi:10.1007/978-3-031-90660-2_14'
apa: 'Chalupa, M., & Richter, C. (2025). BUBAAK: Dynamic cooperative verification.
In 31st International Conference on Tools and Algorithms for the Construction
and Analysis of Systems (Vol. 15698, pp. 212–216). Hamilton, ON, Canada: Springer
Nature. https://doi.org/10.1007/978-3-031-90660-2_14'
chicago: 'Chalupa, Marek, and Cedric Richter. “BUBAAK: Dynamic Cooperative Verification.”
In 31st International Conference on Tools and Algorithms for the Construction
and Analysis of Systems, 15698:212–16. Springer Nature, 2025. https://doi.org/10.1007/978-3-031-90660-2_14.'
ieee: 'M. Chalupa and C. Richter, “BUBAAK: Dynamic cooperative verification,” in
31st International Conference on Tools and Algorithms for the Construction
and Analysis of Systems, Hamilton, ON, Canada, 2025, vol. 15698, pp. 212–216.'
ista: 'Chalupa M, Richter C. 2025. BUBAAK: Dynamic cooperative verification. 31st
International Conference on Tools and Algorithms for the Construction and Analysis
of Systems. TACAS: Tools and Algorithms for the Construction and Analysis of Systems,
LNCS, vol. 15698, 212–216.'
mla: 'Chalupa, Marek, and Cedric Richter. “BUBAAK: Dynamic Cooperative Verification.”
31st International Conference on Tools and Algorithms for the Construction
and Analysis of Systems, vol. 15698, Springer Nature, 2025, pp. 212–16, doi:10.1007/978-3-031-90660-2_14.'
short: M. Chalupa, C. Richter, in:, 31st International Conference on Tools and Algorithms
for the Construction and Analysis of Systems, Springer Nature, 2025, pp. 212–216.
conference:
end_date: 2025-05-08
location: Hamilton, ON, Canada
name: 'TACAS: Tools and Algorithms for the Construction and Analysis of Systems'
start_date: 2025-05-03
corr_author: '1'
date_created: 2025-05-25T22:17:04Z
date_published: 2025-05-01T00:00:00Z
date_updated: 2025-06-02T07:21:41Z
day: '01'
ddc:
- '000'
department:
- _id: ToHe
doi: 10.1007/978-3-031-90660-2_14
ec_funded: 1
file:
- access_level: open_access
checksum: 3f604f25dbe37383acb7f8308aad3ca6
content_type: application/pdf
creator: dernst
date_created: 2025-06-02T07:10:35Z
date_updated: 2025-06-02T07:10:35Z
file_id: '19766'
file_name: 2025_TACAS_Chalupa.pdf
file_size: 259050
relation: main_file
success: 1
file_date_updated: 2025-06-02T07:10:35Z
fulldoi: https://doi.org/10.1007/978-3-031-90660-2_14
has_accepted_license: '1'
intvolume: ' 15698'
language:
- iso: eng
month: '05'
oa: 1
oa_version: Published Version
page: 212-216
project:
- _id: 62781420-2b32-11ec-9570-8d9b63373d4d
call_identifier: H2020
grant_number: '101020093'
name: Vigilant Algorithmic Monitoring of Software
publication: 31st International Conference on Tools and Algorithms for the Construction
and Analysis of Systems
publication_identifier:
eissn:
- 1611-3349
isbn:
- '9783031906596'
issn:
- 0302-9743
publication_status: published
publisher: Springer Nature
quality_controlled: '1'
scopus_import: '1'
status: public
title: 'BUBAAK: Dynamic cooperative verification'
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: 15698
year: '2025'
...
---
OA_type: closed access
_id: '20024'
abstract:
- lang: eng
text: 'Cooperative software verification divides the task of software verification
among several verification tools in order to increase efficiency and effectiveness.
The basic approach is to let verifiers work on different parts of a program and
at the end join verification results. While this idea is intuitively appealing,
cooperative verification is usually hindered by the fact that program decomposition
(1) is often static, disregarding strengths and weaknesses of employed verifiers,
and (2) often represents the decomposed program parts in a specific proprietary
format, thereby making the use of off-the-shelf verifiers in cooperative verification
difficult. In this paper, we propose a novel cooperative verification scheme that
we call dynamic program splitting (DPS). Splitting decomposes programs into (smaller)
programs, and thus directly enables the use of off-the-shelf tools. In DPS, splitting
is dynamically applied on demand: Verification starts by giving a verification
task (a program plus a correctness specification) to a verifier V1. Whenever V1
finds the current task to be hard to verify, it splits the task (i.e., the program)
and restarts verification on subtasks. DPS continues until (1) a violation is
found, (2) all subtasks are completed or (3) some user-defined stopping criterion
is met. In the latter case, the remaining uncompleted subtasks are merged into
a single one and are given to a next verifier V2, repeating the same procedure
on the still unverified program parts. This way, the decomposition is steered
by what is hard to verify for particular verifiers, leveraging their complementary
strengths. We have implemented dynamic program splitting and evaluated it on benchmarks
of the annual software verification competition SV-COMP. The evaluation shows
that cooperative verification with DPS is able to solve verification tasks that
none of the constituent verifiers can solve, without any significant overhead.'
acknowledgement: This work is partially supported by the German Research Foundation
(DFG) – WE2290/13-2 (Coop2), and in part by the ERC-2020-AdG 101020093.
article_processing_charge: No
author:
- first_name: Cedric
full_name: Richter, Cedric
last_name: Richter
- first_name: Marek
full_name: Chalupa, Marek
id: 87e34708-d6c6-11ec-9f5b-9391e7be2463
last_name: Chalupa
- first_name: Marie-Christine
full_name: Jakobs, Marie-Christine
last_name: Jakobs
- first_name: Heike
full_name: Wehrheim, Heike
last_name: Wehrheim
citation:
ama: 'Richter C, Chalupa M, Jakobs M-C, Wehrheim H. Cooperative software verification
via dynamic program splitting. In: 47th International Conference on Software
Engineering. IEEE; 2025:2087-2099. doi:10.1109/ICSE55347.2025.00092'
apa: 'Richter, C., Chalupa, M., Jakobs, M.-C., & Wehrheim, H. (2025). Cooperative
software verification via dynamic program splitting. In 47th International
Conference on Software Engineering (pp. 2087–2099). Ottawa, ON, Canada: IEEE.
https://doi.org/10.1109/ICSE55347.2025.00092'
chicago: Richter, Cedric, Marek Chalupa, Marie-Christine Jakobs, and Heike Wehrheim.
“Cooperative Software Verification via Dynamic Program Splitting.” In 47th
International Conference on Software Engineering, 2087–99. IEEE, 2025. https://doi.org/10.1109/ICSE55347.2025.00092.
ieee: C. Richter, M. Chalupa, M.-C. Jakobs, and H. Wehrheim, “Cooperative software
verification via dynamic program splitting,” in 47th International Conference
on Software Engineering, Ottawa, ON, Canada, 2025, pp. 2087–2099.
ista: 'Richter C, Chalupa M, Jakobs M-C, Wehrheim H. 2025. Cooperative software
verification via dynamic program splitting. 47th International Conference on Software
Engineering. ICSE: International Conference on Software Engineering, 2087–2099.'
mla: Richter, Cedric, et al. “Cooperative Software Verification via Dynamic Program
Splitting.” 47th International Conference on Software Engineering, IEEE,
2025, pp. 2087–99, doi:10.1109/ICSE55347.2025.00092.
short: C. Richter, M. Chalupa, M.-C. Jakobs, H. Wehrheim, in:, 47th International
Conference on Software Engineering, IEEE, 2025, pp. 2087–2099.
conference:
end_date: 2025-05-06
location: Ottawa, ON, Canada
name: 'ICSE: International Conference on Software Engineering'
start_date: 2025-04-26
corr_author: '1'
date_created: 2025-07-16T11:32:29Z
date_published: 2025-05-01T00:00:00Z
date_updated: 2025-09-30T14:01:55Z
day: '01'
department:
- _id: ToHe
doi: 10.1109/ICSE55347.2025.00092
ec_funded: 1
external_id:
isi:
- '001538318100163'
fulldoi: https://doi.org/10.1109/ICSE55347.2025.00092
isi: 1
language:
- iso: eng
month: '05'
oa_version: None
page: 2087-2099
project:
- _id: 62781420-2b32-11ec-9570-8d9b63373d4d
call_identifier: H2020
grant_number: '101020093'
name: Vigilant Algorithmic Monitoring of Software
publication: 47th International Conference on Software Engineering
publication_identifier:
eissn:
- 1558-1225
isbn:
- '9798331505691'
publication_status: published
publisher: IEEE
quality_controlled: '1'
scopus_import: '1'
status: public
title: Cooperative software verification via dynamic program splitting
type: conference
user_id: 317138e5-6ab7-11ef-aa6d-ffef3953e345
year: '2025'
...
---
OA_place: publisher
OA_type: hybrid
_id: '18169'
abstract:
- lang: eng
text: "As the complexity and criticality of software increase every year, so does
the importance of runtime monitoring. Third-party and best-effort monitoring are
especially valuable, yet under-explored areas of runtime monitoring. In this context,
third-party monitoring means monitoring with a limited knowledge of the monitored
software (as it has been developed by a third party). Best-effort monitoring keeps
pace with the monitored software at the cost of possibly imprecise verdicts when
keeping up with the monitored software would not be feasible. Most existing monitoring
frameworks do not support the combination of third-party and best-effort monitoring
because they either require the full access to the monitored code or the ability
to process all observable events, or both.\r\nWe present a middleware framework,
Vamos, for the runtime monitoring of software. Vamos is explicitly designed to
support third-party and best-effort scenarios. The design goals of Vamos are (i)
efficiency (tracing events with low overhead), (ii) flexibility (the ability to
monitor a variety of different event channels, and to connect to a wide range
of monitors), 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 a set
of experiments demonstrating the usability of the scheme. The results indicate
that Vamos enables writing useful yet efficient monitors, 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 STTT reviewers for their valuable feedback and suggestions.
article_number: '103212'
article_processing_charge: Yes (via OA deal)
article_type: original
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. Science of Computer Programming. 2025;240(2). doi:10.1016/j.scico.2024.103212'
apa: 'Chalupa, M., Mühlböck, F., Muroya Lei, S., & Henzinger, T. A. (2025).
VAMOS: Middleware for best-effort third-party monitoring. Science of Computer
Programming. Elsevier. https://doi.org/10.1016/j.scico.2024.103212'
chicago: 'Chalupa, Marek, Fabian Mühlböck, Stefanie Muroya Lei, and Thomas A Henzinger.
“VAMOS: Middleware for Best-Effort Third-Party Monitoring.” Science of Computer
Programming. Elsevier, 2025. https://doi.org/10.1016/j.scico.2024.103212.'
ieee: 'M. Chalupa, F. Mühlböck, S. Muroya Lei, and T. A. Henzinger, “VAMOS: Middleware
for best-effort third-party monitoring,” Science of Computer Programming,
vol. 240, no. 2. Elsevier, 2025.'
ista: 'Chalupa M, Mühlböck F, Muroya Lei S, Henzinger TA. 2025. VAMOS: Middleware
for best-effort third-party monitoring. Science of Computer Programming. 240(2),
103212.'
mla: 'Chalupa, Marek, et al. “VAMOS: Middleware for Best-Effort Third-Party Monitoring.”
Science of Computer Programming, vol. 240, no. 2, 103212, Elsevier, 2025,
doi:10.1016/j.scico.2024.103212.'
short: M. Chalupa, F. Mühlböck, S. Muroya Lei, T.A. Henzinger, Science of Computer
Programming 240 (2025).
corr_author: '1'
date_created: 2024-10-06T22:01:10Z
date_published: 2025-02-01T00:00:00Z
date_updated: 2025-09-09T12:25:29Z
day: '01'
ddc:
- '000'
department:
- _id: ToHe
doi: 10.1016/j.scico.2024.103212
ec_funded: 1
external_id:
isi:
- '001327852600001'
file:
- access_level: open_access
checksum: cd93c0c356e479ffccfbe8499b6ba8e2
content_type: application/pdf
creator: dernst
date_created: 2025-01-13T09:02:47Z
date_updated: 2025-01-13T09:02:47Z
file_id: '18831'
file_name: 2024_ScienceCompProg_Chalupa.pdf
file_size: 1173677
relation: main_file
success: 1
file_date_updated: 2025-01-13T09:02:47Z
fulldoi: https://doi.org/10.1016/j.scico.2024.103212
has_accepted_license: '1'
intvolume: ' 240'
isi: 1
issue: '2'
language:
- iso: eng
month: '02'
oa: 1
oa_version: Published Version
project:
- _id: 62781420-2b32-11ec-9570-8d9b63373d4d
call_identifier: H2020
grant_number: '101020093'
name: Vigilant Algorithmic Monitoring of Software
publication: Science of Computer Programming
publication_identifier:
issn:
- 0167-6423
publication_status: published
publisher: Elsevier
quality_controlled: '1'
related_material:
record:
- id: '12856'
relation: earlier_version
status: public
scopus_import: '1'
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: journal_article
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 240
year: '2025'
...
---
OA_place: publisher
OA_type: hybrid
_id: '19741'
abstract:
- lang: eng
text: 'Quantitative automata model beyond-boolean aspects of systems: every execution
is mapped to a real number by incorporating weighted transitions and value functions
that generalize acceptance conditions of boolean w-automata. Despite the theoretical
advances in systems analysis through quantitative automata, the first comprehensive
software tool for quantitative automata (Quantitative Automata Kit, or QuAK) was
developed only recently. QuAK implements algorithms for solving standard decision
problems, e.g., emptiness and universality, as well as constructions for safety
and liveness of quantitative automata. We present the architecture of QuAK, which
reflects that all of these problems reduce to either checking inclusion between
two quantitative automata or computing the highest value achievable by an automaton—its
so-called top value. We improve QuAK by extending these two algorithms with an
option to return, alongside their results, an ultimately periodic word witnessing
the algorithm’s output, as well as implementing a new safety-liveness decomposition
algorithm that can handle nondeterministic automata, making QuAK more informative
and capable.'
acknowledgement: This work was supported in part by the ERC-2020-AdG 101020093.
alternative_title:
- LNCS
article_processing_charge: No
arxiv: 1
author:
- first_name: Marek
full_name: Chalupa, Marek
id: 87e34708-d6c6-11ec-9f5b-9391e7be2463
last_name: Chalupa
- first_name: Thomas A
full_name: Henzinger, Thomas A
id: 40876CD8-F248-11E8-B48F-1D18A9856A87
last_name: Henzinger
orcid: 0000-0002-2985-7724
- first_name: Nicolas Adrien
full_name: Mazzocchi, Nicolas Adrien
id: b26baa86-3308-11ec-87b0-8990f34baa85
last_name: Mazzocchi
- first_name: Naci E
full_name: Sarac, Naci E
id: 8C6B42F8-C8E6-11E9-A03A-F2DCE5697425
last_name: Sarac
citation:
ama: 'Chalupa M, Henzinger TA, Mazzocchi NA, Sarac NE. Automating the analysis of
quantitative automata with QuAK. In: 31st International Conference on Tools
and Algorithms for the Construction and Analysis of Systems. Vol 15696. Springer
Nature; 2025:303-312. doi:10.1007/978-3-031-90643-5_16'
apa: Chalupa, M., Henzinger, T. A., Mazzocchi, N. A., & Sarac, N. E. (2025).
Automating the analysis of quantitative automata with QuAK. In 31st International
Conference on Tools and Algorithms for the Construction and Analysis of Systems
(Vol. 15696, pp. 303–312). Springer Nature. https://doi.org/10.1007/978-3-031-90643-5_16
chicago: Chalupa, Marek, Thomas A Henzinger, Nicolas Adrien Mazzocchi, and Naci
E Sarac. “Automating the Analysis of Quantitative Automata with QuAK.” In 31st
International Conference on Tools and Algorithms for the Construction and Analysis
of Systems, 15696:303–12. Springer Nature, 2025. https://doi.org/10.1007/978-3-031-90643-5_16.
ieee: M. Chalupa, T. A. Henzinger, N. A. Mazzocchi, and N. E. Sarac, “Automating
the analysis of quantitative automata with QuAK,” in 31st International Conference
on Tools and Algorithms for the Construction and Analysis of Systems, 2025,
vol. 15696, pp. 303–312.
ista: Chalupa M, Henzinger TA, Mazzocchi NA, Sarac NE. 2025. Automating the analysis
of quantitative automata with QuAK. 31st International Conference on Tools and
Algorithms for the Construction and Analysis of Systems. , LNCS, vol. 15696, 303–312.
mla: Chalupa, Marek, et al. “Automating the Analysis of Quantitative Automata with
QuAK.” 31st International Conference on Tools and Algorithms for the Construction
and Analysis of Systems, vol. 15696, Springer Nature, 2025, pp. 303–12, doi:10.1007/978-3-031-90643-5_16.
short: M. Chalupa, T.A. Henzinger, N.A. Mazzocchi, N.E. Sarac, in:, 31st International
Conference on Tools and Algorithms for the Construction and Analysis of Systems,
Springer Nature, 2025, pp. 303–312.
corr_author: '1'
date_created: 2025-05-25T22:17:07Z
date_published: 2025-05-01T00:00:00Z
date_updated: 2026-07-27T12:48:18Z
day: '01'
ddc:
- '000'
department:
- _id: ToHe
doi: 10.1007/978-3-031-90643-5_16
ec_funded: 1
external_id:
arxiv:
- '2501.16088'
file:
- access_level: open_access
checksum: a27fa245be8d83421e9127b48a09c8af
content_type: application/pdf
creator: dernst
date_created: 2025-06-02T08:13:11Z
date_updated: 2025-06-02T08:13:11Z
file_id: '19768'
file_name: 2025_TACAS_ChalupaMarek.pdf
file_size: 420669
relation: main_file
success: 1
file_date_updated: 2025-06-02T08:13:11Z
fulldoi: https://doi.org/10.1007/978-3-031-90643-5_16
has_accepted_license: '1'
intvolume: ' 15696'
language:
- iso: eng
month: '05'
oa: 1
oa_version: Published Version
page: 303-312
project:
- _id: 62781420-2b32-11ec-9570-8d9b63373d4d
call_identifier: H2020
grant_number: '101020093'
name: Vigilant Algorithmic Monitoring of Software
publication: 31st International Conference on Tools and Algorithms for the Construction
and Analysis of Systems
publication_identifier:
eissn:
- 1611-3349
isbn:
- '9783031906428'
issn:
- 0302-9743
publication_status: published
publisher: Springer Nature
quality_controlled: '1'
related_material:
record:
- id: '20147'
relation: dissertation_contains
status: public
scopus_import: '1'
status: public
title: Automating the analysis of quantitative automata with QuAK
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: 15696
year: '2025'
...
---
_id: '15333'
abstract:
- lang: eng
text: BUBAAK-SpLit is a tool for dynamically splitting verification tasks into parts
that can then be analyzed in parallel. It is built on top of BUBAAK, a tool designed
for running combinations of verifiers in parallel. In contrast to BUBAAK, that
directly invokes verifiers on the inputs, BUBAAK-SpLit first starts by splitting
the input program into multiple modified versions called program splits. During
the splitting process, BUBAAK-SpLit utilizes a weak verifier (in our case symbolic
execution with a short timelimit) to analyze each generated program split. If
the weak verifier fails on a program split, we split this program split again
and start the verification process again on the generated program splits. We run
the splitting process until a predefined number of hard-to-verify program splits
is generated or a splitting limit is reached. During the main verification phase,
we run a combination of BUBAAK-LEE and SLOWBEAST in parallel on the remaining
unsolved parts of the verification task.
acknowledgement: This work was partially supported by the ERC-2020-AdG 10102009 grant.
alternative_title:
- LNCS
article_processing_charge: Yes (in subscription journal)
author:
- first_name: Marek
full_name: Chalupa, Marek
id: 87e34708-d6c6-11ec-9f5b-9391e7be2463
last_name: Chalupa
- first_name: Cedric
full_name: Richter, Cedric
last_name: Richter
citation:
ama: 'Chalupa M, Richter C. Bubaak-SpLit: Split what you cannot verify (Competition
contribution). In: 30th International Conference on Tools and Algorithms for
the Construction and Analysis of Systems. Vol 14572. Springer Nature; 2024:353–358.
doi:10.1007/978-3-031-57256-2_20'
apa: 'Chalupa, M., & Richter, C. (2024). Bubaak-SpLit: Split what you cannot
verify (Competition contribution). In 30th International Conference on Tools
and Algorithms for the Construction and Analysis of Systems (Vol. 14572, pp.
353–358). Luxembourg City, Luxembourg: Springer Nature. https://doi.org/10.1007/978-3-031-57256-2_20'
chicago: 'Chalupa, Marek, and Cedric Richter. “Bubaak-SpLit: Split What You Cannot
Verify (Competition Contribution).” In 30th International Conference on Tools
and Algorithms for the Construction and Analysis of Systems, 14572:353–358.
Springer Nature, 2024. https://doi.org/10.1007/978-3-031-57256-2_20.'
ieee: 'M. Chalupa and C. Richter, “Bubaak-SpLit: Split what you cannot verify (Competition
contribution),” in 30th International Conference on Tools and Algorithms for
the Construction and Analysis of Systems, Luxembourg City, Luxembourg, 2024,
vol. 14572, pp. 353–358.'
ista: 'Chalupa M, Richter C. 2024. Bubaak-SpLit: Split what you cannot verify (Competition
contribution). 30th International Conference on Tools and Algorithms for the Construction
and Analysis of Systems. TACAS: Tools and Algorithms for the Construction and
Analysis of Systems, LNCS, vol. 14572, 353–358.'
mla: 'Chalupa, Marek, and Cedric Richter. “Bubaak-SpLit: Split What You Cannot Verify
(Competition Contribution).” 30th International Conference on Tools and Algorithms
for the Construction and Analysis of Systems, vol. 14572, Springer Nature,
2024, pp. 353–358, doi:10.1007/978-3-031-57256-2_20.'
short: M. Chalupa, C. Richter, in:, 30th International Conference on Tools and Algorithms
for the Construction and Analysis of Systems, Springer Nature, 2024, pp. 353–358.
conference:
end_date: 2024-04-11
location: Luxembourg City, Luxembourg
name: 'TACAS: Tools and Algorithms for the Construction and Analysis of Systems'
start_date: 2024-04-06
corr_author: '1'
date_created: 2024-04-20T18:14:06Z
date_published: 2024-04-05T00:00:00Z
date_updated: 2025-09-04T13:48:25Z
day: '05'
ddc:
- '000'
department:
- _id: ToHe
doi: 10.1007/978-3-031-57256-2_20
ec_funded: 1
external_id:
isi:
- '001284187100020'
file:
- access_level: open_access
checksum: 208c855c60824bec936b8d01d0396474
content_type: application/pdf
creator: cchlebak
date_created: 2024-04-26T11:27:26Z
date_updated: 2024-04-26T11:27:26Z
file_id: '15347'
file_name: 2024_LNCS_Chalupa.pdf
file_size: 577128
relation: main_file
success: 1
file_date_updated: 2024-04-26T11:27:26Z
fulldoi: https://doi.org/10.1007/978-3-031-57256-2_20
has_accepted_license: '1'
intvolume: ' 14572'
isi: 1
language:
- iso: eng
month: '04'
oa: 1
oa_version: Published Version
page: 353–358
project:
- _id: 62781420-2b32-11ec-9570-8d9b63373d4d
call_identifier: H2020
grant_number: '101020093'
name: Vigilant Algorithmic Monitoring of Software
publication: 30th International Conference on Tools and Algorithms for the Construction
and Analysis of Systems
publication_identifier:
eisbn:
- '9783031572562'
eissn:
- 1611-3349
isbn:
- '9783031572555'
issn:
- 0302-9743
publication_status: published
publisher: Springer Nature
quality_controlled: '1'
scopus_import: '1'
status: public
title: 'Bubaak-SpLit: Split what you cannot verify (Competition contribution)'
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: 317138e5-6ab7-11ef-aa6d-ffef3953e345
volume: 14572
year: '2024'
...
---
OA_type: closed access
_id: '18599'
abstract:
- lang: eng
text: "Hypernode logic can reason about the prefix relation on stutter-reduced finite
traces through the stutter-reduced prefix predicate. We increase the expressiveness
of hypernode logic in two ways. First, we split the stutter-reduced prefix predicate
into an explicit stutter-reduction operator and the classical prefix predicate
on words. This change gives hypernode logic the ability to combine synchronous
and asynchronous reasoning by explicitly stating which parts of traces can stutter.
Second, we allow the use of regular expressions in formulas to reason about the
structure of traces. This change enables hypernode logic to describe a mixture
of trace properties and hyperproperties.\r\n\r\nWe show how to translate extended
hypernode logic formulas into multi-track automata, which are automata that read
multiple input words. Then we describe a fully online monitoring algorithm for
monitoring k-safety hyperproperties specified in the logic. We have implemented
the monitoring algorithm, and evaluated it on monitoring synchronous and asynchronous
versions of observational determinism, and on checking the privacy preservation
by compiler optimizations."
acknowledgement: This work was supported in part by the ERC-2020-AdG 101020093, and
by the Austrian Science Fund (FWF) SFB project SpyCoDe F8502.
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: Thomas A
full_name: Henzinger, Thomas A
id: 40876CD8-F248-11E8-B48F-1D18A9856A87
last_name: Henzinger
orcid: 0000-0002-2985-7724
- first_name: Ana
full_name: Oliveira da Costa, Ana
id: f347ec37-6676-11ee-b395-a888cb7b4fb4
last_name: Oliveira da Costa
orcid: 0000-0002-8741-5799
citation:
ama: 'Chalupa M, Henzinger TA, Oliveira da Costa A. Monitoring extended hypernode
logic. In: Integrated Formal Methods. Vol 15234. Springer Nature; 2024:151-171.
doi:10.1007/978-3-031-76554-4_9'
apa: Chalupa, M., Henzinger, T. A., & Oliveira da Costa, A. (2024). Monitoring
extended hypernode logic. In Integrated Formal Methods (Vol. 15234, pp.
151–171). Springer Nature. https://doi.org/10.1007/978-3-031-76554-4_9
chicago: Chalupa, Marek, Thomas A Henzinger, and Ana Oliveira da Costa. “Monitoring
Extended Hypernode Logic.” In Integrated Formal Methods, 15234:151–71.
Springer Nature, 2024. https://doi.org/10.1007/978-3-031-76554-4_9.
ieee: M. Chalupa, T. A. Henzinger, and A. Oliveira da Costa, “Monitoring extended
hypernode logic,” in Integrated Formal Methods, 2024, vol. 15234, pp. 151–171.
ista: Chalupa M, Henzinger TA, Oliveira da Costa A. 2024. Monitoring extended hypernode
logic. Integrated Formal Methods. , LNCS, vol. 15234, 151–171.
mla: Chalupa, Marek, et al. “Monitoring Extended Hypernode Logic.” Integrated
Formal Methods, vol. 15234, Springer Nature, 2024, pp. 151–71, doi:10.1007/978-3-031-76554-4_9.
short: M. Chalupa, T.A. Henzinger, A. Oliveira da Costa, in:, Integrated Formal
Methods, Springer Nature, 2024, pp. 151–171.
corr_author: '1'
date_created: 2024-12-01T23:01:52Z
date_published: 2024-11-13T00:00:00Z
date_updated: 2025-09-08T14:47:22Z
day: '13'
department:
- _id: ToHe
doi: 10.1007/978-3-031-76554-4_9
ec_funded: 1
external_id:
isi:
- '001416640500009'
fulldoi: https://doi.org/10.1007/978-3-031-76554-4_9
intvolume: ' 15234'
isi: 1
language:
- iso: eng
month: '11'
oa_version: None
page: 151-171
project:
- _id: 62781420-2b32-11ec-9570-8d9b63373d4d
call_identifier: H2020
grant_number: '101020093'
name: Vigilant Algorithmic Monitoring of Software
- _id: 34a1b658-11ca-11ed-8bc3-c75229f0241e
grant_number: F8502
name: Interface Theory for Security and Privacy
publication: Integrated Formal Methods
publication_identifier:
eissn:
- 1611-3349
isbn:
- '9783031765537'
issn:
- 0302-9743
publication_status: published
publisher: Springer Nature
quality_controlled: '1'
scopus_import: '1'
status: public
title: Monitoring extended hypernode logic
type: conference
user_id: 317138e5-6ab7-11ef-aa6d-ffef3953e345
volume: 15234
year: '2024'
...
---
APC_amount: 2748 EUR
OA_place: publisher
OA_type: hybrid
_id: '17634'
abstract:
- lang: eng
text: System behaviors are traditionally evaluated through binary classifications
of correctness, which do not suffice for properties involving quantitative aspects
of systems and executions. Quantitative automata offer a more nuanced approach,
mapping each execution to a real number by incorporating weighted transitions
and value functions generalizing acceptance conditions. In this paper, we introduce
QuAK, the first tool designed to automate the analysis of quantitative automata.
QuAK currently supports a variety of quantitative automaton types, including Inf,
Sup, LimInf, LimSup, LimInfAvg, and LimSupAvg automata, and implements decision
procedures for problems such as emptiness, universality, inclusion, equivalence,
as well as for checking whether an automaton is safe, live, or constant. Additionally,
QuAK is able to compute extremal values when possible, construct safety-liveness
decompositions, and monitor system behaviors. We demonstrate the effectiveness
of QuAK through experiments focusing on the inclusion, constant-function check,
and monitoring problems.
acknowledgement: This work was supported in part by the ERC-2020-AdG 101020093. N.
Mazzocchi was affiliated with ISTA when his collaboration started.
alternative_title:
- LNCS
article_processing_charge: Yes (in subscription journal)
arxiv: 1
author:
- first_name: Marek
full_name: Chalupa, Marek
id: 87e34708-d6c6-11ec-9f5b-9391e7be2463
last_name: Chalupa
- first_name: Thomas A
full_name: Henzinger, Thomas A
id: 40876CD8-F248-11E8-B48F-1D18A9856A87
last_name: Henzinger
orcid: 0000-0002-2985-7724
- first_name: Nicolas Adrien
full_name: Mazzocchi, Nicolas Adrien
id: b26baa86-3308-11ec-87b0-8990f34baa85
last_name: Mazzocchi
- first_name: Naci E
full_name: Sarac, Naci E
id: 8C6B42F8-C8E6-11E9-A03A-F2DCE5697425
last_name: Sarac
citation:
ama: 'Chalupa M, Henzinger TA, Mazzocchi NA, Sarac NE. QuAK: Quantitative Automata
Kit. In: 12th International Symposium on Leveraging Applications of Formal
Methods, Verification and Validation. Vol 15222. Springer Nature; 2024:3-20.
doi:10.1007/978-3-031-75387-9_1'
apa: 'Chalupa, M., Henzinger, T. A., Mazzocchi, N. A., & Sarac, N. E. (2024).
QuAK: Quantitative Automata Kit. In 12th International Symposium on Leveraging
Applications of Formal Methods, Verification and Validation (Vol. 15222, pp.
3–20). Crete, Greece: Springer Nature. https://doi.org/10.1007/978-3-031-75387-9_1'
chicago: 'Chalupa, Marek, Thomas A Henzinger, Nicolas Adrien Mazzocchi, and Naci
E Sarac. “QuAK: Quantitative Automata Kit.” In 12th International Symposium
on Leveraging Applications of Formal Methods, Verification and Validation,
15222:3–20. Springer Nature, 2024. https://doi.org/10.1007/978-3-031-75387-9_1.'
ieee: 'M. Chalupa, T. A. Henzinger, N. A. Mazzocchi, and N. E. Sarac, “QuAK: Quantitative
Automata Kit,” in 12th International Symposium on Leveraging Applications of
Formal Methods, Verification and Validation, Crete, Greece, 2024, vol. 15222,
pp. 3–20.'
ista: 'Chalupa M, Henzinger TA, Mazzocchi NA, Sarac NE. 2024. QuAK: Quantitative
Automata Kit. 12th International Symposium on Leveraging Applications of Formal
Methods, Verification and Validation. ISoLA: International Symposium on Leveraging
Applications, LNCS, vol. 15222, 3–20.'
mla: 'Chalupa, Marek, et al. “QuAK: Quantitative Automata Kit.” 12th International
Symposium on Leveraging Applications of Formal Methods, Verification and Validation,
vol. 15222, Springer Nature, 2024, pp. 3–20, doi:10.1007/978-3-031-75387-9_1.'
short: M. Chalupa, T.A. Henzinger, N.A. Mazzocchi, N.E. Sarac, in:, 12th International
Symposium on Leveraging Applications of Formal Methods, Verification and Validation,
Springer Nature, 2024, pp. 3–20.
conference:
end_date: 2024-10-31
location: Crete, Greece
name: 'ISoLA: International Symposium on Leveraging Applications'
start_date: 2024-10-27
corr_author: '1'
date_created: 2024-09-05T14:27:08Z
date_published: 2024-10-26T00:00:00Z
date_updated: 2026-07-27T12:48:18Z
day: '26'
ddc:
- '000'
department:
- _id: GradSch
- _id: ToHe
doi: 10.1007/978-3-031-75387-9_1
ec_funded: 1
external_id:
arxiv:
- '2409.03569'
isi:
- '001419008700001'
file:
- access_level: open_access
checksum: 43e432f82be376434b358f3dd7a94b71
content_type: application/pdf
creator: esarac
date_created: 2024-09-05T14:26:02Z
date_updated: 2024-09-05T14:26:02Z
file_id: '17635'
file_name: isola24.pdf
file_size: 847422
relation: main_file
success: 1
- access_level: open_access
checksum: 6bc04f07bb5612c0e7ea00ac121a69b6
content_type: application/pdf
creator: dernst
date_created: 2025-01-21T14:39:49Z
date_updated: 2025-01-21T14:39:49Z
file_id: '18865'
file_name: 2024_LNCS_Chalupa.pdf
file_size: 1358706
relation: main_file
success: 1
file_date_updated: 2025-01-21T14:39:49Z
fulldoi: https://doi.org/10.1007/978-3-031-75387-9_1
has_accepted_license: '1'
intvolume: ' 15222'
isi: 1
language:
- iso: eng
month: '10'
oa: 1
oa_version: Published Version
page: 3-20
project:
- _id: 62781420-2b32-11ec-9570-8d9b63373d4d
call_identifier: H2020
grant_number: '101020093'
name: Vigilant Algorithmic Monitoring of Software
publication: 12th International Symposium on Leveraging Applications of Formal Methods,
Verification and Validation
publication_identifier:
eissn:
- 1611-3349
isbn:
- '9783031753862'
issn:
- 0302-9743
publication_status: published
publisher: Springer Nature
quality_controlled: '1'
related_material:
record:
- id: '20147'
relation: dissertation_contains
status: public
scopus_import: '1'
status: public
title: 'QuAK: Quantitative Automata Kit'
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: 317138e5-6ab7-11ef-aa6d-ffef3953e345
volume: 15222
year: '2024'
...
---
_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. 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'
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.'
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.'
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. VAMOS: Middleware for Best-Effort Third-Party Monitoring.
Institute of Science and Technology Austria, 2023, doi:10.15479/AT:ISTA:12407.'
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.'
corr_author: '1'
date_created: 2023-01-27T03:18:08Z
date_published: 2023-01-27T00:00:00Z
date_updated: 2025-09-09T12:25:29Z
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
fulldoi: https://doi.org/10.15479/AT:ISTA:12407
has_accepted_license: '1'
keyword:
- runtime monitoring
- best effort
- third party
language:
- iso: eng
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: '12854'
abstract:
- lang: eng
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."
acknowledgement: This work was supported by the ERC-2020-AdG 10102009 grant.
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: 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, 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'
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'
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.'
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.'
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.'
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.'
short: M. Chalupa, T.A. Henzinger, in:, Tools and Algorithms for the Construction
and Analysis of Systems, Springer Nature, 2023, pp. 535–540.
conference:
end_date: 2023-04-27
location: Paris, France
name: 'TACAS: Tools and Algorithms for the Construction and Analysis of Systems'
start_date: 2023-04-22
corr_author: '1'
date_created: 2023-04-20T08:22:53Z
date_published: 2023-04-20T00:00:00Z
date_updated: 2025-09-09T12:24:56Z
day: '20'
ddc:
- '000'
department:
- _id: ToHe
doi: 10.1007/978-3-031-30820-8_32
ec_funded: 1
external_id:
isi:
- '001288698100041'
file:
- access_level: open_access
checksum: 120d2c2a38384058ad0630fdf8288312
content_type: application/pdf
creator: dernst
date_created: 2023-04-25T06:58:36Z
date_updated: 2023-04-25T06:58:36Z
file_id: '12864'
file_name: 2023_LNCS_Chalupa.pdf
file_size: 16096413
relation: main_file
success: 1
file_date_updated: 2023-04-25T06:58:36Z
fulldoi: https://doi.org/10.1007/978-3-031-30820-8_32
has_accepted_license: '1'
intvolume: ' 13994'
isi: 1
language:
- iso: eng
month: '04'
oa: 1
oa_version: Published Version
page: 535-540
project:
- _id: 62781420-2b32-11ec-9570-8d9b63373d4d
call_identifier: H2020
grant_number: '101020093'
name: Vigilant Algorithmic Monitoring of Software
publication: Tools and Algorithms for the Construction and Analysis of Systems
publication_identifier:
eisbn:
- '9783031308208'
eissn:
- 1611-3349
isbn:
- '9783031308192'
issn:
- 0302-9743
publication_status: published
publisher: Springer Nature
quality_controlled: '1'
scopus_import: '1'
status: public
title: 'Bubaak: Runtime monitoring of program verifiers'
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: 317138e5-6ab7-11ef-aa6d-ffef3953e345
volume: 13994
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: 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'
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.'
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.'
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.”
Fundamental Approaches to Software Engineering, vol. 13991, Springer Nature,
2023, pp. 260–81, doi: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.
conference:
end_date: 2023-04-27
location: Paris, France
name: 'FASE: Fundamental Approaches to Software Engineering'
start_date: 2023-04-22
corr_author: '1'
date_created: 2023-04-20T08:29:42Z
date_published: 2023-04-20T00:00:00Z
date_updated: 2025-09-09T12:25:29Z
day: '20'
ddc:
- '000'
department:
- _id: ToHe
doi: 10.1007/978-3-031-30826-0_15
ec_funded: 1
external_id:
isi:
- '001284136600015'
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
fulldoi: https://doi.org/10.1007/978-3-031-30826-0_15
has_accepted_license: '1'
intvolume: ' 13991'
isi: 1
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: '18169'
relation: later_version
status: public
- id: '12407'
relation: earlier_version
status: public
scopus_import: '1'
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: 317138e5-6ab7-11ef-aa6d-ffef3953e345
volume: 13991
year: '2023'
...
---
_id: '14076'
abstract:
- lang: eng
text: Hyperproperties are properties that relate multiple execution traces. Previous
work on monitoring hyperproperties focused on synchronous hyperproperties, usually
specified in HyperLTL. When monitoring synchronous hyperproperties, all traces
are assumed to proceed at the same speed. We introduce (multi-trace) prefix transducers
and show how to use them for monitoring synchronous as well as, for the first
time, asynchronous hyperproperties. Prefix transducers map multiple input traces
into one or more output traces by incrementally matching prefixes of the input
traces against expressions similar to regular expressions. The prefixes of different
traces which are consumed by a single matching step of the monitor may have different
lengths. The deterministic and executable nature of prefix transducers makes them
more suitable as an intermediate formalism for runtime verification than logical
specifications, which tend to be highly non-deterministic, especially in the case
of asynchronous hyperproperties. We report on a set of experiments about monitoring
asynchronous version of observational determinism.
acknowledgement: This work was supported in part by the ERC-2020-AdG 101020093. The
authors would like to thank Ana Oliveira da Costa for commenting on a draft of the
paper.
alternative_title:
- LNCS
article_processing_charge: Yes (in subscription journal)
author:
- first_name: Marek
full_name: Chalupa, Marek
id: 87e34708-d6c6-11ec-9f5b-9391e7be2463
last_name: Chalupa
- 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, Henzinger TA. Monitoring hyperproperties with prefix transducers.
In: 23nd International Conference on Runtime Verification. Vol 14245. Springer
Nature; 2023:168-190. doi:10.1007/978-3-031-44267-4_9'
apa: 'Chalupa, M., & Henzinger, T. A. (2023). Monitoring hyperproperties with
prefix transducers. In 23nd International Conference on Runtime Verification
(Vol. 14245, pp. 168–190). Thessaloniki, Greek: Springer Nature. https://doi.org/10.1007/978-3-031-44267-4_9'
chicago: Chalupa, Marek, and Thomas A Henzinger. “Monitoring Hyperproperties with
Prefix Transducers.” In 23nd International Conference on Runtime Verification,
14245:168–90. Springer Nature, 2023. https://doi.org/10.1007/978-3-031-44267-4_9.
ieee: M. Chalupa and T. A. Henzinger, “Monitoring hyperproperties with prefix transducers,”
in 23nd International Conference on Runtime Verification, Thessaloniki,
Greek, 2023, vol. 14245, pp. 168–190.
ista: 'Chalupa M, Henzinger TA. 2023. Monitoring hyperproperties with prefix transducers.
23nd International Conference on Runtime Verification. RV: Conference on Runtime
Verification, LNCS, vol. 14245, 168–190.'
mla: Chalupa, Marek, and Thomas A. Henzinger. “Monitoring Hyperproperties with Prefix
Transducers.” 23nd International Conference on Runtime Verification, vol.
14245, Springer Nature, 2023, pp. 168–90, doi:10.1007/978-3-031-44267-4_9.
short: M. Chalupa, T.A. Henzinger, in:, 23nd International Conference on Runtime
Verification, Springer Nature, 2023, pp. 168–190.
conference:
end_date: 2023-10-07
location: Thessaloniki, Greek
name: 'RV: Conference on Runtime Verification'
start_date: 2023-10-04
corr_author: '1'
date_created: 2023-08-16T20:46:08Z
date_published: 2023-10-01T00:00:00Z
date_updated: 2025-04-14T09:42:55Z
day: '01'
ddc:
- '000'
department:
- _id: ToHe
doi: 10.1007/978-3-031-44267-4_9
ec_funded: 1
file:
- access_level: open_access
checksum: ee33bd6f1a26f4dae7a8192584869fd8
content_type: application/pdf
creator: dernst
date_created: 2023-10-16T07:15:11Z
date_updated: 2023-10-16T07:15:11Z
file_id: '14430'
file_name: 2023_LNCS_RV_Chalupa.pdf
file_size: 867256
relation: main_file
success: 1
file_date_updated: 2023-10-16T07:15:11Z
fulldoi: https://doi.org/10.1007/978-3-031-44267-4_9
has_accepted_license: '1'
intvolume: ' 14245'
language:
- iso: eng
month: '10'
oa: 1
oa_version: Published Version
page: 168-190
project:
- _id: 62781420-2b32-11ec-9570-8d9b63373d4d
call_identifier: H2020
grant_number: '101020093'
name: Vigilant Algorithmic Monitoring of Software
publication: 23nd International Conference on Runtime Verification
publication_identifier:
eisbn:
- 978-3-031-44267-4
isbn:
- 978-3-031-44266-7
publication_status: published
publisher: Springer Nature
quality_controlled: '1'
related_material:
record:
- id: '15035'
relation: research_data
status: public
scopus_import: '1'
status: public
title: Monitoring hyperproperties with prefix transducers
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: 14245
year: '2023'
...
---
_id: '15035'
abstract:
- lang: eng
text: "This artifact aims to reproduce experiments from the paper Monitoring Hyperproperties
With Prefix Transducers accepted at RV'23, and give further pointers to implementation
of prefix transducers.\r\nIt has two parts: a pre-compiled docker image and sources
that one can use to compile (locally or in docker) the software and run the experiments."
article_processing_charge: No
author:
- first_name: Marek
full_name: Chalupa, Marek
id: 87e34708-d6c6-11ec-9f5b-9391e7be2463
last_name: Chalupa
- 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, Henzinger TA. Monitoring hyperproperties with prefix transducers.
2023. doi:10.5281/ZENODO.8191723
apa: Chalupa, M., & Henzinger, T. A. (2023). Monitoring hyperproperties with
prefix transducers. Zenodo. https://doi.org/10.5281/ZENODO.8191723
chicago: Chalupa, Marek, and Thomas A Henzinger. “Monitoring Hyperproperties with
Prefix Transducers.” Zenodo, 2023. https://doi.org/10.5281/ZENODO.8191723.
ieee: M. Chalupa and T. A. Henzinger, “Monitoring hyperproperties with prefix transducers.”
Zenodo, 2023.
ista: Chalupa M, Henzinger TA. 2023. Monitoring hyperproperties with prefix transducers,
Zenodo, 10.5281/ZENODO.8191723.
mla: Chalupa, Marek, and Thomas A. Henzinger. Monitoring Hyperproperties with
Prefix Transducers. Zenodo, 2023, doi:10.5281/ZENODO.8191723.
short: M. Chalupa, T.A. Henzinger, (2023).
corr_author: '1'
date_created: 2024-02-28T07:34:34Z
date_published: 2023-07-28T00:00:00Z
date_updated: 2025-04-14T09:42:55Z
day: '28'
ddc:
- '000'
department:
- _id: ToHe
doi: 10.5281/ZENODO.8191723
ec_funded: 1
fulldoi: https://doi.org/10.5281/ZENODO.8191723
has_accepted_license: '1'
main_file_link:
- open_access: '1'
url: https://doi.org/10.5281/zenodo.8191722
month: '07'
oa: 1
oa_version: Published Version
project:
- _id: 62781420-2b32-11ec-9570-8d9b63373d4d
call_identifier: H2020
grant_number: '101020093'
name: Vigilant Algorithmic Monitoring of Software
publisher: Zenodo
related_material:
record:
- id: '14076'
relation: used_in_publication
status: public
status: public
title: Monitoring hyperproperties with prefix transducers
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: research_data_reference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
year: '2023'
...