---
_id: '14739'
abstract:
- lang: eng
text: Attempts to incorporate topological information in supervised learning tasks
have resulted in the creation of several techniques for vectorizing persistent
homology barcodes. In this paper, we study thirteen such methods. Besides describing
an organizational framework for these methods, we comprehensively benchmark them
against three well-known classification tasks. Surprisingly, we discover that
the best-performing method is a simple vectorization, which consists only of a
few elementary summary statistics. Finally, we provide a convenient web application
which has been designed to facilitate exploration and experimentation with various
vectorization methods.
acknowledgement: "The work of Maria-Jose Jimenez, Eduardo Paluzo-Hidalgo and Manuel
Soriano-Trigueros was supported in part by the Spanish grant Ministerio de Ciencia
e Innovacion under Grants TED2021-129438B-I00 and PID2019-107339GB-I00, and in part
by REXASI-PRO H-EU project, call HORIZON-CL4-2021-HUMAN-01-01 under Grant 101070028.
The work of\r\nMaria-Jose Jimenez was supported by a grant of Convocatoria de la
Universidad de Sevilla para la recualificacion del sistema universitario español,
2021-23, funded by the European Union, NextGenerationEU. The work of Vidit Nanda
was supported in part by EPSRC under Grant EP/R018472/1 and in part by US AFOSR
under Grant FA9550-22-1-0462. \r\nWe are grateful to the team of GUDHI and TEASPOON
developers, for their work and their support. We are also grateful to Streamlit
for providing extra resources to deploy the web app\r\nonline on Streamlit community
cloud. We thank the anonymous referees for their helpful suggestions."
article_processing_charge: Yes (in subscription journal)
article_type: original
author:
- first_name: Dashti
full_name: Ali, Dashti
last_name: Ali
- first_name: Aras
full_name: Asaad, Aras
last_name: Asaad
- first_name: Maria-Jose
full_name: Jimenez, Maria-Jose
last_name: Jimenez
- first_name: Vidit
full_name: Nanda, Vidit
last_name: Nanda
- first_name: Eduardo
full_name: Paluzo-Hidalgo, Eduardo
last_name: Paluzo-Hidalgo
- first_name: Manuel
full_name: Soriano Trigueros, Manuel
id: 15ebd7cf-15bf-11ee-aebd-bb4bb5121ea8
last_name: Soriano Trigueros
orcid: 0000-0003-2449-1433
citation:
ama: Ali D, Asaad A, Jimenez M-J, Nanda V, Paluzo-Hidalgo E, Soriano Trigueros M.
A survey of vectorization methods in topological data analysis. IEEE Transactions
on Pattern Analysis and Machine Intelligence. 2023;45(12):14069-14080. doi:10.1109/tpami.2023.3308391
apa: Ali, D., Asaad, A., Jimenez, M.-J., Nanda, V., Paluzo-Hidalgo, E., & Soriano
Trigueros, M. (2023). A survey of vectorization methods in topological data analysis.
IEEE Transactions on Pattern Analysis and Machine Intelligence. IEEE. https://doi.org/10.1109/tpami.2023.3308391
chicago: Ali, Dashti, Aras Asaad, Maria-Jose Jimenez, Vidit Nanda, Eduardo Paluzo-Hidalgo,
and Manuel Soriano Trigueros. “A Survey of Vectorization Methods in Topological
Data Analysis.” IEEE Transactions on Pattern Analysis and Machine Intelligence.
IEEE, 2023. https://doi.org/10.1109/tpami.2023.3308391.
ieee: D. Ali, A. Asaad, M.-J. Jimenez, V. Nanda, E. Paluzo-Hidalgo, and M. Soriano
Trigueros, “A survey of vectorization methods in topological data analysis,” IEEE
Transactions on Pattern Analysis and Machine Intelligence, vol. 45, no. 12.
IEEE, pp. 14069–14080, 2023.
ista: Ali D, Asaad A, Jimenez M-J, Nanda V, Paluzo-Hidalgo E, Soriano Trigueros
M. 2023. A survey of vectorization methods in topological data analysis. IEEE
Transactions on Pattern Analysis and Machine Intelligence. 45(12), 14069–14080.
mla: Ali, Dashti, et al. “A Survey of Vectorization Methods in Topological Data
Analysis.” IEEE Transactions on Pattern Analysis and Machine Intelligence,
vol. 45, no. 12, IEEE, 2023, pp. 14069–80, doi:10.1109/tpami.2023.3308391.
short: D. Ali, A. Asaad, M.-J. Jimenez, V. Nanda, E. Paluzo-Hidalgo, M. Soriano
Trigueros, IEEE Transactions on Pattern Analysis and Machine Intelligence 45 (2023)
14069–14080.
date_created: 2024-01-08T09:59:46Z
date_published: 2023-12-01T00:00:00Z
date_updated: 2024-01-08T10:11:46Z
day: '01'
ddc:
- '000'
department:
- _id: HeEd
doi: 10.1109/tpami.2023.3308391
file:
- access_level: open_access
checksum: 465c28ef0b151b4b1fb47977ed5581ab
content_type: application/pdf
creator: dernst
date_created: 2024-01-08T10:09:14Z
date_updated: 2024-01-08T10:09:14Z
file_id: '14740'
file_name: 2023_IEEEToP_Ali.pdf
file_size: 2370988
relation: main_file
success: 1
file_date_updated: 2024-01-08T10:09:14Z
has_accepted_license: '1'
intvolume: ' 45'
issue: '12'
keyword:
- Applied Mathematics
- Artificial Intelligence
- Computational Theory and Mathematics
- Computer Vision and Pattern Recognition
- Software
language:
- iso: eng
month: '12'
oa: 1
oa_version: Published Version
page: 14069-14080
publication: IEEE Transactions on Pattern Analysis and Machine Intelligence
publication_identifier:
eissn:
- 1939-3539
issn:
- 0162-8828
publication_status: published
publisher: IEEE
quality_controlled: '1'
status: public
title: A survey of vectorization methods in topological data analysis
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: 45
year: '2023'
...
---
_id: '14778'
abstract:
- lang: eng
text: 'We consider the almost-sure (a.s.) termination problem for probabilistic
programs, which are a stochastic extension of classical imperative programs. Lexicographic
ranking functions provide a sound and practical approach for termination of non-probabilistic
programs, and their extension to probabilistic programs is achieved via lexicographic
ranking supermartingales (LexRSMs). However, LexRSMs introduced in the previous
work have a limitation that impedes their automation: all of their components
have to be non-negative in all reachable states. This might result in a LexRSM
not existing even for simple terminating programs. Our contributions are twofold.
First, we introduce a generalization of LexRSMs that allows for some components
to be negative. This standard feature of non-probabilistic termination proofs
was hitherto not known to be sound in the probabilistic setting, as the soundness
proof requires a careful analysis of the underlying stochastic process. Second,
we present polynomial-time algorithms using our generalized LexRSMs for proving
a.s. termination in broad classes of linear-arithmetic programs.'
acknowledgement: This research was partially supported by the ERC CoG (grant no. 863818;
ForM-SMArt), the Czech Science Foundation (grant no. GA21-24711S), and the European
Union’s Horizon 2020 research and innovation program under the Marie Skłodowska-Curie
Grant Agreement No. 665385.
article_number: '11'
article_processing_charge: Yes (via OA deal)
article_type: original
arxiv: 1
author:
- first_name: Krishnendu
full_name: Chatterjee, Krishnendu
id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
last_name: Chatterjee
orcid: 0000-0002-4561-241X
- first_name: Ehsan
full_name: Kafshdar Goharshady, Ehsan
last_name: Kafshdar Goharshady
- first_name: Petr
full_name: Novotný, Petr
id: 3CC3B868-F248-11E8-B48F-1D18A9856A87
last_name: Novotný
- first_name: Jiří
full_name: Zárevúcky, Jiří
last_name: Zárevúcky
- first_name: Dorde
full_name: Zikelic, Dorde
id: 294AA7A6-F248-11E8-B48F-1D18A9856A87
last_name: Zikelic
orcid: 0000-0002-4681-1699
citation:
ama: Chatterjee K, Kafshdar Goharshady E, Novotný P, Zárevúcky J, Zikelic D. On
lexicographic proof rules for probabilistic termination. Formal Aspects of
Computing. 2023;35(2). doi:10.1145/3585391
apa: Chatterjee, K., Kafshdar Goharshady, E., Novotný, P., Zárevúcky, J., &
Zikelic, D. (2023). On lexicographic proof rules for probabilistic termination.
Formal Aspects of Computing. Association for Computing Machinery. https://doi.org/10.1145/3585391
chicago: Chatterjee, Krishnendu, Ehsan Kafshdar Goharshady, Petr Novotný, Jiří Zárevúcky,
and Dorde Zikelic. “On Lexicographic Proof Rules for Probabilistic Termination.”
Formal Aspects of Computing. Association for Computing Machinery, 2023.
https://doi.org/10.1145/3585391.
ieee: K. Chatterjee, E. Kafshdar Goharshady, P. Novotný, J. Zárevúcky, and D. Zikelic,
“On lexicographic proof rules for probabilistic termination,” Formal Aspects
of Computing, vol. 35, no. 2. Association for Computing Machinery, 2023.
ista: Chatterjee K, Kafshdar Goharshady E, Novotný P, Zárevúcky J, Zikelic D. 2023.
On lexicographic proof rules for probabilistic termination. Formal Aspects of
Computing. 35(2), 11.
mla: Chatterjee, Krishnendu, et al. “On Lexicographic Proof Rules for Probabilistic
Termination.” Formal Aspects of Computing, vol. 35, no. 2, 11, Association
for Computing Machinery, 2023, doi:10.1145/3585391.
short: K. Chatterjee, E. Kafshdar Goharshady, P. Novotný, J. Zárevúcky, D. Zikelic,
Formal Aspects of Computing 35 (2023).
date_created: 2024-01-10T09:27:43Z
date_published: 2023-06-23T00:00:00Z
date_updated: 2025-07-14T09:10:10Z
day: '23'
ddc:
- '000'
department:
- _id: KrCh
doi: 10.1145/3585391
ec_funded: 1
external_id:
arxiv:
- '2108.02188'
file:
- access_level: open_access
checksum: 3bb133eeb27ec01649a9a36445d952d9
content_type: application/pdf
creator: dernst
date_created: 2024-01-16T08:11:24Z
date_updated: 2024-01-16T08:11:24Z
file_id: '14804'
file_name: 2023_FormalAspectsComputing_Chatterjee.pdf
file_size: 502522
relation: main_file
success: 1
file_date_updated: 2024-01-16T08:11:24Z
has_accepted_license: '1'
intvolume: ' 35'
issue: '2'
keyword:
- Theoretical Computer Science
- Software
language:
- iso: eng
month: '06'
oa: 1
oa_version: Published Version
project:
- _id: 0599E47C-7A3F-11EA-A408-12923DDC885E
call_identifier: H2020
grant_number: '863818'
name: 'Formal Methods for Stochastic Models: Algorithms and Applications'
- _id: 2564DBCA-B435-11E9-9278-68D0E5697425
call_identifier: H2020
grant_number: '665385'
name: International IST Doctoral Program
publication: Formal Aspects of Computing
publication_identifier:
eissn:
- 1433-299X
issn:
- 0934-5043
publication_status: published
publisher: Association for Computing Machinery
quality_controlled: '1'
related_material:
record:
- id: '10414'
relation: earlier_version
status: public
status: public
title: On lexicographic proof rules for probabilistic termination
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: 35
year: '2023'
...
---
_id: '10602'
abstract:
- lang: eng
text: Transforming ω-automata into parity automata is traditionally done using appearance
records. We present an efficient variant of this idea, tailored to Rabin automata,
and several optimizations applicable to all appearance records. We compare the
methods experimentally and show that our method produces significantly smaller
automata than previous approaches.
acknowledgement: This work is partially funded by the German Research Foundation (DFG)
projects Verified Model Checkers (No. 317422601) and Statistical Unbounded Verification
(No. 383882557), and the Alexander von Humboldt Foundation with funds from the German
Federal Ministry of Education and Research. It is an extended version of [21], including
all proofs together with further explanations and examples. Moreover, we provide
a new, more efficient construction based on (total) preorders, unifying previous
optimizations. Experiments are performed with a new, performant implementation,
comparing our approach to the current state of the art.
article_processing_charge: Yes (via OA deal)
article_type: original
author:
- first_name: Jan
full_name: Kretinsky, Jan
id: 44CEF464-F248-11E8-B48F-1D18A9856A87
last_name: Kretinsky
orcid: 0000-0002-8122-2881
- first_name: Tobias
full_name: Meggendorfer, Tobias
id: b21b0c15-30a2-11eb-80dc-f13ca25802e1
last_name: Meggendorfer
orcid: 0000-0002-1712-2165
- first_name: Clara
full_name: Waldmann, Clara
last_name: Waldmann
- first_name: Maximilian
full_name: Weininger, Maximilian
last_name: Weininger
citation:
ama: Kretinsky J, Meggendorfer T, Waldmann C, Weininger M. Index appearance record
with preorders. Acta Informatica. 2022;59:585-618. doi:10.1007/s00236-021-00412-y
apa: Kretinsky, J., Meggendorfer, T., Waldmann, C., & Weininger, M. (2022).
Index appearance record with preorders. Acta Informatica. Springer Nature.
https://doi.org/10.1007/s00236-021-00412-y
chicago: Kretinsky, Jan, Tobias Meggendorfer, Clara Waldmann, and Maximilian Weininger.
“Index Appearance Record with Preorders.” Acta Informatica. Springer Nature,
2022. https://doi.org/10.1007/s00236-021-00412-y.
ieee: J. Kretinsky, T. Meggendorfer, C. Waldmann, and M. Weininger, “Index appearance
record with preorders,” Acta Informatica, vol. 59. Springer Nature, pp.
585–618, 2022.
ista: Kretinsky J, Meggendorfer T, Waldmann C, Weininger M. 2022. Index appearance
record with preorders. Acta Informatica. 59, 585–618.
mla: Kretinsky, Jan, et al. “Index Appearance Record with Preorders.” Acta Informatica,
vol. 59, Springer Nature, 2022, pp. 585–618, doi:10.1007/s00236-021-00412-y.
short: J. Kretinsky, T. Meggendorfer, C. Waldmann, M. Weininger, Acta Informatica
59 (2022) 585–618.
date_created: 2022-01-06T12:37:27Z
date_published: 2022-10-01T00:00:00Z
date_updated: 2023-08-02T13:49:28Z
day: '01'
ddc:
- '000'
department:
- _id: KrCh
doi: 10.1007/s00236-021-00412-y
external_id:
isi:
- '000735765500001'
file:
- access_level: open_access
checksum: bf1c195b6aaf59e8530cf9e3a9d731f7
content_type: application/pdf
creator: cchlebak
date_created: 2022-01-07T07:50:31Z
date_updated: 2022-01-07T07:50:31Z
file_id: '10603'
file_name: 2021_ActaInfor_Křetínský.pdf
file_size: 1066082
relation: main_file
success: 1
file_date_updated: 2022-01-07T07:50:31Z
has_accepted_license: '1'
intvolume: ' 59'
isi: 1
keyword:
- computer networks and communications
- information systems
- software
language:
- iso: eng
month: '10'
oa: 1
oa_version: Published Version
page: 585-618
project:
- _id: B67AFEDC-15C9-11EA-A837-991A96BB2854
name: IST Austria Open Access Fund
publication: Acta Informatica
publication_identifier:
eissn:
- 1432-0525
issn:
- 0001-5903
publication_status: published
publisher: Springer Nature
quality_controlled: '1'
scopus_import: '1'
status: public
title: Index appearance record with preorders
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: 4359f0d1-fa6c-11eb-b949-802e58b17ae8
volume: 59
year: '2022'
...
---
_id: '12128'
abstract:
- lang: eng
text: We introduce a machine-learning (ML) framework for high-throughput benchmarking
of diverse representations of chemical systems against datasets of materials and
molecules. The guiding principle underlying the benchmarking approach is to evaluate
raw descriptor performance by limiting model complexity to simple regression schemes
while enforcing best ML practices, allowing for unbiased hyperparameter optimization,
and assessing learning progress through learning curves along series of synchronized
train-test splits. The resulting models are intended as baselines that can inform
future method development, in addition to indicating how easily a given dataset
can be learnt. Through a comparative analysis of the training outcome across a
diverse set of physicochemical, topological and geometric representations, we
glean insight into the relative merits of these representations as well as their
interrelatedness.
acknowledgement: 'C P acknowledges funding from Astex through the Sustaining Innovation
Program under the Milner Consortium. B C acknowledges resources provided by the
Cambridge Tier-2 system operated by the University of Cambridge Research Computing
Service funded by EPSRC Tier-2 capital Grant EP/P020259/1. F A F acknowledges funding
from the Swiss National Science Foundation (Grant No. P2BSP2_191736). '
article_number: '040501'
article_processing_charge: No
article_type: original
author:
- first_name: Carl
full_name: Poelking, Carl
last_name: Poelking
- first_name: Felix A
full_name: Faber, Felix A
last_name: Faber
- first_name: Bingqing
full_name: Cheng, Bingqing
id: cbe3cda4-d82c-11eb-8dc7-8ff94289fcc9
last_name: Cheng
orcid: 0000-0002-3584-9632
citation:
ama: 'Poelking C, Faber FA, Cheng B. BenchML: An extensible pipelining framework
for benchmarking representations of materials and molecules at scale. Machine
Learning: Science and Technology. 2022;3(4). doi:10.1088/2632-2153/ac4d11'
apa: 'Poelking, C., Faber, F. A., & Cheng, B. (2022). BenchML: An extensible
pipelining framework for benchmarking representations of materials and molecules
at scale. Machine Learning: Science and Technology. IOP Publishing. https://doi.org/10.1088/2632-2153/ac4d11'
chicago: 'Poelking, Carl, Felix A Faber, and Bingqing Cheng. “BenchML: An Extensible
Pipelining Framework for Benchmarking Representations of Materials and Molecules
at Scale.” Machine Learning: Science and Technology. IOP Publishing, 2022.
https://doi.org/10.1088/2632-2153/ac4d11.'
ieee: 'C. Poelking, F. A. Faber, and B. Cheng, “BenchML: An extensible pipelining
framework for benchmarking representations of materials and molecules at scale,”
Machine Learning: Science and Technology, vol. 3, no. 4. IOP Publishing,
2022.'
ista: 'Poelking C, Faber FA, Cheng B. 2022. BenchML: An extensible pipelining framework
for benchmarking representations of materials and molecules at scale. Machine
Learning: Science and Technology. 3(4), 040501.'
mla: 'Poelking, Carl, et al. “BenchML: An Extensible Pipelining Framework for Benchmarking
Representations of Materials and Molecules at Scale.” Machine Learning: Science
and Technology, vol. 3, no. 4, 040501, IOP Publishing, 2022, doi:10.1088/2632-2153/ac4d11.'
short: 'C. Poelking, F.A. Faber, B. Cheng, Machine Learning: Science and Technology
3 (2022).'
date_created: 2023-01-12T12:02:21Z
date_published: 2022-11-17T00:00:00Z
date_updated: 2023-08-04T08:49:53Z
day: '17'
ddc:
- '000'
department:
- _id: BiCh
doi: 10.1088/2632-2153/ac4d11
external_id:
isi:
- '000886534000001'
file:
- access_level: open_access
checksum: 8930d4ad6ed9b47358c6f1a68666adb6
content_type: application/pdf
creator: dernst
date_created: 2023-01-23T10:42:04Z
date_updated: 2023-01-23T10:42:04Z
file_id: '12343'
file_name: 2022_MachLearning_Poelking.pdf
file_size: 13814559
relation: main_file
success: 1
file_date_updated: 2023-01-23T10:42:04Z
has_accepted_license: '1'
intvolume: ' 3'
isi: 1
issue: '4'
keyword:
- Artificial Intelligence
- Human-Computer Interaction
- Software
language:
- iso: eng
month: '11'
oa: 1
oa_version: Published Version
publication: 'Machine Learning: Science and Technology'
publication_identifier:
issn:
- 2632-2153
publication_status: published
publisher: IOP Publishing
quality_controlled: '1'
related_material:
link:
- relation: software
url: https://github.com/capoe/benchml
scopus_import: '1'
status: public
title: 'BenchML: An extensible pipelining framework for benchmarking representations
of materials and molecules at scale'
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: 4359f0d1-fa6c-11eb-b949-802e58b17ae8
volume: 3
year: '2022'
...
---
_id: '12147'
abstract:
- lang: eng
text: Continuous-time neural networks are a class of machine learning systems that
can tackle representation learning on spatiotemporal decision-making tasks. These
models are typically represented by continuous differential equations. However,
their expressive power when they are deployed on computers is bottlenecked by
numerical differential equation solvers. This limitation has notably slowed down
the scaling and understanding of numerous natural physical phenomena such as the
dynamics of nervous systems. Ideally, we would circumvent this bottleneck by solving
the given dynamical system in closed form. This is known to be intractable in
general. Here, we show that it is possible to closely approximate the interaction
between neurons and synapses—the building blocks of natural and artificial neural
networks—constructed by liquid time-constant networks efficiently in closed form.
To this end, we compute a tightly bounded approximation of the solution of an
integral appearing in liquid time-constant dynamics that has had no known closed-form
solution so far. This closed-form solution impacts the design of continuous-time
and continuous-depth neural models. For instance, since time appears explicitly
in closed form, the formulation relaxes the need for complex numerical solvers.
Consequently, we obtain models that are between one and five orders of magnitude
faster in training and inference compared with differential equation-based counterparts.
More importantly, in contrast to ordinary differential equation-based continuous
networks, closed-form networks can scale remarkably well compared with other deep
learning instances. Lastly, as these models are derived from liquid networks,
they show good performance in time-series modelling compared with advanced recurrent
neural network models.
acknowledgement: This research was supported in part by the AI2050 program at Schmidt
Futures (grant G-22-63172), the Boeing Company, and the United States Air Force
Research Laboratory and the United States Air Force Artificial Intelligence Accelerator
and was accomplished under cooperative agreement number FA8750-19-2-1000. The views
and conclusions contained in this document are those of the authors and should not
be interpreted as representing the official policies, either expressed or implied,
of the United States Air Force or the U.S. Government. The U.S. Government is authorized
to reproduce and distribute reprints for Government purposes, notwithstanding any
copyright notation herein. This work was further supported by The Boeing Company
and Office of Naval Research grant N00014-18-1-2830. M.T. is supported by the Poul
Due Jensen Foundation, grant 883901. M.L. was supported in part by the Austrian
Science Fund under grant Z211-N23 (Wittgenstein Award). A.A. was supported by the
National Science Foundation Graduate Research Fellowship Program. We thank T.-H.
Wang, P. Kao, M. Chahine, W. Xiao, X. Li, L. Yin and Y. Ben for useful suggestions
and for testing of CfC models to confirm the results across other domains.
article_processing_charge: No
article_type: original
arxiv: 1
author:
- first_name: Ramin
full_name: Hasani, Ramin
last_name: Hasani
- first_name: Mathias
full_name: Lechner, Mathias
id: 3DC22916-F248-11E8-B48F-1D18A9856A87
last_name: Lechner
- first_name: Alexander
full_name: Amini, Alexander
last_name: Amini
- first_name: Lucas
full_name: Liebenwein, Lucas
last_name: Liebenwein
- first_name: Aaron
full_name: Ray, Aaron
last_name: Ray
- first_name: Max
full_name: Tschaikowski, Max
last_name: Tschaikowski
- first_name: Gerald
full_name: Teschl, Gerald
last_name: Teschl
- first_name: Daniela
full_name: Rus, Daniela
last_name: Rus
citation:
ama: Hasani R, Lechner M, Amini A, et al. Closed-form continuous-time neural networks.
Nature Machine Intelligence. 2022;4(11):992-1003. doi:10.1038/s42256-022-00556-7
apa: Hasani, R., Lechner, M., Amini, A., Liebenwein, L., Ray, A., Tschaikowski,
M., … Rus, D. (2022). Closed-form continuous-time neural networks. Nature Machine
Intelligence. Springer Nature. https://doi.org/10.1038/s42256-022-00556-7
chicago: Hasani, Ramin, Mathias Lechner, Alexander Amini, Lucas Liebenwein, Aaron
Ray, Max Tschaikowski, Gerald Teschl, and Daniela Rus. “Closed-Form Continuous-Time
Neural Networks.” Nature Machine Intelligence. Springer Nature, 2022. https://doi.org/10.1038/s42256-022-00556-7.
ieee: R. Hasani et al., “Closed-form continuous-time neural networks,” Nature
Machine Intelligence, vol. 4, no. 11. Springer Nature, pp. 992–1003, 2022.
ista: Hasani R, Lechner M, Amini A, Liebenwein L, Ray A, Tschaikowski M, Teschl
G, Rus D. 2022. Closed-form continuous-time neural networks. Nature Machine Intelligence.
4(11), 992–1003.
mla: Hasani, Ramin, et al. “Closed-Form Continuous-Time Neural Networks.” Nature
Machine Intelligence, vol. 4, no. 11, Springer Nature, 2022, pp. 992–1003,
doi:10.1038/s42256-022-00556-7.
short: R. Hasani, M. Lechner, A. Amini, L. Liebenwein, A. Ray, M. Tschaikowski,
G. Teschl, D. Rus, Nature Machine Intelligence 4 (2022) 992–1003.
date_created: 2023-01-12T12:07:21Z
date_published: 2022-11-15T00:00:00Z
date_updated: 2023-08-04T09:00:10Z
day: '15'
ddc:
- '000'
department:
- _id: ToHe
doi: 10.1038/s42256-022-00556-7
external_id:
arxiv:
- '2106.13898'
isi:
- '000884215600003'
file:
- access_level: open_access
checksum: b4789122ce04bfb4ac042390f59aaa8b
content_type: application/pdf
creator: dernst
date_created: 2023-01-24T09:49:44Z
date_updated: 2023-01-24T09:49:44Z
file_id: '12355'
file_name: 2022_NatureMachineIntelligence_Hasani.pdf
file_size: 3259553
relation: main_file
success: 1
file_date_updated: 2023-01-24T09:49:44Z
has_accepted_license: '1'
intvolume: ' 4'
isi: 1
issue: '11'
keyword:
- Artificial Intelligence
- Computer Networks and Communications
- Computer Vision and Pattern Recognition
- Human-Computer Interaction
- Software
language:
- iso: eng
month: '11'
oa: 1
oa_version: Published Version
page: 992-1003
project:
- _id: 25F42A32-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: Z211
name: The Wittgenstein Prize
publication: Nature Machine Intelligence
publication_identifier:
issn:
- 2522-5839
publication_status: published
publisher: Springer Nature
quality_controlled: '1'
related_material:
link:
- relation: erratum
url: https://doi.org/10.1038/s42256-022-00597-y
scopus_import: '1'
status: public
title: Closed-form continuous-time neural networks
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: 4359f0d1-fa6c-11eb-b949-802e58b17ae8
volume: 4
year: '2022'
...
---
_id: '9234'
abstract:
- lang: eng
text: In this paper, we present two new inertial projection-type methods for solving
multivalued variational inequality problems in finite-dimensional spaces. We establish
the convergence of the sequence generated by these methods when the multivalued
mapping associated with the problem is only required to be locally bounded without
any monotonicity assumption. Furthermore, the inertial techniques that we employ
in this paper are quite different from the ones used in most papers. Moreover,
based on the weaker assumptions on the inertial factor in our methods, we derive
several special cases of our methods. Finally, we present some experimental results
to illustrate the profits that we gain by introducing the inertial extrapolation
steps.
acknowledgement: 'The authors sincerely thank the Editor-in-Chief and anonymous referees
for their careful reading, constructive comments and fruitful suggestions that help
improve the manuscript. The research of the first author is supported by the National
Research Foundation (NRF) South Africa (S& F-DSI/NRF Free Standing Postdoctoral
Fellowship; Grant Number: 120784). The first author also acknowledges the financial
support from DSI/NRF, South Africa Center of Excellence in Mathematical and Statistical
Sciences (CoE-MaSS) Postdoctoral Fellowship. The second author has received funding
from the European Research Council (ERC) under the European Union’s Seventh Framework
Program (FP7 - 2007-2013) (Grant agreement No. 616160). Open Access funding provided
by Institute of Science and Technology (IST Austria).'
article_processing_charge: Yes (via OA deal)
article_type: original
author:
- first_name: Chinedu
full_name: Izuchukwu, Chinedu
last_name: Izuchukwu
- first_name: Yekini
full_name: Shehu, Yekini
id: 3FC7CB58-F248-11E8-B48F-1D18A9856A87
last_name: Shehu
orcid: 0000-0001-9224-7139
citation:
ama: Izuchukwu C, Shehu Y. New inertial projection methods for solving multivalued
variational inequality problems beyond monotonicity. Networks and Spatial Economics.
2021;21(2):291-323. doi:10.1007/s11067-021-09517-w
apa: Izuchukwu, C., & Shehu, Y. (2021). New inertial projection methods for
solving multivalued variational inequality problems beyond monotonicity. Networks
and Spatial Economics. Springer Nature. https://doi.org/10.1007/s11067-021-09517-w
chicago: Izuchukwu, Chinedu, and Yekini Shehu. “New Inertial Projection Methods
for Solving Multivalued Variational Inequality Problems beyond Monotonicity.”
Networks and Spatial Economics. Springer Nature, 2021. https://doi.org/10.1007/s11067-021-09517-w.
ieee: C. Izuchukwu and Y. Shehu, “New inertial projection methods for solving multivalued
variational inequality problems beyond monotonicity,” Networks and Spatial
Economics, vol. 21, no. 2. Springer Nature, pp. 291–323, 2021.
ista: Izuchukwu C, Shehu Y. 2021. New inertial projection methods for solving multivalued
variational inequality problems beyond monotonicity. Networks and Spatial Economics.
21(2), 291–323.
mla: Izuchukwu, Chinedu, and Yekini Shehu. “New Inertial Projection Methods for
Solving Multivalued Variational Inequality Problems beyond Monotonicity.” Networks
and Spatial Economics, vol. 21, no. 2, Springer Nature, 2021, pp. 291–323,
doi:10.1007/s11067-021-09517-w.
short: C. Izuchukwu, Y. Shehu, Networks and Spatial Economics 21 (2021) 291–323.
date_created: 2021-03-10T12:18:47Z
date_published: 2021-06-01T00:00:00Z
date_updated: 2023-09-05T15:32:32Z
day: '01'
ddc:
- '510'
department:
- _id: VlKo
doi: 10.1007/s11067-021-09517-w
ec_funded: 1
external_id:
isi:
- '000625002100001'
file:
- access_level: open_access
checksum: 22b4253a2e5da843622a2df713784b4c
content_type: application/pdf
creator: kschuh
date_created: 2021-08-11T12:44:16Z
date_updated: 2021-08-11T12:44:16Z
file_id: '9884'
file_name: 2021_NetworksSpatialEconomics_Shehu.pdf
file_size: 834964
relation: main_file
success: 1
file_date_updated: 2021-08-11T12:44:16Z
has_accepted_license: '1'
intvolume: ' 21'
isi: 1
issue: '2'
keyword:
- Computer Networks and Communications
- Software
- Artificial Intelligence
language:
- iso: eng
month: '06'
oa: 1
oa_version: Published Version
page: 291-323
project:
- _id: 25FBA906-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '616160'
name: 'Discrete Optimization in Computer Vision: Theory and Practice'
- _id: B67AFEDC-15C9-11EA-A837-991A96BB2854
name: IST Austria Open Access Fund
publication: Networks and Spatial Economics
publication_identifier:
eissn:
- 1572-9427
issn:
- 1566-113X
publication_status: published
publisher: Springer Nature
quality_controlled: '1'
scopus_import: '1'
status: public
title: New inertial projection methods for solving multivalued variational inequality
problems beyond monotonicity
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: c635000d-4b10-11ee-a964-aac5a93f6ac1
volume: 21
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: International Conference
on Runtime Verification. Vol 12974. Cham: Springer Nature; 2021:231-243. doi:10.1007/978-3-030-88494-9_12'
apa: 'Mühlböck, F., & Henzinger, T. A. (2021). Differential monitoring. In International
Conference on Runtime Verification (Vol. 12974, pp. 231–243). Cham: Springer
Nature. https://doi.org/10.1007/978-3-030-88494-9_12'
chicago: 'Mühlböck, Fabian, and Thomas A Henzinger. “Differential Monitoring.” In
International Conference on Runtime Verification, 12974:231–43. Cham: Springer
Nature, 2021. https://doi.org/10.1007/978-3-030-88494-9_12.'
ieee: F. Mühlböck and T. A. Henzinger, “Differential monitoring,” in International
Conference on Runtime Verification, 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.” International
Conference on Runtime Verification, vol. 12974, Springer Nature, 2021, pp.
231–43, doi:10.1007/978-3-030-88494-9_12.
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: '10191'
abstract:
- lang: eng
text: "In this work we solve the algorithmic problem of consistency verification
for the TSO and PSO memory models given a reads-from map, denoted VTSO-rf and
VPSO-rf, respectively. For an execution of n events over k threads and d variables,
we establish novel bounds that scale as nk+1 for TSO and as nk+1· min(nk2, 2k·
d) for PSO. Moreover, based on our solution to these problems, we develop an SMC
algorithm under TSO and PSO that uses the RF equivalence. The algorithm is exploration-optimal,
in the sense that it is guaranteed to explore each class of the RF partitioning
exactly once, and spends polynomial time per class when k is bounded. Finally,
we implement all our algorithms in the SMC tool Nidhugg, and perform a large number
of experiments over benchmarks from existing literature. Our experimental results
show that our algorithms for VTSO-rf and VPSO-rf provide significant scalability
improvements over standard alternatives. Moreover, when used for SMC, the RF partitioning
is often much coarser than the standard Shasha-Snir partitioning for TSO/PSO,
which yields a significant speedup in the model checking task.\r\n\r\n"
acknowledgement: "The research was partially funded by the ERC CoG 863818 (ForM-SMArt)
and the Vienna Science\r\nand Technology Fund (WWTF) through project ICT15-003."
article_number: '164'
article_processing_charge: No
article_type: original
arxiv: 1
author:
- first_name: Truc Lam
full_name: Bui, Truc Lam
last_name: Bui
- first_name: Krishnendu
full_name: Chatterjee, Krishnendu
id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
last_name: Chatterjee
orcid: 0000-0002-4561-241X
- first_name: Tushar
full_name: Gautam, Tushar
last_name: Gautam
- first_name: Andreas
full_name: Pavlogiannis, Andreas
id: 49704004-F248-11E8-B48F-1D18A9856A87
last_name: Pavlogiannis
orcid: 0000-0002-8943-0722
- first_name: Viktor
full_name: Toman, Viktor
id: 3AF3DA7C-F248-11E8-B48F-1D18A9856A87
last_name: Toman
orcid: 0000-0001-9036-063X
citation:
ama: Bui TL, Chatterjee K, Gautam T, Pavlogiannis A, Toman V. The reads-from equivalence
for the TSO and PSO memory models. Proceedings of the ACM on Programming Languages.
2021;5(OOPSLA). doi:10.1145/3485541
apa: Bui, T. L., Chatterjee, K., Gautam, T., Pavlogiannis, A., & Toman, V. (2021).
The reads-from equivalence for the TSO and PSO memory models. Proceedings of
the ACM on Programming Languages. Association for Computing Machinery. https://doi.org/10.1145/3485541
chicago: Bui, Truc Lam, Krishnendu Chatterjee, Tushar Gautam, Andreas Pavlogiannis,
and Viktor Toman. “The Reads-from Equivalence for the TSO and PSO Memory Models.”
Proceedings of the ACM on Programming Languages. Association for Computing
Machinery, 2021. https://doi.org/10.1145/3485541.
ieee: T. L. Bui, K. Chatterjee, T. Gautam, A. Pavlogiannis, and V. Toman, “The reads-from
equivalence for the TSO and PSO memory models,” Proceedings of the ACM on Programming
Languages, vol. 5, no. OOPSLA. Association for Computing Machinery, 2021.
ista: Bui TL, Chatterjee K, Gautam T, Pavlogiannis A, Toman V. 2021. The reads-from
equivalence for the TSO and PSO memory models. Proceedings of the ACM on Programming
Languages. 5(OOPSLA), 164.
mla: Bui, Truc Lam, et al. “The Reads-from Equivalence for the TSO and PSO Memory
Models.” Proceedings of the ACM on Programming Languages, vol. 5, no. OOPSLA,
164, Association for Computing Machinery, 2021, doi:10.1145/3485541.
short: T.L. Bui, K. Chatterjee, T. Gautam, A. Pavlogiannis, V. Toman, Proceedings
of the ACM on Programming Languages 5 (2021).
date_created: 2021-10-27T15:05:34Z
date_published: 2021-10-15T00:00:00Z
date_updated: 2025-07-14T09:10:16Z
day: '15'
ddc:
- '000'
department:
- _id: GradSch
- _id: KrCh
doi: 10.1145/3485541
ec_funded: 1
external_id:
arxiv:
- '2011.11763'
file:
- access_level: open_access
checksum: 9d6dce7b611853c529bb7b1915ac579e
content_type: application/pdf
creator: cchlebak
date_created: 2021-11-04T07:24:48Z
date_updated: 2021-11-04T07:24:48Z
file_id: '10215'
file_name: 2021_ProcACMPL_Bui.pdf
file_size: 2903485
relation: main_file
success: 1
file_date_updated: 2021-11-04T07:24:48Z
has_accepted_license: '1'
intvolume: ' 5'
issue: OOPSLA
keyword:
- safety
- risk
- reliability and quality
- software
language:
- iso: eng
month: '10'
oa: 1
oa_version: Published Version
project:
- _id: 0599E47C-7A3F-11EA-A408-12923DDC885E
call_identifier: H2020
grant_number: '863818'
name: 'Formal Methods for Stochastic Models: Algorithms and Applications'
- _id: 25892FC0-B435-11E9-9278-68D0E5697425
grant_number: ICT15-003
name: Efficient Algorithms for Computer Aided Verification
publication: Proceedings of the ACM on Programming Languages
publication_identifier:
eissn:
- 2475-1421
publication_status: published
publisher: Association for Computing Machinery
quality_controlled: '1'
related_material:
record:
- id: '10199'
relation: dissertation_contains
status: public
scopus_import: '1'
status: public
title: The reads-from equivalence for the TSO and PSO memory models
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: 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. Differential Monitoring. IST Austria; 2021.
doi:10.15479/AT:ISTA:9946
apa: Mühlböck, F., & Henzinger, T. A. (2021). Differential monitoring.
IST Austria. https://doi.org/10.15479/AT:ISTA:9946
chicago: Mühlböck, Fabian, and Thomas A Henzinger. Differential Monitoring.
IST Austria, 2021. https://doi.org/10.15479/AT:ISTA:9946.
ieee: F. Mühlböck and T. A. Henzinger, Differential monitoring. 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. Differential Monitoring.
IST Austria, 2021, doi:10.15479/AT:ISTA:9946.
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'
...
---
_id: '10861'
abstract:
- lang: eng
text: We introduce in this paper AMT2.0, a tool for qualitative and quantitative
analysis of hybrid continuous and Boolean signals that combine numerical values
and discrete events. The evaluation of the signals is based on rich temporal specifications
expressed in extended signal temporal logic, which integrates timed regular expressions
within signal temporal logic. The tool features qualitative monitoring (property
satisfaction checking), trace diagnostics for explaining and justifying property
violations and specification-driven measurement of quantitative features of the
signal. We demonstrate the tool functionality on several running examples and
case studies, and evaluate its performance.
article_processing_charge: No
article_type: original
author:
- first_name: Dejan
full_name: Nickovic, Dejan
id: 41BCEE5C-F248-11E8-B48F-1D18A9856A87
last_name: Nickovic
- first_name: Olivier
full_name: Lebeltel, Olivier
last_name: Lebeltel
- first_name: Oded
full_name: Maler, Oded
last_name: Maler
- first_name: Thomas
full_name: Ferrere, Thomas
id: 40960E6E-F248-11E8-B48F-1D18A9856A87
last_name: Ferrere
orcid: 0000-0001-5199-3143
- first_name: Dogan
full_name: Ulus, Dogan
last_name: Ulus
citation:
ama: 'Nickovic D, Lebeltel O, Maler O, Ferrere T, Ulus D. AMT 2.0: Qualitative and
quantitative trace analysis with extended signal temporal logic. International
Journal on Software Tools for Technology Transfer. 2020;22(6):741-758. doi:10.1007/s10009-020-00582-z'
apa: 'Nickovic, D., Lebeltel, O., Maler, O., Ferrere, T., & Ulus, D. (2020).
AMT 2.0: Qualitative and quantitative trace analysis with extended signal temporal
logic. International Journal on Software Tools for Technology Transfer.
Springer Nature. https://doi.org/10.1007/s10009-020-00582-z'
chicago: 'Nickovic, Dejan, Olivier Lebeltel, Oded Maler, Thomas Ferrere, and Dogan
Ulus. “AMT 2.0: Qualitative and Quantitative Trace Analysis with Extended Signal
Temporal Logic.” International Journal on Software Tools for Technology Transfer.
Springer Nature, 2020. https://doi.org/10.1007/s10009-020-00582-z.'
ieee: 'D. Nickovic, O. Lebeltel, O. Maler, T. Ferrere, and D. Ulus, “AMT 2.0: Qualitative
and quantitative trace analysis with extended signal temporal logic,” International
Journal on Software Tools for Technology Transfer, vol. 22, no. 6. Springer
Nature, pp. 741–758, 2020.'
ista: 'Nickovic D, Lebeltel O, Maler O, Ferrere T, Ulus D. 2020. AMT 2.0: Qualitative
and quantitative trace analysis with extended signal temporal logic. International
Journal on Software Tools for Technology Transfer. 22(6), 741–758.'
mla: 'Nickovic, Dejan, et al. “AMT 2.0: Qualitative and Quantitative Trace Analysis
with Extended Signal Temporal Logic.” International Journal on Software Tools
for Technology Transfer, vol. 22, no. 6, Springer Nature, 2020, pp. 741–58,
doi:10.1007/s10009-020-00582-z.'
short: D. Nickovic, O. Lebeltel, O. Maler, T. Ferrere, D. Ulus, International Journal
on Software Tools for Technology Transfer 22 (2020) 741–758.
date_created: 2022-03-18T10:10:53Z
date_published: 2020-08-03T00:00:00Z
date_updated: 2023-09-08T11:52:02Z
day: '03'
department:
- _id: ToHe
doi: 10.1007/s10009-020-00582-z
external_id:
isi:
- '000555398600001'
intvolume: ' 22'
isi: 1
issue: '6'
keyword:
- Information Systems
- Software
language:
- iso: eng
month: '08'
oa_version: None
page: 741-758
publication: International Journal on Software Tools for Technology Transfer
publication_identifier:
eissn:
- 1433-2787
issn:
- 1433-2779
publication_status: published
publisher: Springer Nature
quality_controlled: '1'
related_material:
record:
- id: '299'
relation: earlier_version
status: public
scopus_import: '1'
status: public
title: 'AMT 2.0: Qualitative and quantitative trace analysis with extended signal
temporal logic'
type: journal_article
user_id: c635000d-4b10-11ee-a964-aac5a93f6ac1
volume: 22
year: '2020'
...
---
_id: '10190'
abstract:
- lang: eng
text: 'The verification of concurrent programs remains an open challenge, as thread
interaction has to be accounted for, which leads to state-space explosion. Stateless
model checking battles this problem by exploring traces rather than states of
the program. As there are exponentially many traces, dynamic partial-order reduction
(DPOR) techniques are used to partition the trace space into equivalence classes,
and explore a few representatives from each class. The standard equivalence that
underlies most DPOR techniques is the happens-before equivalence, however recent
works have spawned a vivid interest towards coarser equivalences. The efficiency
of such approaches is a product of two parameters: (i) the size of the partitioning
induced by the equivalence, and (ii) the time spent by the exploration algorithm
in each class of the partitioning. In this work, we present a new equivalence,
called value-happens-before and show that it has two appealing features. First,
value-happens-before is always at least as coarse as the happens-before equivalence,
and can be even exponentially coarser. Second, the value-happens-before partitioning
is efficiently explorable when the number of threads is bounded. We present an
algorithm called value-centric DPOR (VCDPOR), which explores the underlying partitioning
using polynomial time per class. Finally, we perform an experimental evaluation
of VCDPOR on various benchmarks, and compare it against other state-of-the-art
approaches. Our results show that value-happens-before typically induces a significant
reduction in the size of the underlying partitioning, which leads to a considerable
reduction in the running time for exploring the whole partitioning.'
acknowledgement: "The authors would also like to thank anonymous referees for their
valuable comments and helpful suggestions. This work is supported by the Austrian
Science Fund (FWF) NFN grants S11407-N23 (RiSE/SHiNE) and S11402-N23 (RiSE/SHiNE),
by the Vienna Science and Technology Fund (WWTF) Project ICT15-003, and by the Austrian
Science Fund (FWF) Schrodinger grant J-4220.\r\n"
article_number: '124'
article_processing_charge: No
arxiv: 1
author:
- first_name: Krishnendu
full_name: Chatterjee, Krishnendu
id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
last_name: Chatterjee
orcid: 0000-0002-4561-241X
- first_name: Andreas
full_name: Pavlogiannis, Andreas
id: 49704004-F248-11E8-B48F-1D18A9856A87
last_name: Pavlogiannis
orcid: 0000-0002-8943-0722
- first_name: Viktor
full_name: Toman, Viktor
id: 3AF3DA7C-F248-11E8-B48F-1D18A9856A87
last_name: Toman
orcid: 0000-0001-9036-063X
citation:
ama: 'Chatterjee K, Pavlogiannis A, Toman V. Value-centric dynamic partial order
reduction. In: Proceedings of the 34th ACM International Conference on Object-Oriented
Programming, Systems, Languages, and Applications. Vol 3. ACM; 2019. doi:10.1145/3360550'
apa: 'Chatterjee, K., Pavlogiannis, A., & Toman, V. (2019). Value-centric dynamic
partial order reduction. In Proceedings of the 34th ACM International Conference
on Object-Oriented Programming, Systems, Languages, and Applications (Vol.
3). Athens, Greece: ACM. https://doi.org/10.1145/3360550'
chicago: Chatterjee, Krishnendu, Andreas Pavlogiannis, and Viktor Toman. “Value-Centric
Dynamic Partial Order Reduction.” In Proceedings of the 34th ACM International
Conference on Object-Oriented Programming, Systems, Languages, and Applications,
Vol. 3. ACM, 2019. https://doi.org/10.1145/3360550.
ieee: K. Chatterjee, A. Pavlogiannis, and V. Toman, “Value-centric dynamic partial
order reduction,” in Proceedings of the 34th ACM International Conference on
Object-Oriented Programming, Systems, Languages, and Applications, Athens,
Greece, 2019, vol. 3.
ista: 'Chatterjee K, Pavlogiannis A, Toman V. 2019. Value-centric dynamic partial
order reduction. Proceedings of the 34th ACM International Conference on Object-Oriented
Programming, Systems, Languages, and Applications. OOPSLA: Object-oriented Programming,
Systems, Languages and Applications vol. 3, 124.'
mla: Chatterjee, Krishnendu, et al. “Value-Centric Dynamic Partial Order Reduction.”
Proceedings of the 34th ACM International Conference on Object-Oriented Programming,
Systems, Languages, and Applications, vol. 3, 124, ACM, 2019, doi:10.1145/3360550.
short: K. Chatterjee, A. Pavlogiannis, V. Toman, in:, Proceedings of the 34th ACM
International Conference on Object-Oriented Programming, Systems, Languages, and
Applications, ACM, 2019.
conference:
end_date: 2019-10-25
location: Athens, Greece
name: 'OOPSLA: Object-oriented Programming, Systems, Languages and Applications'
start_date: 2019-10-23
date_created: 2021-10-27T14:57:06Z
date_published: 2019-10-10T00:00:00Z
date_updated: 2025-07-14T09:10:15Z
day: '10'
ddc:
- '000'
department:
- _id: GradSch
- _id: KrCh
doi: 10.1145/3360550
external_id:
arxiv:
- '1909.00989'
file:
- access_level: open_access
checksum: 2149979c46964c4d117af06ccb6c0834
content_type: application/pdf
creator: cchlebak
date_created: 2021-11-12T11:41:56Z
date_updated: 2021-11-12T11:41:56Z
file_id: '10278'
file_name: 2019_ACM_Chatterjee.pdf
file_size: 570829
relation: main_file
success: 1
file_date_updated: 2021-11-12T11:41:56Z
has_accepted_license: '1'
intvolume: ' 3'
keyword:
- safety
- risk
- reliability and quality
- software
language:
- iso: eng
main_file_link:
- open_access: '1'
url: https://dl.acm.org/doi/10.1145/3360550
month: '10'
oa: 1
oa_version: Published Version
project:
- _id: 25892FC0-B435-11E9-9278-68D0E5697425
grant_number: ICT15-003
name: Efficient Algorithms for Computer Aided Verification
- _id: 25863FF4-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: S11407
name: Game Theory
- _id: 25832EC2-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: S 11407_N23
name: Rigorous Systems Engineering
- _id: 25F5A88A-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: S11402-N23
name: Moderne Concurrency Paradigms
publication: Proceedings of the 34th ACM International Conference on Object-Oriented
Programming, Systems, Languages, and Applications
publication_identifier:
eissn:
- 2475-1421
publication_status: published
publisher: ACM
quality_controlled: '1'
related_material:
record:
- id: '10199'
relation: dissertation_contains
status: public
status: public
title: Value-centric dynamic partial order reduction
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: 8b945eb4-e2f2-11eb-945a-df72226e66a9
volume: 3
year: '2019'
...
---
_id: '10396'
abstract:
- lang: eng
text: Stimfit is a free cross-platform software package for viewing and analyzing
electrophysiological data. It supports most standard file types for cellular neurophysiology
and other biomedical formats. Its analysis algorithms have been used and validated
in several experimental laboratories. Its embedded Python scripting interface
makes Stimfit highly extensible and customizable.
article_number: '000010151520134181'
article_processing_charge: No
article_type: original
author:
- first_name: Alois
full_name: Schlögl, Alois
id: 45BF87EE-F248-11E8-B48F-1D18A9856A87
last_name: Schlögl
orcid: 0000-0002-5621-8100
- first_name: Peter M
full_name: Jonas, Peter M
id: 353C1B58-F248-11E8-B48F-1D18A9856A87
last_name: Jonas
orcid: 0000-0001-5001-4804
- first_name: C.
full_name: Schmidt-Hieber, C.
last_name: Schmidt-Hieber
- first_name: S. J.
full_name: Guzman, S. J.
last_name: Guzman
citation:
ama: 'Schlögl A, Jonas PM, Schmidt-Hieber C, Guzman SJ. Stimfit: A fast visualization
and analysis environment for cellular neurophysiology. Biomedical Engineering
/ Biomedizinische Technik. 2013;58(SI-1-Track-G). doi:10.1515/bmt-2013-4181'
apa: 'Schlögl, A., Jonas, P. M., Schmidt-Hieber, C., & Guzman, S. J. (2013).
Stimfit: A fast visualization and analysis environment for cellular neurophysiology.
Biomedical Engineering / Biomedizinische Technik. Graz, Austria: De Gruyter.
https://doi.org/10.1515/bmt-2013-4181'
chicago: 'Schlögl, Alois, Peter M Jonas, C. Schmidt-Hieber, and S. J. Guzman. “Stimfit:
A Fast Visualization and Analysis Environment for Cellular Neurophysiology.” Biomedical
Engineering / Biomedizinische Technik. De Gruyter, 2013. https://doi.org/10.1515/bmt-2013-4181.'
ieee: 'A. Schlögl, P. M. Jonas, C. Schmidt-Hieber, and S. J. Guzman, “Stimfit: A
fast visualization and analysis environment for cellular neurophysiology,” Biomedical
Engineering / Biomedizinische Technik, vol. 58, no. SI-1-Track-G. De Gruyter,
2013.'
ista: 'Schlögl A, Jonas PM, Schmidt-Hieber C, Guzman SJ. 2013. Stimfit: A fast visualization
and analysis environment for cellular neurophysiology. Biomedical Engineering
/ Biomedizinische Technik. 58(SI-1-Track-G), 000010151520134181.'
mla: 'Schlögl, Alois, et al. “Stimfit: A Fast Visualization and Analysis Environment
for Cellular Neurophysiology.” Biomedical Engineering / Biomedizinische Technik,
vol. 58, no. SI-1-Track-G, 000010151520134181, De Gruyter, 2013, doi:10.1515/bmt-2013-4181.'
short: A. Schlögl, P.M. Jonas, C. Schmidt-Hieber, S.J. Guzman, Biomedical Engineering
/ Biomedizinische Technik 58 (2013).
conference:
end_date: 2013-09-21
location: Graz, Austria
name: 'BMT: Biomedizinische Technik '
start_date: 2013-09-19
date_created: 2021-12-01T14:35:35Z
date_published: 2013-08-01T00:00:00Z
date_updated: 2021-12-02T12:51:12Z
day: '01'
ddc:
- '005'
- '610'
department:
- _id: PeJo
doi: 10.1515/bmt-2013-4181
external_id:
pmid:
- '24042795'
file:
- access_level: open_access
checksum: cdfc5339b530a25d6079f7223f0b1f16
content_type: application/pdf
creator: schloegl
date_created: 2021-12-01T14:38:08Z
date_updated: 2021-12-01T14:38:08Z
file_id: '10397'
file_name: Schloegl_Abstract-BMT2013.pdf
file_size: 149825
relation: main_file
success: 1
file_date_updated: 2021-12-01T14:38:08Z
has_accepted_license: '1'
intvolume: ' 58'
issue: SI-1-Track-G
keyword:
- biomedical engineering
- data analysis
- free software
language:
- iso: eng
month: '08'
oa: 1
oa_version: Submitted Version
pmid: 1
publication: Biomedical Engineering / Biomedizinische Technik
publication_identifier:
eissn:
- 1862-278X
issn:
- 0013-5585
publication_status: published
publisher: De Gruyter
quality_controlled: '1'
status: public
title: 'Stimfit: A fast visualization and analysis environment for cellular neurophysiology'
type: journal_article
user_id: 8b945eb4-e2f2-11eb-945a-df72226e66a9
volume: 58
year: '2013'
...