[{"acknowledgement":"The research was partially funded by the ERC CoG 863818 (ForM-SMArt) and the Vienna Science and Technology Fund (WWTF) through project ICT15-003.","publisher":"Springer Nature","quality_controlled":"1","oa":1,"isi":1,"has_accepted_license":"1","year":"2021","day":"15","publication":"33rd International Conference on Computer-Aided Verification ","page":"341-366","date_published":"2021-07-15T00:00:00Z","doi":"10.1007/978-3-030-81685-8_16","date_created":"2021-09-05T22:01:24Z","project":[{"grant_number":"ICT15-003","name":"Efficient Algorithms for Computer Aided Verification","_id":"25892FC0-B435-11E9-9278-68D0E5697425"},{"name":"Formal Methods for Stochastic Models: Algorithms and Applications","grant_number":"863818","_id":"0599E47C-7A3F-11EA-A408-12923DDC885E","call_identifier":"H2020"}],"citation":{"ista":"Agarwal P, Chatterjee K, Pathak S, Pavlogiannis A, Toman V. 2021. Stateless model checking under a reads-value-from equivalence. 33rd International Conference on Computer-Aided Verification . CAV: Computer Aided Verification , LNCS, vol. 12759, 341–366.","chicago":"Agarwal, Pratyush, Krishnendu Chatterjee, Shreya Pathak, Andreas Pavlogiannis, and Viktor Toman. “Stateless Model Checking under a Reads-Value-from Equivalence.” In 33rd International Conference on Computer-Aided Verification , 12759:341–66. Springer Nature, 2021. https://doi.org/10.1007/978-3-030-81685-8_16.","short":"P. Agarwal, K. Chatterjee, S. Pathak, A. Pavlogiannis, V. Toman, in:, 33rd International Conference on Computer-Aided Verification , Springer Nature, 2021, pp. 341–366.","ieee":"P. Agarwal, K. Chatterjee, S. Pathak, A. Pavlogiannis, and V. Toman, “Stateless model checking under a reads-value-from equivalence,” in 33rd International Conference on Computer-Aided Verification , Virtual, 2021, vol. 12759, pp. 341–366.","ama":"Agarwal P, Chatterjee K, Pathak S, Pavlogiannis A, Toman V. Stateless model checking under a reads-value-from equivalence. In: 33rd International Conference on Computer-Aided Verification . Vol 12759. Springer Nature; 2021:341-366. doi:10.1007/978-3-030-81685-8_16","apa":"Agarwal, P., Chatterjee, K., Pathak, S., Pavlogiannis, A., & Toman, V. (2021). Stateless model checking under a reads-value-from equivalence. In 33rd International Conference on Computer-Aided Verification (Vol. 12759, pp. 341–366). Virtual: Springer Nature. https://doi.org/10.1007/978-3-030-81685-8_16","mla":"Agarwal, Pratyush, et al. “Stateless Model Checking under a Reads-Value-from Equivalence.” 33rd International Conference on Computer-Aided Verification , vol. 12759, Springer Nature, 2021, pp. 341–66, doi:10.1007/978-3-030-81685-8_16."},"user_id":"4359f0d1-fa6c-11eb-b949-802e58b17ae8","author":[{"last_name":"Agarwal","full_name":"Agarwal, Pratyush","first_name":"Pratyush"},{"last_name":"Chatterjee","orcid":"0000-0002-4561-241X","full_name":"Chatterjee, Krishnendu","first_name":"Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87"},{"last_name":"Pathak","full_name":"Pathak, Shreya","first_name":"Shreya"},{"last_name":"Pavlogiannis","full_name":"Pavlogiannis, Andreas","orcid":"0000-0002-8943-0722","id":"49704004-F248-11E8-B48F-1D18A9856A87","first_name":"Andreas"},{"id":"3AF3DA7C-F248-11E8-B48F-1D18A9856A87","first_name":"Viktor","full_name":"Toman, Viktor","orcid":"0000-0001-9036-063X","last_name":"Toman"}],"external_id":{"arxiv":["2105.06424"],"isi":["000698732400016"]},"article_processing_charge":"Yes","title":"Stateless model checking under a reads-value-from equivalence","abstract":[{"text":"Stateless model checking (SMC) is one of the standard approaches to the verification of concurrent programs. As scheduling non-determinism creates exponentially large spaces of thread interleavings, SMC attempts to partition this space into equivalence classes and explore only a few representatives from each class. The efficiency of this approach depends on two factors: (a) the coarseness of the partitioning, and (b) the time to generate representatives in each class. For this reason, the search for coarse partitionings that are efficiently explorable is an active research challenge. In this work we present RVF-SMC , a new SMC algorithm that uses a novel reads-value-from (RVF) partitioning. Intuitively, two interleavings are deemed equivalent if they agree on the value obtained in each read event, and read events induce consistent causal orderings between them. The RVF partitioning is provably coarser than recent approaches based on Mazurkiewicz and “reads-from” partitionings. Our experimental evaluation reveals that RVF is quite often a very effective equivalence, as the underlying partitioning is exponentially coarser than other approaches. Moreover, RVF-SMC generates representatives very efficiently, as the reduction in the partitioning is often met with significant speed-ups in the model checking task.","lang":"eng"}],"oa_version":"Published Version","alternative_title":["LNCS"],"scopus_import":"1","month":"07","publication_identifier":{"eisbn":["978-3-030-81685-8"],"isbn":["978-3-030-81684-1"],"eissn":["1611-3349"],"issn":["0302-9743"]},"publication_status":"published","file":[{"file_size":1516756,"date_updated":"2022-05-13T07:00:20Z","creator":"dernst","file_name":"2021_LNCS_Agarwal.pdf","date_created":"2022-05-13T07:00:20Z","content_type":"application/pdf","relation":"main_file","access_level":"open_access","success":1,"checksum":"4b346e5fbaa8b9bdf107819c7b2aadee","file_id":"11368"}],"language":[{"iso":"eng"}],"related_material":{"record":[{"id":"10199","status":"public","relation":"dissertation_contains"}]},"volume":"12759 ","ec_funded":1,"_id":"9987","type":"conference","tmp":{"legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","image":"/images/cc_by.png","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","short":"CC BY (4.0)"},"conference":{"start_date":"2021-07-20","location":"Virtual","end_date":"2021-07-23","name":"CAV: Computer Aided Verification "},"status":"public","date_updated":"2023-09-07T13:30:27Z","ddc":["000"],"department":[{"_id":"KrCh"}],"file_date_updated":"2022-05-13T07:00:20Z"},{"project":[{"grant_number":"863818","name":"Formal Methods for Stochastic Models: Algorithms and Applications","call_identifier":"H2020","_id":"0599E47C-7A3F-11EA-A408-12923DDC885E"},{"_id":"25892FC0-B435-11E9-9278-68D0E5697425","name":"Efficient Algorithms for Computer Aided Verification","grant_number":"ICT15-003"}],"article_number":"164","title":"The reads-from equivalence for the TSO and PSO memory models","article_processing_charge":"No","external_id":{"arxiv":["2011.11763"]},"author":[{"first_name":"Truc Lam","full_name":"Bui, Truc Lam","last_name":"Bui"},{"full_name":"Chatterjee, Krishnendu","orcid":"0000-0002-4561-241X","last_name":"Chatterjee","first_name":"Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87"},{"full_name":"Gautam, Tushar","last_name":"Gautam","first_name":"Tushar"},{"id":"49704004-F248-11E8-B48F-1D18A9856A87","first_name":"Andreas","last_name":"Pavlogiannis","full_name":"Pavlogiannis, Andreas","orcid":"0000-0002-8943-0722"},{"full_name":"Toman, Viktor","orcid":"0000-0001-9036-063X","last_name":"Toman","id":"3AF3DA7C-F248-11E8-B48F-1D18A9856A87","first_name":"Viktor"}],"user_id":"8b945eb4-e2f2-11eb-945a-df72226e66a9","citation":{"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.","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.","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","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","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.","short":"T.L. Bui, K. Chatterjee, T. Gautam, A. Pavlogiannis, V. Toman, Proceedings of the ACM on Programming Languages 5 (2021).","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."},"oa":1,"quality_controlled":"1","publisher":"Association for Computing Machinery","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.","date_created":"2021-10-27T15:05:34Z","doi":"10.1145/3485541","date_published":"2021-10-15T00:00:00Z","publication":"Proceedings of the ACM on Programming Languages","day":"15","year":"2021","has_accepted_license":"1","keyword":["safety","risk","reliability and quality","software"],"status":"public","tmp":{"legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","image":"/images/cc_by.png","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","short":"CC BY (4.0)"},"type":"journal_article","article_type":"original","_id":"10191","file_date_updated":"2021-11-04T07:24:48Z","department":[{"_id":"GradSch"},{"_id":"KrCh"}],"ddc":["000"],"date_updated":"2023-09-07T13:30:27Z","intvolume":" 5","month":"10","scopus_import":"1","oa_version":"Published Version","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"}],"ec_funded":1,"issue":"OOPSLA","related_material":{"record":[{"relation":"dissertation_contains","status":"public","id":"10199"}]},"volume":5,"language":[{"iso":"eng"}],"file":[{"access_level":"open_access","relation":"main_file","content_type":"application/pdf","checksum":"9d6dce7b611853c529bb7b1915ac579e","file_id":"10215","success":1,"creator":"cchlebak","date_updated":"2021-11-04T07:24:48Z","file_size":2903485,"date_created":"2021-11-04T07:24:48Z","file_name":"2021_ProcACMPL_Bui.pdf"}],"publication_status":"published","publication_identifier":{"eissn":["2475-1421"]}},{"_id":"10199","keyword":["concurrency","verification","model checking"],"status":"public","type":"dissertation","ddc":["000"],"date_updated":"2023-09-19T09:59:54Z","supervisor":[{"first_name":"Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","last_name":"Chatterjee","full_name":"Chatterjee, Krishnendu","orcid":"0000-0002-4561-241X"}],"file_date_updated":"2021-11-09T09:00:50Z","department":[{"_id":"GradSch"},{"_id":"KrCh"}],"oa_version":"Published Version","abstract":[{"lang":"eng","text":"The design and verification of concurrent systems remains an open challenge due to the non-determinism that arises from the inter-process communication. In particular, concurrent programs are notoriously difficult both to be written correctly and to be analyzed formally, as complex thread interaction has to be accounted for. The difficulties are further exacerbated when concurrent programs get executed on modern-day hardware, which contains various buffering and caching mechanisms for efficiency reasons. This causes further subtle non-determinism, which can often produce very unintuitive behavior of the concurrent programs. Model checking is at the forefront of tackling the verification problem, where the task is to decide, given as input a concurrent system and a desired property, whether the system satisfies the property. The inherent state-space explosion problem in model checking of concurrent systems causes naïve explicit methods not to scale, thus more inventive methods are required. One such method is stateless model checking (SMC), which explores in memory-efficient manner the program executions rather than the states of the program. State-of-the-art SMC is typically coupled with partial order reduction (POR) techniques, which argue that certain executions provably produce identical system behavior, thus limiting the amount of executions one needs to explore in order to cover all possible behaviors. Another method to tackle the state-space explosion is symbolic model checking, where the considered techniques operate on a succinct implicit representation of the input system rather than explicitly accessing the system. In this thesis we present new techniques for verification of concurrent systems. We present several novel POR methods for SMC of concurrent programs under various models of semantics, some of which account for write-buffering mechanisms. Additionally, we present novel algorithms for symbolic model checking of finite-state concurrent systems, where the desired property of the systems is to ensure a formally defined notion of fairness."}],"acknowledged_ssus":[{"_id":"SSU"}],"month":"10","alternative_title":["ISTA Thesis"],"language":[{"iso":"eng"}],"file":[{"file_name":"toman_th_final.pdf","date_created":"2021-11-08T14:12:22Z","creator":"vtoman","file_size":2915234,"date_updated":"2021-11-08T14:12:22Z","file_id":"10225","checksum":"4f412a1ee60952221b499a4b1268df35","relation":"main_file","access_level":"open_access","content_type":"application/pdf"},{"content_type":"application/zip","access_level":"closed","relation":"source_file","checksum":"9584943f99127be2dd2963f6784c37d4","file_id":"10226","date_updated":"2021-11-09T09:00:50Z","file_size":8616056,"creator":"vtoman","date_created":"2021-11-08T14:12:46Z","file_name":"toman_thesis.zip"}],"degree_awarded":"PhD","publication_status":"published","publication_identifier":{"issn":["2663-337X"]},"ec_funded":1,"related_material":{"record":[{"status":"public","id":"10190","relation":"part_of_dissertation"},{"relation":"part_of_dissertation","id":"10191","status":"public"},{"id":"9987","status":"public","relation":"part_of_dissertation"},{"relation":"part_of_dissertation","id":"141","status":"public"}]},"project":[{"call_identifier":"H2020","_id":"2564DBCA-B435-11E9-9278-68D0E5697425","name":"International IST Doctoral Program","grant_number":"665385"},{"name":"Rigorous Systems Engineering","grant_number":"S11402-N23","call_identifier":"FWF","_id":"25F2ACDE-B435-11E9-9278-68D0E5697425"},{"_id":"25892FC0-B435-11E9-9278-68D0E5697425","name":"Efficient Algorithms for Computer Aided Verification","grant_number":"ICT15-003"},{"_id":"0599E47C-7A3F-11EA-A408-12923DDC885E","call_identifier":"H2020","grant_number":"863818","name":"Formal Methods for Stochastic Models: Algorithms and Applications"}],"user_id":"c635000d-4b10-11ee-a964-aac5a93f6ac1","citation":{"chicago":"Toman, Viktor. “Improved Verification Techniques for Concurrent Systems.” Institute of Science and Technology Austria, 2021. https://doi.org/10.15479/at:ista:10199.","ista":"Toman V. 2021. Improved verification techniques for concurrent systems. Institute of Science and Technology Austria.","mla":"Toman, Viktor. Improved Verification Techniques for Concurrent Systems. Institute of Science and Technology Austria, 2021, doi:10.15479/at:ista:10199.","short":"V. Toman, Improved Verification Techniques for Concurrent Systems, Institute of Science and Technology Austria, 2021.","ieee":"V. Toman, “Improved verification techniques for concurrent systems,” Institute of Science and Technology Austria, 2021.","ama":"Toman V. Improved verification techniques for concurrent systems. 2021. doi:10.15479/at:ista:10199","apa":"Toman, V. (2021). Improved verification techniques for concurrent systems. Institute of Science and Technology Austria. https://doi.org/10.15479/at:ista:10199"},"title":"Improved verification techniques for concurrent systems","article_processing_charge":"No","author":[{"id":"3AF3DA7C-F248-11E8-B48F-1D18A9856A87","first_name":"Viktor","last_name":"Toman","orcid":"0000-0001-9036-063X","full_name":"Toman, Viktor"}],"oa":1,"publisher":"Institute of Science and Technology Austria","day":"31","year":"2021","has_accepted_license":"1","date_created":"2021-10-29T20:09:01Z","date_published":"2021-10-31T00:00:00Z","doi":"10.15479/at:ista:10199","page":"166"},{"page":"109-128","date_created":"2019-10-14T06:57:49Z","date_published":"2019-09-04T00:00:00Z","doi":"10.1007/978-3-030-30281-8_7","year":"2019","isi":1,"publication":"16th International Conference on Quantitative Evaluation of Systems","day":"04","oa":1,"quality_controlled":"1","publisher":"Springer Nature","external_id":{"isi":["000679281300007"],"arxiv":["1906.08178"]},"article_processing_charge":"No","author":[{"full_name":"Ashok, Pranav","last_name":"Ashok","first_name":"Pranav"},{"full_name":"Brázdil, Tomáš","last_name":"Brázdil","first_name":"Tomáš"},{"id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","first_name":"Krishnendu","last_name":"Chatterjee","full_name":"Chatterjee, Krishnendu","orcid":"0000-0002-4561-241X"},{"first_name":"Jan","last_name":"Křetínský","full_name":"Křetínský, Jan"},{"orcid":"0000-0001-8622-7887","full_name":"Lampert, Christoph","last_name":"Lampert","id":"40C20FD2-F248-11E8-B48F-1D18A9856A87","first_name":"Christoph"},{"id":"3AF3DA7C-F248-11E8-B48F-1D18A9856A87","first_name":"Viktor","orcid":"0000-0001-9036-063X","full_name":"Toman, Viktor","last_name":"Toman"}],"title":"Strategy representation by decision trees with linear classifiers","citation":{"ista":"Ashok P, Brázdil T, Chatterjee K, Křetínský J, Lampert C, Toman V. 2019. Strategy representation by decision trees with linear classifiers. 16th International Conference on Quantitative Evaluation of Systems. QEST: Quantitative Evaluation of Systems, LNCS, vol. 11785, 109–128.","chicago":"Ashok, Pranav, Tomáš Brázdil, Krishnendu Chatterjee, Jan Křetínský, Christoph Lampert, and Viktor Toman. “Strategy Representation by Decision Trees with Linear Classifiers.” In 16th International Conference on Quantitative Evaluation of Systems, 11785:109–28. Springer Nature, 2019. https://doi.org/10.1007/978-3-030-30281-8_7.","apa":"Ashok, P., Brázdil, T., Chatterjee, K., Křetínský, J., Lampert, C., & Toman, V. (2019). Strategy representation by decision trees with linear classifiers. In 16th International Conference on Quantitative Evaluation of Systems (Vol. 11785, pp. 109–128). Glasgow, United Kingdom: Springer Nature. https://doi.org/10.1007/978-3-030-30281-8_7","ama":"Ashok P, Brázdil T, Chatterjee K, Křetínský J, Lampert C, Toman V. Strategy representation by decision trees with linear classifiers. In: 16th International Conference on Quantitative Evaluation of Systems. Vol 11785. Springer Nature; 2019:109-128. doi:10.1007/978-3-030-30281-8_7","ieee":"P. Ashok, T. Brázdil, K. Chatterjee, J. Křetínský, C. Lampert, and V. Toman, “Strategy representation by decision trees with linear classifiers,” in 16th International Conference on Quantitative Evaluation of Systems, Glasgow, United Kingdom, 2019, vol. 11785, pp. 109–128.","short":"P. Ashok, T. Brázdil, K. Chatterjee, J. Křetínský, C. Lampert, V. Toman, in:, 16th International Conference on Quantitative Evaluation of Systems, Springer Nature, 2019, pp. 109–128.","mla":"Ashok, Pranav, et al. “Strategy Representation by Decision Trees with Linear Classifiers.” 16th International Conference on Quantitative Evaluation of Systems, vol. 11785, Springer Nature, 2019, pp. 109–28, doi:10.1007/978-3-030-30281-8_7."},"user_id":"4359f0d1-fa6c-11eb-b949-802e58b17ae8","project":[{"call_identifier":"FWF","_id":"25863FF4-B435-11E9-9278-68D0E5697425","grant_number":"S11407","name":"Game Theory"},{"name":"Rigorous Systems Engineering","grant_number":"S11402-N23","_id":"25F2ACDE-B435-11E9-9278-68D0E5697425","call_identifier":"FWF"},{"_id":"25892FC0-B435-11E9-9278-68D0E5697425","grant_number":"ICT15-003","name":"Efficient Algorithms for Computer Aided Verification"}],"volume":11785,"publication_status":"published","publication_identifier":{"eisbn":["9783030302818"],"isbn":["9783030302801"],"issn":["0302-9743"]},"language":[{"iso":"eng"}],"main_file_link":[{"open_access":"1","url":"https://arxiv.org/abs/1906.08178"}],"scopus_import":"1","alternative_title":["LNCS"],"intvolume":" 11785","month":"09","abstract":[{"text":"Graph games and Markov decision processes (MDPs) are standard models in reactive synthesis and verification of probabilistic systems with nondeterminism. The class of 𝜔 -regular winning conditions; e.g., safety, reachability, liveness, parity conditions; provides a robust and expressive specification formalism for properties that arise in analysis of reactive systems. The resolutions of nondeterminism in games and MDPs are represented as strategies, and we consider succinct representation of such strategies. The decision-tree data structure from machine learning retains the flavor of decisions of strategies and allows entropy-based minimization to obtain succinct trees. However, in contrast to traditional machine-learning problems where small errors are allowed, for winning strategies in graph games and MDPs no error is allowed, and the decision tree must represent the entire strategy. In this work we propose decision trees with linear classifiers for representation of strategies in graph games and MDPs. We have implemented strategy representation using this data structure and we present experimental results for problems on graph games and MDPs, which show that this new data structure presents a much more efficient strategy representation as compared to standard decision trees.","lang":"eng"}],"oa_version":"Preprint","department":[{"_id":"KrCh"},{"_id":"ChLa"}],"date_updated":"2023-08-30T06:59:36Z","conference":{"name":"QEST: Quantitative Evaluation of Systems","location":"Glasgow, United Kingdom","end_date":"2019-09-12","start_date":"2019-09-10"},"type":"conference","status":"public","_id":"6942"},{"_id":"10190","tmp":{"legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","image":"/images/cc_by.png","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","short":"CC BY (4.0)"},"conference":{"end_date":"2019-10-25","location":"Athens, Greece","start_date":"2019-10-23","name":"OOPSLA: Object-oriented Programming, Systems, Languages and Applications"},"type":"conference","keyword":["safety","risk","reliability and quality","software"],"status":"public","date_updated":"2023-09-07T13:30:27Z","ddc":["000"],"file_date_updated":"2021-11-12T11:41:56Z","department":[{"_id":"GradSch"},{"_id":"KrCh"}],"abstract":[{"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.","lang":"eng"}],"oa_version":"Published Version","main_file_link":[{"url":"https://dl.acm.org/doi/10.1145/3360550","open_access":"1"}],"intvolume":" 3","month":"10","publication_status":"published","publication_identifier":{"eissn":["2475-1421"]},"language":[{"iso":"eng"}],"file":[{"date_created":"2021-11-12T11:41:56Z","file_name":"2019_ACM_Chatterjee.pdf","creator":"cchlebak","date_updated":"2021-11-12T11:41:56Z","file_size":570829,"checksum":"2149979c46964c4d117af06ccb6c0834","file_id":"10278","success":1,"access_level":"open_access","relation":"main_file","content_type":"application/pdf"}],"volume":3,"related_material":{"record":[{"relation":"dissertation_contains","status":"public","id":"10199"}]},"article_number":"124","project":[{"name":"Efficient Algorithms for Computer Aided Verification","grant_number":"ICT15-003","_id":"25892FC0-B435-11E9-9278-68D0E5697425"},{"name":"Game Theory","grant_number":"S11407","_id":"25863FF4-B435-11E9-9278-68D0E5697425","call_identifier":"FWF"},{"call_identifier":"FWF","_id":"25832EC2-B435-11E9-9278-68D0E5697425","name":"Rigorous Systems Engineering","grant_number":"S 11407_N23"},{"grant_number":"S11402-N23","name":"Moderne Concurrency Paradigms","_id":"25F5A88A-B435-11E9-9278-68D0E5697425","call_identifier":"FWF"}],"citation":{"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.","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","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.","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.","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.","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."},"user_id":"8b945eb4-e2f2-11eb-945a-df72226e66a9","article_processing_charge":"No","external_id":{"arxiv":["1909.00989"]},"author":[{"last_name":"Chatterjee","full_name":"Chatterjee, Krishnendu","orcid":"0000-0002-4561-241X","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","first_name":"Krishnendu"},{"last_name":"Pavlogiannis","full_name":"Pavlogiannis, Andreas","orcid":"0000-0002-8943-0722","id":"49704004-F248-11E8-B48F-1D18A9856A87","first_name":"Andreas"},{"full_name":"Toman, Viktor","orcid":"0000-0001-9036-063X","last_name":"Toman","id":"3AF3DA7C-F248-11E8-B48F-1D18A9856A87","first_name":"Viktor"}],"title":"Value-centric dynamic partial order reduction","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","oa":1,"publisher":"ACM","quality_controlled":"1","year":"2019","has_accepted_license":"1","publication":"Proceedings of the 34th ACM International Conference on Object-Oriented Programming, Systems, Languages, and Applications","day":"10","date_created":"2021-10-27T14:57:06Z","date_published":"2019-10-10T00:00:00Z","doi":"10.1145/3360550"},{"has_accepted_license":"1","isi":1,"year":"2018","day":"12","page":"385 - 407","date_published":"2018-04-12T00:00:00Z","doi":"10.1007/978-3-319-89960-2_21","date_created":"2018-12-11T11:45:41Z","quality_controlled":"1","publisher":"Springer","oa":1,"citation":{"mla":"Brázdil, Tomáš, et al. Strategy Representation by Decision Trees in Reactive Synthesis. Vol. 10805, Springer, 2018, pp. 385–407, doi:10.1007/978-3-319-89960-2_21.","short":"T. Brázdil, K. Chatterjee, J. Kretinsky, V. Toman, in:, Springer, 2018, pp. 385–407.","ieee":"T. Brázdil, K. Chatterjee, J. Kretinsky, and V. Toman, “Strategy representation by decision trees in reactive synthesis,” presented at the TACAS 2018: Tools and Algorithms for the Construction and Analysis of Systems, Thessaloniki, Greece, 2018, vol. 10805, pp. 385–407.","ama":"Brázdil T, Chatterjee K, Kretinsky J, Toman V. Strategy representation by decision trees in reactive synthesis. In: Vol 10805. Springer; 2018:385-407. doi:10.1007/978-3-319-89960-2_21","apa":"Brázdil, T., Chatterjee, K., Kretinsky, J., & Toman, V. (2018). Strategy representation by decision trees in reactive synthesis (Vol. 10805, pp. 385–407). Presented at the TACAS 2018: Tools and Algorithms for the Construction and Analysis of Systems, Thessaloniki, Greece: Springer. https://doi.org/10.1007/978-3-319-89960-2_21","chicago":"Brázdil, Tomáš, Krishnendu Chatterjee, Jan Kretinsky, and Viktor Toman. “Strategy Representation by Decision Trees in Reactive Synthesis,” 10805:385–407. Springer, 2018. https://doi.org/10.1007/978-3-319-89960-2_21.","ista":"Brázdil T, Chatterjee K, Kretinsky J, Toman V. 2018. Strategy representation by decision trees in reactive synthesis. TACAS 2018: Tools and Algorithms for the Construction and Analysis of Systems, LNCS, vol. 10805, 385–407."},"user_id":"c635000d-4b10-11ee-a964-aac5a93f6ac1","publist_id":"7584","author":[{"first_name":"Tomáš","last_name":"Brázdil","full_name":"Brázdil, Tomáš"},{"last_name":"Chatterjee","full_name":"Chatterjee, Krishnendu","orcid":"0000-0002-4561-241X","first_name":"Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87"},{"id":"44CEF464-F248-11E8-B48F-1D18A9856A87","first_name":"Jan","full_name":"Kretinsky, Jan","orcid":"0000-0002-8122-2881","last_name":"Kretinsky"},{"first_name":"Viktor","id":"3AF3DA7C-F248-11E8-B48F-1D18A9856A87","last_name":"Toman","orcid":"0000-0001-9036-063X","full_name":"Toman, Viktor"}],"external_id":{"isi":["000546326300021"]},"article_processing_charge":"No","title":"Strategy representation by decision trees in reactive synthesis","project":[{"_id":"25892FC0-B435-11E9-9278-68D0E5697425","name":"Efficient Algorithms for Computer Aided Verification","grant_number":"ICT15-003"},{"name":"Rigorous Systems Engineering","grant_number":"S 11407_N23","call_identifier":"FWF","_id":"25832EC2-B435-11E9-9278-68D0E5697425"},{"call_identifier":"FP7","_id":"2581B60A-B435-11E9-9278-68D0E5697425","grant_number":"279307","name":"Quantitative Graph Games: Theory and Applications"},{"grant_number":"665385","name":"International IST Doctoral Program","call_identifier":"H2020","_id":"2564DBCA-B435-11E9-9278-68D0E5697425"}],"publication_status":"published","file":[{"file_id":"5723","checksum":"b13874ffb114932ad9cc2586b7469db4","access_level":"open_access","relation":"main_file","content_type":"application/pdf","date_created":"2018-12-17T16:29:08Z","file_name":"2018_LNCS_Brazdil.pdf","creator":"dernst","date_updated":"2020-07-14T12:45:57Z","file_size":1829940}],"language":[{"iso":"eng"}],"volume":10805,"ec_funded":1,"abstract":[{"text":"Graph games played by two players over finite-state graphs are central in many problems in computer science. In particular, graph games with ω -regular winning conditions, specified as parity objectives, which can express properties such as safety, liveness, fairness, are the basic framework for verification and synthesis of reactive systems. The decisions for a player at various states of the graph game are represented as strategies. While the algorithmic problem for solving graph games with parity objectives has been widely studied, the most prominent data-structure for strategy representation in graph games has been binary decision diagrams (BDDs). However, due to the bit-level representation, BDDs do not retain the inherent flavor of the decisions of strategies, and are notoriously hard to minimize to obtain succinct representation. In this work we propose decision trees for strategy representation in graph games. Decision trees retain the flavor of decisions of strategies and allow entropy-based minimization to obtain succinct trees. However, decision trees work in settings (e.g., probabilistic models) where errors are allowed, and overfitting of data is typically avoided. In contrast, for strategies in graph games no error is allowed, and the decision tree must represent the entire strategy. We develop new techniques to extend decision trees to overcome the above obstacles, while retaining the entropy-based techniques to obtain succinct trees. We have implemented our techniques to extend the existing decision tree solvers. We present experimental results for problems in reactive synthesis to show that decision trees provide a much more efficient data-structure for strategy representation as compared to BDDs.","lang":"eng"}],"oa_version":"Published Version","alternative_title":["LNCS"],"scopus_import":"1","month":"04","intvolume":" 10805","date_updated":"2023-09-19T09:57:08Z","ddc":["000"],"department":[{"_id":"KrCh"},{"_id":"ToHe"}],"file_date_updated":"2020-07-14T12:45:57Z","_id":"297","type":"conference","tmp":{"legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","image":"/images/cc_by.png","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","short":"CC BY (4.0)"},"conference":{"name":"TACAS 2018: Tools and Algorithms for the Construction and Analysis of Systems","start_date":"2018-04-14","location":"Thessaloniki, Greece","end_date":"2018-04-20"},"status":"public"},{"article_processing_charge":"No","external_id":{"isi":["000491469700013"]},"publist_id":"7782","author":[{"first_name":"Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","last_name":"Chatterjee","orcid":"0000-0002-4561-241X","full_name":"Chatterjee, Krishnendu"},{"last_name":"Henzinger","orcid":"0000-0002-5008-6530","full_name":"Henzinger, Monika H","first_name":"Monika H","id":"540c9bbd-f2de-11ec-812d-d04a5be85630"},{"full_name":"Loitzenbauer, Veronika","last_name":"Loitzenbauer","first_name":"Veronika"},{"first_name":"Simin","full_name":"Oraee, Simin","last_name":"Oraee"},{"first_name":"Viktor","id":"3AF3DA7C-F248-11E8-B48F-1D18A9856A87","last_name":"Toman","full_name":"Toman, Viktor","orcid":"0000-0001-9036-063X"}],"title":"Symbolic algorithms for graphs and Markov decision processes with fairness objectives","citation":{"mla":"Chatterjee, Krishnendu, et al. Symbolic Algorithms for Graphs and Markov Decision Processes with Fairness Objectives. Vol. 10982, Springer, 2018, pp. 178–97, doi:10.1007/978-3-319-96142-2_13.","short":"K. Chatterjee, M.H. Henzinger, V. Loitzenbauer, S. Oraee, V. Toman, in:, Springer, 2018, pp. 178–197.","ieee":"K. Chatterjee, M. H. Henzinger, V. Loitzenbauer, S. Oraee, and V. Toman, “Symbolic algorithms for graphs and Markov decision processes with fairness objectives,” presented at the CAV: Computer Aided Verification, Oxford, United Kingdom, 2018, vol. 10982, pp. 178–197.","ama":"Chatterjee K, Henzinger MH, Loitzenbauer V, Oraee S, Toman V. Symbolic algorithms for graphs and Markov decision processes with fairness objectives. In: Vol 10982. Springer; 2018:178-197. doi:10.1007/978-3-319-96142-2_13","apa":"Chatterjee, K., Henzinger, M. H., Loitzenbauer, V., Oraee, S., & Toman, V. (2018). Symbolic algorithms for graphs and Markov decision processes with fairness objectives (Vol. 10982, pp. 178–197). Presented at the CAV: Computer Aided Verification, Oxford, United Kingdom: Springer. https://doi.org/10.1007/978-3-319-96142-2_13","chicago":"Chatterjee, Krishnendu, Monika H Henzinger, Veronika Loitzenbauer, Simin Oraee, and Viktor Toman. “Symbolic Algorithms for Graphs and Markov Decision Processes with Fairness Objectives,” 10982:178–97. Springer, 2018. https://doi.org/10.1007/978-3-319-96142-2_13.","ista":"Chatterjee K, Henzinger MH, Loitzenbauer V, Oraee S, Toman V. 2018. Symbolic algorithms for graphs and Markov decision processes with fairness objectives. CAV: Computer Aided Verification, LNCS, vol. 10982, 178–197."},"user_id":"c635000d-4b10-11ee-a964-aac5a93f6ac1","project":[{"grant_number":"279307","name":"Quantitative Graph Games: Theory and Applications","call_identifier":"FP7","_id":"2581B60A-B435-11E9-9278-68D0E5697425"},{"_id":"25892FC0-B435-11E9-9278-68D0E5697425","name":"Efficient Algorithms for Computer Aided Verification","grant_number":"ICT15-003"},{"call_identifier":"FWF","_id":"25832EC2-B435-11E9-9278-68D0E5697425","grant_number":"S 11407_N23","name":"Rigorous Systems Engineering"},{"name":"International IST Doctoral Program","grant_number":"665385","call_identifier":"H2020","_id":"2564DBCA-B435-11E9-9278-68D0E5697425"}],"page":"178-197","date_created":"2018-12-11T11:44:51Z","date_published":"2018-07-18T00:00:00Z","doi":"10.1007/978-3-319-96142-2_13","year":"2018","isi":1,"has_accepted_license":"1","day":"18","oa":1,"quality_controlled":"1","publisher":"Springer","acknowledgement":"Acknowledgements. K. C. and M. H. are partially supported by the Vienna Science and Technology Fund (WWTF) grant ICT15-003. K. C. is partially supported by the Austrian Science Fund (FWF): S11407-N23 (RiSE/SHiNE), and an ERC Start Grant (279307: Graph Games). V. T. is partially supported by the European Union’s Horizon 2020 research and innovation programme under the Marie Sk lodowska-Curie Grant Agreement No. 665385.","department":[{"_id":"KrCh"}],"file_date_updated":"2020-07-14T12:44:53Z","date_updated":"2023-09-19T09:59:55Z","ddc":["000"],"tmp":{"legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","image":"/images/cc_by.png","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","short":"CC BY (4.0)"},"conference":{"start_date":"2018-07-14","location":"Oxford, United Kingdom","end_date":"2018-07-17","name":"CAV: Computer Aided Verification"},"type":"conference","status":"public","_id":"141","ec_funded":1,"volume":10982,"related_material":{"record":[{"status":"public","id":"10199","relation":"dissertation_contains"}]},"publication_status":"published","language":[{"iso":"eng"}],"file":[{"file_name":"2018_LNCS_Chatterjee.pdf","date_created":"2018-12-18T08:52:38Z","creator":"dernst","file_size":675606,"date_updated":"2020-07-14T12:44:53Z","checksum":"1a6ffa4febe8bb8ac28be3adb3eafebc","file_id":"5737","relation":"main_file","access_level":"open_access","content_type":"application/pdf"}],"alternative_title":["LNCS"],"scopus_import":"1","intvolume":" 10982","month":"07","abstract":[{"text":"Given a model and a specification, the fundamental model-checking problem asks for algorithmic verification of whether the model satisfies the specification. We consider graphs and Markov decision processes (MDPs), which are fundamental models for reactive systems. One of the very basic specifications that arise in verification of reactive systems is the strong fairness (aka Streett) objective. Given different types of requests and corresponding grants, the objective requires that for each type, if the request event happens infinitely often, then the corresponding grant event must also happen infinitely often. All ω -regular objectives can be expressed as Streett objectives and hence they are canonical in verification. To handle the state-space explosion, symbolic algorithms are required that operate on a succinct implicit representation of the system rather than explicitly accessing the system. While explicit algorithms for graphs and MDPs with Streett objectives have been widely studied, there has been no improvement of the basic symbolic algorithms. The worst-case numbers of symbolic steps required for the basic symbolic algorithms are as follows: quadratic for graphs and cubic for MDPs. In this work we present the first sub-quadratic symbolic algorithm for graphs with Streett objectives, and our algorithm is sub-quadratic even for MDPs. Based on our algorithmic insights we present an implementation of the new symbolic approach and show that it improves the existing approach on several academic benchmark examples.","lang":"eng"}],"oa_version":"Published Version"}]