[{"abstract":[{"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.","lang":"eng"}],"alternative_title":["IST Austria Technical Report"],"type":"technical_report","oa_version":"Published Version","file":[{"content_type":"application/pdf","file_size":"320453","creator":"fmuehlbo","access_level":"open_access","file_name":"differentialmonitoring-techreport.pdf","checksum":"0f9aafd59444cb6bdca6925d163ab946","date_created":"2021-08-20T19:59:44Z","date_updated":"2021-09-03T12:34:28Z","relation":"main_file","file_id":"9948"}],"ddc":["005"],"title":"Differential monitoring","status":"public","_id":"9946","user_id":"8b945eb4-e2f2-11eb-945a-df72226e66a9","day":"01","has_accepted_license":"1","article_processing_charge":"No","keyword":["run-time verification","software engineering","implicit specification"],"date_published":"2021-09-01T00:00:00Z","page":"17","citation":{"short":"F. Mühlböck, T.A. Henzinger, Differential Monitoring, IST Austria, 2021.","mla":"Mühlböck, Fabian, and Thomas A. Henzinger. Differential Monitoring. IST Austria, 2021, doi: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.","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","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."},"file_date_updated":"2021-09-03T12:34:28Z","date_created":"2021-08-20T20:00:37Z","date_updated":"2023-08-14T07:20:29Z","author":[{"first_name":"Fabian","last_name":"Mühlböck","id":"6395C5F6-89DF-11E9-9C97-6BDFE5697425","orcid":"0000-0003-1548-0177","full_name":"Mühlböck, Fabian"},{"orcid":"0000-0002-2985-7724","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","last_name":"Henzinger","first_name":"Thomas A","full_name":"Henzinger, Thomas A"}],"related_material":{"record":[{"status":"public","relation":"other","id":"9281"},{"id":"10108","status":"public","relation":"shorter_version"}]},"publication_status":"published","publisher":"IST Austria","department":[{"_id":"ToHe"}],"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.","year":"2021","month":"09","publication_identifier":{"issn":["2664-1690"]},"language":[{"iso":"eng"}],"doi":"10.15479/AT:ISTA:9946","project":[{"call_identifier":"FWF","name":"The Wittgenstein Prize","grant_number":"Z211","_id":"25F42A32-B435-11E9-9278-68D0E5697425"}],"oa":1},{"month":"07","publication_identifier":{"issn":["2664-1690"]},"language":[{"iso":"eng"}],"doi":"10.15479/AT:ISTA:8067","oa":1,"file_date_updated":"2020-07-14T12:48:08Z","date_created":"2020-06-30T07:37:39Z","date_updated":"2023-08-22T09:20:36Z","author":[{"first_name":"Alberto","last_name":"Varzi","full_name":"Varzi, Alberto"},{"first_name":"Katharina","last_name":"Thanner","full_name":"Thanner, Katharina"},{"full_name":"Scipioni, Roberto","last_name":"Scipioni","first_name":"Roberto"},{"full_name":"Di Lecce, Daniele","first_name":"Daniele","last_name":"Di Lecce"},{"full_name":"Hassoun, Jusef","last_name":"Hassoun","first_name":"Jusef"},{"first_name":"Susanne","last_name":"Dörfler","full_name":"Dörfler, Susanne"},{"first_name":"Holger","last_name":"Altheus","full_name":"Altheus, Holger"},{"last_name":"Kaskel","first_name":"Stefan","full_name":"Kaskel, Stefan"},{"full_name":"Prehal, Christian","first_name":"Christian","last_name":"Prehal"},{"id":"A8CA28E6-CE23-11E9-AD2D-EC27E6697425","orcid":"0000-0003-2902-5319","first_name":"Stefan Alexander","last_name":"Freunberger","full_name":"Freunberger, Stefan Alexander"}],"related_material":{"record":[{"id":"8361","status":"public","relation":"later_version"}]},"publication_status":"submitted","department":[{"_id":"StFr"}],"publisher":"IST Austria","year":"2020","day":"01","article_processing_charge":"No","has_accepted_license":"1","keyword":["Battery","Lithium metal","Lithium-sulphur","Lithium-air","All-solid-state"],"date_published":"2020-07-01T00:00:00Z","page":"63","citation":{"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.","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.","mla":"Varzi, Alberto, 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","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.","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"},"abstract":[{"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.","lang":"eng"}],"alternative_title":["IST Austria Technical Report"],"type":"technical_report","file":[{"file_name":"20200612_JPS_review_Li_metal_submitted.pdf","access_level":"open_access","creator":"dernst","content_type":"application/pdf","file_size":2612498,"file_id":"8076","relation":"main_file","date_created":"2020-07-02T07:36:04Z","date_updated":"2020-07-14T12:48:08Z","checksum":"d183ca1465a1cbb4f8db27875cd156f7"}],"oa_version":"Published Version","status":"public","title":"Current status and future perspectives of Lithium metal batteries","ddc":["540"],"_id":"8067","user_id":"8b945eb4-e2f2-11eb-945a-df72226e66a9"},{"related_material":{"record":[{"id":"6175","status":"public","relation":"later_version"}]},"pubrep_id":"1066","author":[{"first_name":"1","last_name":"Anonymous","full_name":"Anonymous, 1"},{"full_name":"Anonymous, 2","last_name":"Anonymous","first_name":"2"},{"full_name":"Anonymous, 3","last_name":"Anonymous","first_name":"3"},{"full_name":"Anonymous, 4","first_name":"4","last_name":"Anonymous"},{"full_name":"Anonymous, 5","last_name":"Anonymous","first_name":"5"},{"last_name":"Anonymous","first_name":"6","full_name":"Anonymous, 6"}],"file":[{"access_level":"open_access","file_name":"IST-2018-1066-v1+1_techreport.pdf","creator":"system","content_type":"application/pdf","file_size":4202966,"file_id":"5493","relation":"main_file","checksum":"ba3adafd36fe200385ccda583063b9eb","date_created":"2018-12-12T11:53:32Z","date_updated":"2020-07-14T12:47:00Z"},{"date_created":"2019-05-10T13:22:12Z","date_updated":"2020-07-14T12:47:00Z","checksum":"6cf3a19164bb8e5048a9c8c84dfd9fa3","relation":"main_file","file_id":"6402","file_size":322,"content_type":"text/plain","creator":"dernst","file_name":"authors-names.txt","access_level":"closed"}],"oa_version":"Published Version","date_created":"2018-12-12T11:39:26Z","date_updated":"2023-08-25T08:07:48Z","_id":"5457","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","year":"2018","publisher":"IST Austria","title":"Cost analysis of nondeterministic probabilistic programs","ddc":["000"],"publication_status":"published","status":"public","abstract":[{"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.","lang":"eng"}],"file_date_updated":"2020-07-14T12:47:00Z","type":"technical_report","alternative_title":["IST Austria Technical Report"],"date_published":"2018-11-11T00:00:00Z","language":[{"iso":"eng"}],"oa":1,"citation":{"ista":"Anonymous 1, Anonymous 2, Anonymous 3, Anonymous 4, Anonymous 5, Anonymous 6. 2018. Cost analysis of nondeterministic probabilistic programs, IST Austria, 27p.","apa":"Anonymous, 1, Anonymous, 2, Anonymous, 3, Anonymous, 4, Anonymous, 5, & Anonymous, 6. (2018). Cost analysis of nondeterministic probabilistic programs. IST Austria.","ieee":"1 Anonymous, 2 Anonymous, 3 Anonymous, 4 Anonymous, 5 Anonymous, and 6 Anonymous, Cost analysis of nondeterministic probabilistic programs. IST Austria, 2018.","ama":"Anonymous 1, Anonymous 2, Anonymous 3, Anonymous 4, Anonymous 5, Anonymous 6. Cost Analysis of Nondeterministic Probabilistic Programs. IST Austria; 2018.","chicago":"Anonymous, 1, 2 Anonymous, 3 Anonymous, 4 Anonymous, 5 Anonymous, and 6 Anonymous. Cost Analysis of Nondeterministic Probabilistic Programs. IST Austria, 2018.","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."},"page":"27","has_accepted_license":"1","publication_identifier":{"issn":["2664-1690"]},"month":"11","day":"11","scopus_import":1},{"status":"public","ddc":["000"],"title":"Optimal Dyck reachability for data-dependence and alias analysis","_id":"5455","user_id":"8b945eb4-e2f2-11eb-945a-df72226e66a9","file":[{"content_type":"application/pdf","file_size":960491,"creator":"system","access_level":"open_access","file_name":"IST-2017-870-v1+1_main.pdf","checksum":"177a84a46e3ac17e87b31534ad16a4c9","date_created":"2018-12-12T11:54:02Z","date_updated":"2020-07-14T12:46:59Z","relation":"main_file","file_id":"5524"}],"oa_version":"Published Version","pubrep_id":"870","alternative_title":["IST Austria Technical Report"],"type":"technical_report","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."}],"page":"37","citation":{"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.","short":"K. Chatterjee, B. Choudhary, A. Pavlogiannis, Optimal Dyck Reachability for Data-Dependence and Alias Analysis, IST Austria, 2017.","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.","ieee":"K. Chatterjee, B. Choudhary, and A. Pavlogiannis, Optimal Dyck reachability for data-dependence and alias analysis. IST Austria, 2017.","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","ista":"Chatterjee K, Choudhary B, Pavlogiannis A. 2017. Optimal Dyck reachability for data-dependence and alias analysis, IST Austria, 37p.","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"},"date_published":"2017-10-23T00:00:00Z","has_accepted_license":"1","article_processing_charge":"No","day":"23","department":[{"_id":"KrCh"}],"publisher":"IST Austria","publication_status":"published","year":"2017","date_created":"2018-12-12T11:39:26Z","date_updated":"2023-02-21T15:54:10Z","related_material":{"record":[{"relation":"later_version","status":"public","id":"10416"}]},"author":[{"full_name":"Chatterjee, Krishnendu","last_name":"Chatterjee","first_name":"Krishnendu","orcid":"0000-0002-4561-241X","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87"},{"last_name":"Choudhary","first_name":"Bhavya","full_name":"Choudhary, Bhavya"},{"id":"49704004-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-8943-0722","first_name":"Andreas","last_name":"Pavlogiannis","full_name":"Pavlogiannis, Andreas"}],"file_date_updated":"2020-07-14T12:46:59Z","oa":1,"language":[{"iso":"eng"}],"doi":"10.15479/AT:IST-2017-870-v1-1","publication_identifier":{"issn":["2664-1690"]},"month":"10"},{"day":"23","month":"10","publication_identifier":{"issn":["2664-1690"]},"has_accepted_license":"1","doi":"10.15479/AT:IST-2017-872-v1-1","date_published":"2017-10-23T00:00:00Z","language":[{"iso":"eng"}],"citation":{"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.","short":"M. Chalupa, K. Chatterjee, A. Pavlogiannis, N. Sinha, K. Vaidya, Data-Centric Dynamic Partial Order Reduction, IST Austria, 2017.","mla":"Chalupa, Marek, et al. Data-Centric Dynamic Partial Order Reduction. IST Austria, 2017, doi: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.","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","ista":"Chalupa M, Chatterjee K, Pavlogiannis A, Sinha N, Vaidya K. 2017. Data-centric dynamic partial order reduction, IST Austria, 36p.","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"},"oa":1,"page":"36","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."}],"file_date_updated":"2020-07-14T12:46:59Z","type":"technical_report","alternative_title":["IST Austria Technical Report"],"author":[{"full_name":"Chalupa, Marek","last_name":"Chalupa","first_name":"Marek"},{"id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-4561-241X","first_name":"Krishnendu","last_name":"Chatterjee","full_name":"Chatterjee, Krishnendu"},{"full_name":"Pavlogiannis, Andreas","orcid":"0000-0002-8943-0722","id":"49704004-F248-11E8-B48F-1D18A9856A87","last_name":"Pavlogiannis","first_name":"Andreas"},{"last_name":"Sinha","first_name":"Nishant","full_name":"Sinha, Nishant"},{"full_name":"Vaidya, Kapil","first_name":"Kapil","last_name":"Vaidya"}],"related_material":{"record":[{"id":"10417","relation":"later_version","status":"public"},{"id":"5448","status":"public","relation":"earlier_version"}]},"pubrep_id":"872","date_created":"2018-12-12T11:39:26Z","date_updated":"2023-02-23T12:26:54Z","file":[{"date_created":"2018-12-12T11:53:26Z","date_updated":"2020-07-14T12:46:59Z","checksum":"d2635c4cf013000f0a1b09e80f9e4ab7","file_id":"5487","relation":"main_file","creator":"system","content_type":"application/pdf","file_size":910347,"file_name":"IST-2017-872-v1+1_main.pdf","access_level":"open_access"}],"oa_version":"Published Version","_id":"5456","year":"2017","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","ddc":["000"],"publication_status":"published","status":"public","title":"Data-centric dynamic partial order reduction","publisher":"IST Austria","department":[{"_id":"KrCh"}]}]