---
_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: '8067'
abstract:
- lang: eng
text: "With the lithium-ion technology approaching its intrinsic limit with graphite-based
anodes, lithium metal is recently receiving renewed interest from the battery
community as potential high capacity anode for next-generation rechargeable batteries.
In this focus paper, we review the main advances in this field since the first
attempts in the\r\nmid-1970s. Strategies for enabling reversible cycling and avoiding
dendrite growth are thoroughly discussed, including specific applications in all-solid-state
(polymeric and inorganic), Lithium-sulphur and Li-O2 (air) batteries. A particular
attention is paid to review recent developments in regard of prototype manufacturing
and current state-ofthe-art of these battery technologies with respect to the
2030 targets of the EU Integrated Strategic Energy Technology Plan (SET-Plan)
Action 7."
alternative_title:
- IST Austria Technical Report
article_processing_charge: No
author:
- first_name: Alberto
full_name: Varzi, Alberto
last_name: Varzi
- first_name: Katharina
full_name: Thanner, Katharina
last_name: Thanner
- first_name: Roberto
full_name: Scipioni, Roberto
last_name: Scipioni
- first_name: Daniele
full_name: Di Lecce, Daniele
last_name: Di Lecce
- first_name: Jusef
full_name: Hassoun, Jusef
last_name: Hassoun
- first_name: Susanne
full_name: Dörfler, Susanne
last_name: Dörfler
- first_name: Holger
full_name: Altheus, Holger
last_name: Altheus
- first_name: Stefan
full_name: Kaskel, Stefan
last_name: Kaskel
- first_name: Christian
full_name: Prehal, Christian
last_name: Prehal
- first_name: Stefan Alexander
full_name: Freunberger, Stefan Alexander
id: A8CA28E6-CE23-11E9-AD2D-EC27E6697425
last_name: Freunberger
orcid: 0000-0003-2902-5319
citation:
ama: Varzi A, Thanner K, Scipioni R, et al. Current Status and Future Perspectives
of Lithium Metal Batteries. IST Austria doi:10.15479/AT:ISTA:8067
apa: Varzi, A., Thanner, K., Scipioni, R., Di Lecce, D., Hassoun, J., Dörfler, S.,
… Freunberger, S. A. (n.d.). Current status and future perspectives of Lithium
metal batteries. IST Austria. https://doi.org/10.15479/AT:ISTA:8067
chicago: Varzi, Alberto, Katharina Thanner, Roberto Scipioni, Daniele Di Lecce,
Jusef Hassoun, Susanne Dörfler, Holger Altheus, Stefan Kaskel, Christian Prehal,
and Stefan Alexander Freunberger. Current Status and Future Perspectives of
Lithium Metal Batteries. IST Austria, n.d. https://doi.org/10.15479/AT:ISTA:8067.
ieee: A. Varzi et al., Current status and future perspectives of Lithium
metal batteries. IST Austria.
ista: Varzi A, Thanner K, Scipioni R, Di Lecce D, Hassoun J, Dörfler S, Altheus
H, Kaskel S, Prehal C, Freunberger SA. Current status and future perspectives
of Lithium metal batteries, IST Austria, 63p.
mla: Varzi, Alberto, et al. Current Status and Future Perspectives of Lithium
Metal Batteries. IST Austria, doi:10.15479/AT:ISTA:8067.
short: A. Varzi, K. Thanner, R. Scipioni, D. Di Lecce, J. Hassoun, S. Dörfler, H.
Altheus, S. Kaskel, C. Prehal, S.A. Freunberger, Current Status and Future Perspectives
of Lithium Metal Batteries, IST Austria, n.d.
date_created: 2020-06-30T07:37:39Z
date_published: 2020-07-01T00:00:00Z
date_updated: 2023-08-22T09:20:36Z
day: '01'
ddc:
- '540'
department:
- _id: StFr
doi: 10.15479/AT:ISTA:8067
file:
- access_level: open_access
checksum: d183ca1465a1cbb4f8db27875cd156f7
content_type: application/pdf
creator: dernst
date_created: 2020-07-02T07:36:04Z
date_updated: 2020-07-14T12:48:08Z
file_id: '8076'
file_name: 20200612_JPS_review_Li_metal_submitted.pdf
file_size: 2612498
relation: main_file
file_date_updated: 2020-07-14T12:48:08Z
has_accepted_license: '1'
keyword:
- Battery
- Lithium metal
- Lithium-sulphur
- Lithium-air
- All-solid-state
language:
- iso: eng
month: '07'
oa: 1
oa_version: Published Version
page: '63'
publication_identifier:
issn:
- 2664-1690
publication_status: submitted
publisher: IST Austria
related_material:
record:
- id: '8361'
relation: later_version
status: public
status: public
title: Current status and future perspectives of Lithium metal batteries
type: technical_report
user_id: 8b945eb4-e2f2-11eb-945a-df72226e66a9
year: '2020'
...
---
_id: '5457'
abstract:
- lang: eng
text: "We consider the problem of expected cost analysis over nondeterministic probabilistic
programs, which aims at automated methods for analyzing the resource-usage of
such programs. Previous approaches for this problem could only handle nonnegative
bounded costs. However, in many scenarios, such as queuing networks or analysis
of cryptocurrency protocols, both positive and negative costs are necessary and
the costs are unbounded as well.\r\n\r\nIn this work, we present a sound and efficient
approach to obtain polynomial bounds on the expected accumulated cost of nondeterministic
probabilistic programs. Our approach can handle (a) general positive and negative
costs with bounded updates in variables; and (b) nonnegative costs with general
updates to variables. We show that several natural examples which could not be
handled by previous approaches are captured in our framework.\r\n\r\nMoreover,
our approach leads to an efficient polynomial-time algorithm, while no previous
approach for cost analysis of probabilistic programs could guarantee polynomial
runtime. Finally, we show the effectiveness of our approach by presenting experimental
results on a variety of programs, motivated by real-world applications, for which
we efficiently synthesize tight resource-usage bounds."
alternative_title:
- IST Austria Technical Report
author:
- first_name: '1'
full_name: Anonymous, 1
last_name: Anonymous
- first_name: '2'
full_name: Anonymous, 2
last_name: Anonymous
- first_name: '3'
full_name: Anonymous, 3
last_name: Anonymous
- first_name: '4'
full_name: Anonymous, 4
last_name: Anonymous
- first_name: '5'
full_name: Anonymous, 5
last_name: Anonymous
- first_name: '6'
full_name: Anonymous, 6
last_name: Anonymous
citation:
ama: Anonymous 1, Anonymous 2, Anonymous 3, Anonymous 4, Anonymous 5, Anonymous
6. Cost Analysis of Nondeterministic Probabilistic Programs. IST Austria;
2018.
apa: Anonymous, 1, Anonymous, 2, Anonymous, 3, Anonymous, 4, Anonymous, 5, &
Anonymous, 6. (2018). Cost analysis of nondeterministic probabilistic programs.
IST Austria.
chicago: Anonymous, 1, 2 Anonymous, 3 Anonymous, 4 Anonymous, 5 Anonymous, and 6
Anonymous. Cost Analysis of Nondeterministic Probabilistic Programs. IST
Austria, 2018.
ieee: 1 Anonymous, 2 Anonymous, 3 Anonymous, 4 Anonymous, 5 Anonymous, and 6 Anonymous,
Cost analysis of nondeterministic probabilistic programs. IST Austria,
2018.
ista: Anonymous 1, Anonymous 2, Anonymous 3, Anonymous 4, Anonymous 5, Anonymous
6. 2018. Cost analysis of nondeterministic probabilistic programs, IST Austria,
27p.
mla: Anonymous, 1, et al. Cost Analysis of Nondeterministic Probabilistic Programs.
IST Austria, 2018.
short: 1 Anonymous, 2 Anonymous, 3 Anonymous, 4 Anonymous, 5 Anonymous, 6 Anonymous,
Cost Analysis of Nondeterministic Probabilistic Programs, IST Austria, 2018.
date_created: 2018-12-12T11:39:26Z
date_published: 2018-11-11T00:00:00Z
date_updated: 2023-08-25T08:07:48Z
day: '11'
ddc:
- '000'
file:
- access_level: open_access
checksum: ba3adafd36fe200385ccda583063b9eb
content_type: application/pdf
creator: system
date_created: 2018-12-12T11:53:32Z
date_updated: 2020-07-14T12:47:00Z
file_id: '5493'
file_name: IST-2018-1066-v1+1_techreport.pdf
file_size: 4202966
relation: main_file
- access_level: closed
checksum: 6cf3a19164bb8e5048a9c8c84dfd9fa3
content_type: text/plain
creator: dernst
date_created: 2019-05-10T13:22:12Z
date_updated: 2020-07-14T12:47:00Z
file_id: '6402'
file_name: authors-names.txt
file_size: 322
relation: main_file
file_date_updated: 2020-07-14T12:47:00Z
has_accepted_license: '1'
language:
- iso: eng
month: '11'
oa: 1
oa_version: Published Version
page: '27'
publication_identifier:
issn:
- 2664-1690
publication_status: published
publisher: IST Austria
pubrep_id: '1066'
related_material:
record:
- id: '6175'
relation: later_version
status: public
scopus_import: 1
status: public
title: Cost analysis of nondeterministic probabilistic programs
type: technical_report
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
year: '2018'
...
---
_id: '5455'
abstract:
- lang: eng
text: 'A fundamental algorithmic problem at the heart of static analysis is Dyck
reachability. The input is a graphwhere the edges are labeled with different types
of opening and closing parentheses, and the reachabilityinformation is computed
via paths whose parentheses are properly matched. We present new results for Dyckreachability
problems with applications to alias analysis and data-dependence analysis. Our
main contributions,that include improved upper bounds as well as lower bounds
that establish optimality guarantees, are asfollows:First, we consider Dyck reachability
on bidirected graphs, which is the standard way of performing field-sensitive
points-to analysis. Given a bidirected graph withnnodes andmedges, we present:
(i) an algorithmwith worst-case running timeO(m+n·α(n)), whereα(n)is the inverse
Ackermann function, improving thepreviously knownO(n2)time bound; (ii) a matching
lower bound that shows that our algorithm is optimalwrt to worst-case complexity;
and (iii) an optimal average-case upper bound ofO(m)time, improving thepreviously
knownO(m·logn)bound.Second, we consider the problem of context-sensitive data-dependence
analysis, where the task is to obtainanalysis summaries of library code in the
presence of callbacks. Our algorithm preprocesses libraries in almostlinear time,
after which the contribution of the library in the complexity of the client analysis
is only linear,and only wrt the number of call sites.Third, we prove that combinatorial
algorithms for Dyck reachability on general graphs with truly sub-cubic bounds
cannot be obtained without obtaining sub-cubic combinatorial algorithms for Boolean
MatrixMultiplication, which is a long-standing open problem. Thus we establish
that the existing combinatorialalgorithms for Dyck reachability are (conditionally)
optimal for general graphs. We also show that the samehardness holds for graphs
of constant treewidth.Finally, we provide a prototype implementation of our algorithms
for both alias analysis and data-dependenceanalysis. Our experimental evaluation
demonstrates that the new algorithms significantly outperform allexisting methods
on the two problems, over real-world benchmarks.'
alternative_title:
- IST Austria Technical Report
article_processing_charge: No
author:
- first_name: Krishnendu
full_name: Chatterjee, Krishnendu
id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
last_name: Chatterjee
orcid: 0000-0002-4561-241X
- first_name: Bhavya
full_name: Choudhary, Bhavya
last_name: Choudhary
- first_name: Andreas
full_name: Pavlogiannis, Andreas
id: 49704004-F248-11E8-B48F-1D18A9856A87
last_name: Pavlogiannis
orcid: 0000-0002-8943-0722
citation:
ama: Chatterjee K, Choudhary B, Pavlogiannis A. Optimal Dyck Reachability for
Data-Dependence and Alias Analysis. IST Austria; 2017. doi:10.15479/AT:IST-2017-870-v1-1
apa: Chatterjee, K., Choudhary, B., & Pavlogiannis, A. (2017). Optimal Dyck
reachability for data-dependence and alias analysis. IST Austria. https://doi.org/10.15479/AT:IST-2017-870-v1-1
chicago: Chatterjee, Krishnendu, Bhavya Choudhary, and Andreas Pavlogiannis. Optimal
Dyck Reachability for Data-Dependence and Alias Analysis. IST Austria, 2017.
https://doi.org/10.15479/AT:IST-2017-870-v1-1.
ieee: K. Chatterjee, B. Choudhary, and A. Pavlogiannis, Optimal Dyck reachability
for data-dependence and alias analysis. IST Austria, 2017.
ista: Chatterjee K, Choudhary B, Pavlogiannis A. 2017. Optimal Dyck reachability
for data-dependence and alias analysis, IST Austria, 37p.
mla: Chatterjee, Krishnendu, et al. Optimal Dyck Reachability for Data-Dependence
and Alias Analysis. IST Austria, 2017, doi:10.15479/AT:IST-2017-870-v1-1.
short: K. Chatterjee, B. Choudhary, A. Pavlogiannis, Optimal Dyck Reachability for
Data-Dependence and Alias Analysis, IST Austria, 2017.
date_created: 2018-12-12T11:39:26Z
date_published: 2017-10-23T00:00:00Z
date_updated: 2023-02-21T15:54:10Z
day: '23'
ddc:
- '000'
department:
- _id: KrCh
doi: 10.15479/AT:IST-2017-870-v1-1
file:
- access_level: open_access
checksum: 177a84a46e3ac17e87b31534ad16a4c9
content_type: application/pdf
creator: system
date_created: 2018-12-12T11:54:02Z
date_updated: 2020-07-14T12:46:59Z
file_id: '5524'
file_name: IST-2017-870-v1+1_main.pdf
file_size: 960491
relation: main_file
file_date_updated: 2020-07-14T12:46:59Z
has_accepted_license: '1'
language:
- iso: eng
month: '10'
oa: 1
oa_version: Published Version
page: '37'
publication_identifier:
issn:
- 2664-1690
publication_status: published
publisher: IST Austria
pubrep_id: '870'
related_material:
record:
- id: '10416'
relation: later_version
status: public
status: public
title: Optimal Dyck reachability for data-dependence and alias analysis
type: technical_report
user_id: 8b945eb4-e2f2-11eb-945a-df72226e66a9
year: '2017'
...
---
_id: '5456'
abstract:
- lang: eng
text: "We present a new dynamic partial-order reduction method for stateless model
checking of concurrent programs. A common approach for exploring program behaviors
relies on enumerating the traces of the program, without storing the visited states
(aka stateless exploration). As the number of distinct traces grows exponentially,
dynamic partial-order reduction (DPOR) techniques have been successfully used
to partition the space of traces into equivalence classes (Mazurkiewicz partitioning),
with the goal of exploring only few representative traces from each class.\r\nWe
introduce a new equivalence on traces under sequential consistency semantics,
which we call the observation equivalence. Two traces are observationally equivalent
if every read event observes the same write event in both traces. While the traditional
Mazurkiewicz equivalence is control-centric, our new definition is data-centric.
We show that our observation equivalence is coarser than the Mazurkiewicz equivalence,
and in many cases even exponentially coarser. We devise a DPOR exploration of
the trace space, called data-centric DPOR, based on the observation equivalence.\r\n1.
For acyclic architectures, our algorithm is guaranteed to explore exactly one
representative trace from each observation class, while spending polynomial time
per class. Hence, our algorithm is optimal wrt the observation equivalence, and
in several cases explores exponentially fewer traces than any enumerative method
based on the Mazurkiewicz equivalence.\r\n2. For cyclic architectures, we consider
an equivalence between traces which is finer than the observation equivalence;
but coarser than the Mazurkiewicz equivalence, and in some cases is exponentially
coarser. Our data-centric DPOR algorithm remains optimal under this trace equivalence.
\r\nFinally, we perform a basic experimental comparison between the existing Mazurkiewicz-based
DPOR and our data-centric DPOR on a set of academic benchmarks. Our results show
a significant reduction in both running time and the number of explored equivalence
classes."
alternative_title:
- IST Austria Technical Report
author:
- first_name: Marek
full_name: Chalupa, Marek
last_name: Chalupa
- 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: Nishant
full_name: Sinha, Nishant
last_name: Sinha
- first_name: Kapil
full_name: Vaidya, Kapil
last_name: Vaidya
citation:
ama: Chalupa M, Chatterjee K, Pavlogiannis A, Sinha N, Vaidya K. Data-Centric
Dynamic Partial Order Reduction. IST Austria; 2017. doi:10.15479/AT:IST-2017-872-v1-1
apa: Chalupa, M., Chatterjee, K., Pavlogiannis, A., Sinha, N., & Vaidya, K.
(2017). Data-centric dynamic partial order reduction. IST Austria. https://doi.org/10.15479/AT:IST-2017-872-v1-1
chicago: Chalupa, Marek, Krishnendu Chatterjee, Andreas Pavlogiannis, Nishant Sinha,
and Kapil Vaidya. Data-Centric Dynamic Partial Order Reduction. IST Austria,
2017. https://doi.org/10.15479/AT:IST-2017-872-v1-1.
ieee: M. Chalupa, K. Chatterjee, A. Pavlogiannis, N. Sinha, and K. Vaidya, Data-centric
dynamic partial order reduction. IST Austria, 2017.
ista: Chalupa M, Chatterjee K, Pavlogiannis A, Sinha N, Vaidya K. 2017. Data-centric
dynamic partial order reduction, IST Austria, 36p.
mla: Chalupa, Marek, et al. Data-Centric Dynamic Partial Order Reduction.
IST Austria, 2017, doi:10.15479/AT:IST-2017-872-v1-1.
short: M. Chalupa, K. Chatterjee, A. Pavlogiannis, N. Sinha, K. Vaidya, Data-Centric
Dynamic Partial Order Reduction, IST Austria, 2017.
date_created: 2018-12-12T11:39:26Z
date_published: 2017-10-23T00:00:00Z
date_updated: 2023-02-23T12:26:54Z
day: '23'
ddc:
- '000'
department:
- _id: KrCh
doi: 10.15479/AT:IST-2017-872-v1-1
file:
- access_level: open_access
checksum: d2635c4cf013000f0a1b09e80f9e4ab7
content_type: application/pdf
creator: system
date_created: 2018-12-12T11:53:26Z
date_updated: 2020-07-14T12:46:59Z
file_id: '5487'
file_name: IST-2017-872-v1+1_main.pdf
file_size: 910347
relation: main_file
file_date_updated: 2020-07-14T12:46:59Z
has_accepted_license: '1'
language:
- iso: eng
month: '10'
oa: 1
oa_version: Published Version
page: '36'
publication_identifier:
issn:
- 2664-1690
publication_status: published
publisher: IST Austria
pubrep_id: '872'
related_material:
record:
- id: '10417'
relation: later_version
status: public
- id: '5448'
relation: earlier_version
status: public
status: public
title: Data-centric dynamic partial order reduction
type: technical_report
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
year: '2017'
...