--- _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' ...