[{"department":[{"_id":"GradSch"},{"_id":"ToHe"}],"doi":"10.15479/AT-ISTA-21401","acknowledgement":"This work is part of the project VAMOS, which has received funding from the European\r\nResearch Council (ERC) under grant agreement No. 101020093, and the Austrian Science\r\nFund (FWF) SFB project SpyCoDe F8502.\r\n","supervisor":[{"id":"40876CD8-F248-11E8-B48F-1D18A9856A87","full_name":"Henzinger, Thomas A","last_name":"Henzinger","first_name":"Thomas A","orcid":"0000-0002-2985-7724"}],"publication_identifier":{"issn":["2791-4585"]},"language":[{"iso":"eng"}],"oa_version":"Published Version","has_accepted_license":"1","month":"03","author":[{"id":"6e5417ba-5355-11ee-ae5a-94c2e510b26b","last_name":"Karimi","full_name":"Karimi, Mahyar","first_name":"Mahyar","orcid":"0009-0005-0820-1696"}],"date_published":"2026-03-05T00:00:00Z","alternative_title":["ISTA Master’s Thesis"],"ddc":["000"],"degree_awarded":"MS","OA_place":"repository","date_updated":"2026-03-13T13:37:20Z","project":[{"call_identifier":"H2020","_id":"62781420-2b32-11ec-9570-8d9b63373d4d","name":"Vigilant Algorithmic Monitoring of Software","grant_number":"101020093"},{"grant_number":"F8512","name":"Security and Privacy by Design for Complex Systems","_id":"34a4ce89-11ca-11ed-8bc3-8cc37fb6e11f"}],"related_material":{"record":[{"status":"public","id":"21020","relation":"part_of_dissertation"}]},"user_id":"8b945eb4-e2f2-11eb-945a-df72226e66a9","file_date_updated":"2026-03-10T15:20:09Z","title":"Privacy-preserving runtime verification","ec_funded":1,"corr_author":"1","date_created":"2026-03-05T15:20:47Z","year":"2026","citation":{"ama":"Karimi M. Privacy-preserving runtime verification. 2026. doi:<a href=\"https://doi.org/10.15479/AT-ISTA-21401\">10.15479/AT-ISTA-21401</a>","ista":"Karimi M. 2026. Privacy-preserving runtime verification. Institute of Science and Technology Austria.","apa":"Karimi, M. (2026). <i>Privacy-preserving runtime verification</i>. Institute of Science and Technology Austria. <a href=\"https://doi.org/10.15479/AT-ISTA-21401\">https://doi.org/10.15479/AT-ISTA-21401</a>","chicago":"Karimi, Mahyar. “Privacy-Preserving Runtime Verification.” Institute of Science and Technology Austria, 2026. <a href=\"https://doi.org/10.15479/AT-ISTA-21401\">https://doi.org/10.15479/AT-ISTA-21401</a>.","mla":"Karimi, Mahyar. <i>Privacy-Preserving Runtime Verification</i>. Institute of Science and Technology Austria, 2026, doi:<a href=\"https://doi.org/10.15479/AT-ISTA-21401\">10.15479/AT-ISTA-21401</a>.","ieee":"M. Karimi, “Privacy-preserving runtime verification,” Institute of Science and Technology Austria, 2026.","short":"M. Karimi, Privacy-Preserving Runtime Verification, Institute of Science and Technology Austria, 2026."},"oa":1,"article_processing_charge":"No","publisher":"Institute of Science and Technology Austria","page":"60","keyword":["Privacy-preserving verification","Runtime verification","Monitoring","Reactive functionalities","Cryptographic protocols"],"day":"05","type":"dissertation","publication_status":"published","file":[{"creator":"mkarimi","date_updated":"2026-03-10T15:20:09Z","content_type":"application/pdf","relation":"main_file","date_created":"2026-03-06T14:06:25Z","file_name":"2026_Karimi_Mahyar_Thesis.pdf","file_id":"21404","access_level":"open_access","file_size":766048,"checksum":"3f49f05c9d123e14d7adb73d3bc50fe2"},{"file_id":"21405","access_level":"closed","file_size":1243394,"checksum":"8fb9db4b4187e26443369a993427a5ff","creator":"mkarimi","date_updated":"2026-03-06T14:06:25Z","content_type":"application/zip","relation":"source_file","date_created":"2026-03-06T14:06:25Z","file_name":"2026_Karimi_Mahyar_Thesis_src.zip"}],"_id":"21401","abstract":[{"lang":"eng","text":"Runtime verification offers scalable solutions to improve the safety and reliability of systems. However, systems that require verification or monitoring by a third party to ensure compliance with a specification might contain sensitive information, causing privacy concerns when usual runtime verification approaches are used. Privacy is compromised if protected information about the system, or sensitive data that is processed by the system, is revealed. In addition, revealing the specification being monitored may undermine the essence of third-party verification.\r\n\r\nIn this thesis, we propose a protocol for privacy-preserving runtime verification of systems against formal sequential specifications. We develop the protocol in two steps. In the first step, the monitor verifies whether the system satisfies the specification without learning anything else, though both parties are aware of the specification. In the second step, we extend the protocol to ensure that the system remains oblivious to the monitored specification, while the monitor learns only whether the system satisfies the specification and nothing more. Our protocol adapts and improves existing techniques used in cryptography, and more specifically, multi-party computation.\r\n\r\nThe sequential specification defines the observation step of the monitor, whose granularity depends on the situation (e.g., banks may be monitored on a daily basis). Our protocol exchanges a single message per observation step, after an initialization phase. This design minimizes communication overhead, enabling relatively lightweight privacy-preserving monitoring. We implement our approach for monitoring specifications described by register automata and evaluate it experimentally.\r\n"}],"status":"public"},{"doi":"10.15479/at:ista:11362","publication_identifier":{"isbn":["978-3-99078-017-6"]},"supervisor":[{"last_name":"Henzinger","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","full_name":"Henzinger, Thomas A","orcid":"0000-0002-2985-7724","first_name":"Thomas A"}],"license":"https://creativecommons.org/licenses/by-nd/4.0/","tmp":{"name":"Creative Commons Attribution-NoDerivatives 4.0 International (CC BY-ND 4.0)","legal_code_url":"https://creativecommons.org/licenses/by-nd/4.0/legalcode","short":"CC BY-ND (4.0)","image":"/image/cc_by_nd.png"},"department":[{"_id":"GradSch"},{"_id":"ToHe"}],"ddc":["004"],"alternative_title":["ISTA Thesis"],"date_published":"2022-05-12T00:00:00Z","author":[{"id":"3DC22916-F248-11E8-B48F-1D18A9856A87","full_name":"Lechner, Mathias","last_name":"Lechner","first_name":"Mathias"}],"project":[{"grant_number":"Z211","name":"Formal methods for the design and analysis of complex systems","call_identifier":"FWF","_id":"25F42A32-B435-11E9-9278-68D0E5697425"},{"name":"Vigilant Algorithmic Monitoring of Software","call_identifier":"H2020","_id":"62781420-2b32-11ec-9570-8d9b63373d4d","grant_number":"101020093"}],"date_updated":"2026-04-16T09:46:06Z","degree_awarded":"PhD","OA_place":"publisher","language":[{"iso":"eng"}],"month":"05","has_accepted_license":"1","oa_version":"Published Version","year":"2022","date_created":"2022-05-12T07:14:01Z","corr_author":"1","oa":1,"citation":{"chicago":"Lechner, Mathias. “Learning Verifiable Representations.” Institute of Science and Technology Austria, 2022. <a href=\"https://doi.org/10.15479/at:ista:11362\">https://doi.org/10.15479/at:ista:11362</a>.","apa":"Lechner, M. (2022). <i>Learning verifiable representations</i>. Institute of Science and Technology Austria. <a href=\"https://doi.org/10.15479/at:ista:11362\">https://doi.org/10.15479/at:ista:11362</a>","ista":"Lechner M. 2022. Learning verifiable representations. Institute of Science and Technology Austria.","ama":"Lechner M. Learning verifiable representations. 2022. doi:<a href=\"https://doi.org/10.15479/at:ista:11362\">10.15479/at:ista:11362</a>","short":"M. Lechner, Learning Verifiable Representations, Institute of Science and Technology Austria, 2022.","mla":"Lechner, Mathias. <i>Learning Verifiable Representations</i>. Institute of Science and Technology Austria, 2022, doi:<a href=\"https://doi.org/10.15479/at:ista:11362\">10.15479/at:ista:11362</a>.","ieee":"M. Lechner, “Learning verifiable representations,” Institute of Science and Technology Austria, 2022."},"title":"Learning verifiable representations","ec_funded":1,"file_date_updated":"2022-05-17T15:19:39Z","user_id":"ba8df636-2132-11f1-aed0-ed93e2281fdd","related_material":{"record":[{"status":"public","id":"11366","relation":"part_of_dissertation"},{"id":"10665","relation":"part_of_dissertation","status":"public"},{"status":"public","relation":"part_of_dissertation","id":"10667"},{"status":"public","id":"10666","relation":"part_of_dissertation"},{"status":"public","relation":"part_of_dissertation","id":"7808"}]},"file":[{"date_created":"2022-05-13T12:33:26Z","file_name":"src.zip","content_type":"application/zip","relation":"source_file","date_updated":"2022-05-13T12:49:00Z","creator":"mlechner","checksum":"8eefa9c7c10ca7e1a2ccdd731962a645","file_size":13210143,"access_level":"closed","file_id":"11378"},{"content_type":"application/pdf","relation":"main_file","file_name":"thesis_main-a2.pdf","date_created":"2022-05-16T08:02:28Z","creator":"mlechner","date_updated":"2022-05-17T15:19:39Z","file_size":2732536,"checksum":"1b9e1e5a9a83ed9d89dad2f5133dc026","file_id":"11382","access_level":"open_access"}],"publication_status":"published","status":"public","abstract":[{"lang":"eng","text":"Deep learning has enabled breakthroughs in challenging computing problems and has emerged as the standard problem-solving tool for computer vision and natural language processing tasks.\r\nOne exception to this trend is safety-critical tasks where robustness and resilience requirements contradict the black-box nature of neural networks. \r\nTo deploy deep learning methods for these tasks, it is vital to provide guarantees on neural network agents' safety and robustness criteria. \r\nThis can be achieved by developing formal verification methods to verify the safety and robustness properties of neural networks.\r\n\r\nOur goal is to design, develop and assess safety verification methods for neural networks to improve their reliability and trustworthiness in real-world applications.\r\nThis thesis establishes techniques for the verification of compressed and adversarially trained models as well as the design of novel neural networks for verifiably safe decision-making.\r\n\r\nFirst, we establish the problem of verifying quantized neural networks. Quantization is a technique that trades numerical precision for the computational efficiency of running a neural network and is widely adopted in industry.\r\nWe show that neglecting the reduced precision when verifying a neural network can lead to wrong conclusions about the robustness and safety of the network, highlighting that novel techniques for quantized network verification are necessary. We introduce several bit-exact verification methods explicitly designed for quantized neural networks and experimentally confirm on realistic networks that the network's robustness and other formal properties are affected by the quantization.\r\n\r\nFurthermore, we perform a case study providing evidence that adversarial training, a standard technique for making neural networks more robust, has detrimental effects on the network's performance. This robustness-accuracy tradeoff has been studied before regarding the accuracy obtained on classification datasets where each data point is independent of all other data points. On the other hand, we investigate the tradeoff empirically in robot learning settings where a both, a high accuracy and a high robustness, are desirable.\r\nOur results suggest that the negative side-effects of adversarial training outweigh its robustness benefits in practice.\r\n\r\nFinally, we consider the problem of verifying safety when running a Bayesian neural network policy in a feedback loop with systems over the infinite time horizon. Bayesian neural networks are probabilistic models for learning uncertainties in the data and are therefore often used on robotic and healthcare applications where data is inherently stochastic.\r\nWe introduce a method for recalibrating Bayesian neural networks so that they yield probability distributions over safe decisions only.\r\nOur method learns a safety certificate that guarantees safety over the infinite time horizon to determine which decisions are safe in every possible state of the system.\r\nWe demonstrate the effectiveness of our approach on a series of reinforcement learning benchmarks."}],"_id":"11362","publisher":"Institute of Science and Technology Austria","article_processing_charge":"No","type":"dissertation","day":"12","page":"124","keyword":["neural networks","verification","machine learning"]},{"title":"Symbolic time and space tradeoffs for probabilistic verification","ec_funded":1,"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","oa":1,"citation":{"mla":"Chatterjee, Krishnendu, et al. “Symbolic Time and Space Tradeoffs for Probabilistic Verification.” <i>Proceedings of the 36th Annual ACM/IEEE Symposium on Logic in Computer Science</i>, Institute of Electrical and Electronics Engineers, 2021, pp. 1–13, doi:<a href=\"https://doi.org/10.1109/LICS52264.2021.9470739\">10.1109/LICS52264.2021.9470739</a>.","ieee":"K. Chatterjee, W. Dvorak, M. Henzinger, and A. Svozil, “Symbolic time and space tradeoffs for probabilistic verification,” in <i>Proceedings of the 36th Annual ACM/IEEE Symposium on Logic in Computer Science</i>, Rome, Italy, 2021, pp. 1–13.","short":"K. Chatterjee, W. Dvorak, M. Henzinger, A. Svozil, in:, Proceedings of the 36th Annual ACM/IEEE Symposium on Logic in Computer Science, Institute of Electrical and Electronics Engineers, 2021, pp. 1–13.","chicago":"Chatterjee, Krishnendu, Wolfgang Dvorak, Monika Henzinger, and Alexander Svozil. “Symbolic Time and Space Tradeoffs for Probabilistic Verification.” In <i>Proceedings of the 36th Annual ACM/IEEE Symposium on Logic in Computer Science</i>, 1–13. Institute of Electrical and Electronics Engineers, 2021. <a href=\"https://doi.org/10.1109/LICS52264.2021.9470739\">https://doi.org/10.1109/LICS52264.2021.9470739</a>.","apa":"Chatterjee, K., Dvorak, W., Henzinger, M., &#38; Svozil, A. (2021). Symbolic time and space tradeoffs for probabilistic verification. In <i>Proceedings of the 36th Annual ACM/IEEE Symposium on Logic in Computer Science</i> (pp. 1–13). Rome, Italy: Institute of Electrical and Electronics Engineers. <a href=\"https://doi.org/10.1109/LICS52264.2021.9470739\">https://doi.org/10.1109/LICS52264.2021.9470739</a>","ista":"Chatterjee K, Dvorak W, Henzinger M, Svozil A. 2021. Symbolic time and space tradeoffs for probabilistic verification. Proceedings of the 36th Annual ACM/IEEE Symposium on Logic in Computer Science. LICS: Logic in Computer Science, 1–13.","ama":"Chatterjee K, Dvorak W, Henzinger M, Svozil A. Symbolic time and space tradeoffs for probabilistic verification. In: <i>Proceedings of the 36th Annual ACM/IEEE Symposium on Logic in Computer Science</i>. Institute of Electrical and Electronics Engineers; 2021:1-13. doi:<a href=\"https://doi.org/10.1109/LICS52264.2021.9470739\">10.1109/LICS52264.2021.9470739</a>"},"date_created":"2021-09-12T22:01:24Z","year":"2021","quality_controlled":"1","type":"conference","keyword":["Computer science","Computational modeling","Markov processes","Probabilistic logic","Formal verification","Game Theory"],"day":"07","page":"1-13","publication":"Proceedings of the 36th Annual ACM/IEEE Symposium on Logic in Computer Science","publisher":"Institute of Electrical and Electronics Engineers","article_processing_charge":"No","_id":"10002","abstract":[{"text":"We present a faster symbolic algorithm for the following central problem in probabilistic verification: Compute the maximal end-component (MEC) decomposition of Markov decision processes (MDPs). This problem generalizes the SCC decomposition problem of graphs and closed recurrent sets of Markov chains. The model of symbolic algorithms is widely used in formal verification and model-checking, where access to the input model is restricted to only symbolic operations (e.g., basic set operations and computation of one-step neighborhood). For an input MDP with  n  vertices and  m  edges, the classical symbolic algorithm from the 1990s for the MEC decomposition requires  O(n2)  symbolic operations and  O(1)  symbolic space. The only other symbolic algorithm for the MEC decomposition requires  O(nm−−√)  symbolic operations and  O(m−−√)  symbolic space. A main open question is whether the worst-case  O(n2)  bound for symbolic operations can be beaten. We present a symbolic algorithm that requires  O˜(n1.5)  symbolic operations and  O˜(n−−√)  symbolic space. Moreover, the parametrization of our algorithm provides a trade-off between symbolic operations and symbolic space: for all  0<ϵ≤1/2  the symbolic algorithm requires  O˜(n2−ϵ)  symbolic operations and  O˜(nϵ)  symbolic space ( O˜  hides poly-logarithmic factors). Using our techniques we present faster algorithms for computing the almost-sure winning regions of  ω -regular objectives for MDPs. We consider the canonical parity objectives for  ω -regular objectives, and for parity objectives with  d -priorities we present an algorithm that computes the almost-sure winning region with  O˜(n2−ϵ)  symbolic operations and  O˜(nϵ)  symbolic space, for all  0<ϵ≤1/2 .","lang":"eng"}],"status":"public","main_file_link":[{"open_access":"1","url":"https://arxiv.org/abs/2104.07466"}],"arxiv":1,"publication_status":"published","isi":1,"department":[{"_id":"KrCh"}],"publication_identifier":{"eisbn":["978-1-6654-4895-6"],"issn":["1043-6871"],"isbn":["978-1-6654-4896-3"]},"acknowledgement":"The authors are grateful to the anonymous referees for their valuable comments. A. S. is fully supported by the Vienna Science and Technology Fund (WWTF) through project ICT15–003. K. C. is supported by the Austrian Science Fund (FWF) NFN Grant No S11407-N23 (RiSE/SHiNE) and by the ERC CoG 863818 (ForM-SMArt). For M. H. the research leading to these results has received funding from the European Research Council under the European Unions Seventh Framework Programme (FP/2007–2013) / ERC Grant Agreement no. 340506.","doi":"10.1109/LICS52264.2021.9470739","month":"07","scopus_import":"1","oa_version":"Preprint","language":[{"iso":"eng"}],"conference":{"end_date":"2021-07-02","start_date":"2021-06-29","location":"Rome, Italy","name":"LICS: Logic in Computer Science"},"external_id":{"arxiv":["2104.07466"],"isi":["000947350400089"]},"project":[{"call_identifier":"FWF","_id":"25863FF4-B435-11E9-9278-68D0E5697425","name":"Game Theory","grant_number":"S11407"},{"grant_number":"863818","call_identifier":"H2020","_id":"0599E47C-7A3F-11EA-A408-12923DDC885E","name":"Formal Methods for Stochastic Models: Algorithms and Applications"}],"date_updated":"2025-07-10T11:15:45Z","date_published":"2021-07-07T00:00:00Z","author":[{"first_name":"Krishnendu","orcid":"0000-0002-4561-241X","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","full_name":"Chatterjee, Krishnendu","last_name":"Chatterjee"},{"full_name":"Dvorak, Wolfgang","last_name":"Dvorak","first_name":"Wolfgang"},{"id":"540c9bbd-f2de-11ec-812d-d04a5be85630","full_name":"Henzinger, Monika H","last_name":"Henzinger","orcid":"0000-0002-5008-6530","first_name":"Monika H"},{"first_name":"Alexander","full_name":"Svozil, Alexander","last_name":"Svozil"}]},{"intvolume":"     12974","_id":"10108","abstract":[{"lang":"eng","text":"We argue that the time is ripe to investigate differential monitoring, in which the specification of a program's behavior is implicitly given by a second program implementing the same informal specification. Similar ideas have been proposed before, and are currently implemented in restricted form for testing and specialized run-time analyses, aspects of which we combine. We discuss the challenges of implementing differential monitoring as a general-purpose, black-box run-time monitoring framework, and present promising results of a preliminary implementation, showing low monitoring overheads for diverse programs."}],"status":"public","publication_status":"published","file":[{"content_type":"application/pdf","relation":"main_file","file_name":"differentialmonitoring-cameraready-openaccess.pdf","date_created":"2021-10-07T23:32:18Z","success":1,"creator":"fmuehlbo","date_updated":"2021-10-07T23:32:18Z","file_size":350632,"checksum":"554c7fdb259eda703a8b6328a6dad55a","file_id":"10109","access_level":"open_access"}],"type":"conference","volume":12974,"keyword":["run-time verification","software engineering","implicit specification"],"page":"231-243","day":"06","publication":"International Conference on Runtime Verification","publisher":"Springer Nature","article_processing_charge":"No","oa":1,"citation":{"mla":"Mühlböck, Fabian, and Thomas A. Henzinger. “Differential Monitoring.” <i>International Conference on Runtime Verification</i>, vol. 12974, Springer Nature, 2021, pp. 231–43, doi:<a href=\"https://doi.org/10.1007/978-3-030-88494-9_12\">10.1007/978-3-030-88494-9_12</a>.","ieee":"F. Mühlböck and T. A. Henzinger, “Differential monitoring,” in <i>International Conference on Runtime Verification</i>, Virtual, 2021, vol. 12974, pp. 231–243.","short":"F. Mühlböck, T.A. Henzinger, in:, International Conference on Runtime Verification, Springer Nature, Cham, 2021, pp. 231–243.","chicago":"Mühlböck, Fabian, and Thomas A Henzinger. “Differential Monitoring.” In <i>International Conference on Runtime Verification</i>, 12974:231–43. Cham: Springer Nature, 2021. <a href=\"https://doi.org/10.1007/978-3-030-88494-9_12\">https://doi.org/10.1007/978-3-030-88494-9_12</a>.","apa":"Mühlböck, F., &#38; Henzinger, T. A. (2021). Differential monitoring. In <i>International Conference on Runtime Verification</i> (Vol. 12974, pp. 231–243). Cham: Springer Nature. <a href=\"https://doi.org/10.1007/978-3-030-88494-9_12\">https://doi.org/10.1007/978-3-030-88494-9_12</a>","ista":"Mühlböck F, Henzinger TA. 2021. Differential monitoring. International Conference on Runtime Verification. RV: Runtime Verification, LNCS, vol. 12974, 231–243.","ama":"Mühlböck F, Henzinger TA. Differential monitoring. In: <i>International Conference on Runtime Verification</i>. Vol 12974. Cham: Springer Nature; 2021:231-243. doi:<a href=\"https://doi.org/10.1007/978-3-030-88494-9_12\">10.1007/978-3-030-88494-9_12</a>"},"date_created":"2021-10-07T23:30:10Z","year":"2021","quality_controlled":"1","corr_author":"1","file_date_updated":"2021-10-07T23:32:18Z","title":"Differential monitoring","related_material":{"record":[{"id":"9946","relation":"extended_version","status":"public"}]},"user_id":"4359f0d1-fa6c-11eb-b949-802e58b17ae8","date_updated":"2025-04-15T06:26:12Z","project":[{"grant_number":"Z211","call_identifier":"FWF","_id":"25F42A32-B435-11E9-9278-68D0E5697425","name":"Formal methods for the design and analysis of complex systems"}],"date_published":"2021-10-06T00:00:00Z","ddc":["005"],"alternative_title":["LNCS"],"place":"Cham","author":[{"last_name":"Mühlböck","id":"6395C5F6-89DF-11E9-9C97-6BDFE5697425","full_name":"Mühlböck, Fabian","orcid":"0000-0003-1548-0177","first_name":"Fabian"},{"first_name":"Thomas A","orcid":"0000-0002-2985-7724","full_name":"Henzinger, Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","last_name":"Henzinger"}],"month":"10","scopus_import":"1","oa_version":"Preprint","has_accepted_license":"1","language":[{"iso":"eng"}],"conference":{"end_date":"2021-10-14","start_date":"2021-10-11","location":"Virtual","name":"RV: Runtime Verification"},"external_id":{"isi":["000719383800012"]},"publication_identifier":{"isbn":["978-3-030-88493-2"],"eissn":["1611-3349"],"issn":["0302-9743"],"eisbn":["978-3-030-88494-9"]},"acknowledgement":"The authors would like to thank Borzoo Bonakdarpour, Derek Dreyer, Adrian Francalanza, Owolabi Legunsen, Mae Milano, Manuel Rigger, Cesar Sanchez, and the members of the IST Verification Seminar for their helpful comments and insights on various stages of this work, as well as the reviewers of RV’21 for their helpful suggestions on the actual paper.","doi":"10.1007/978-3-030-88494-9_12","isi":1,"department":[{"_id":"ToHe"}]},{"file_date_updated":"2021-09-03T12:34:28Z","title":"Differential monitoring","related_material":{"record":[{"relation":"shorter_version","id":"10108","status":"public"},{"status":"public","relation":"other","id":"9281"}]},"user_id":"8b945eb4-e2f2-11eb-945a-df72226e66a9","date_created":"2021-08-20T20:00:37Z","year":"2021","oa":1,"citation":{"short":"F. Mühlböck, T.A. Henzinger, Differential Monitoring, IST Austria, 2021.","mla":"Mühlböck, Fabian, and Thomas A. Henzinger. <i>Differential Monitoring</i>. IST Austria, 2021, doi:<a href=\"https://doi.org/10.15479/AT:ISTA:9946\">10.15479/AT:ISTA:9946</a>.","ieee":"F. Mühlböck and T. A. Henzinger, <i>Differential monitoring</i>. IST Austria, 2021.","ista":"Mühlböck F, Henzinger TA. 2021. Differential monitoring, IST Austria, 17p.","ama":"Mühlböck F, Henzinger TA. <i>Differential Monitoring</i>. IST Austria; 2021. doi:<a href=\"https://doi.org/10.15479/AT:ISTA:9946\">10.15479/AT:ISTA:9946</a>","chicago":"Mühlböck, Fabian, and Thomas A Henzinger. <i>Differential Monitoring</i>. IST Austria, 2021. <a href=\"https://doi.org/10.15479/AT:ISTA:9946\">https://doi.org/10.15479/AT:ISTA:9946</a>.","apa":"Mühlböck, F., &#38; Henzinger, T. A. (2021). <i>Differential monitoring</i>. IST Austria. <a href=\"https://doi.org/10.15479/AT:ISTA:9946\">https://doi.org/10.15479/AT:ISTA:9946</a>"},"publisher":"IST Austria","article_processing_charge":"No","type":"technical_report","keyword":["run-time verification","software engineering","implicit specification"],"day":"01","page":"17","publication_status":"published","file":[{"file_id":"9948","access_level":"open_access","checksum":"0f9aafd59444cb6bdca6925d163ab946","file_size":"320453","creator":"fmuehlbo","date_updated":"2021-09-03T12:34:28Z","relation":"main_file","content_type":"application/pdf","date_created":"2021-08-20T19:59:44Z","file_name":"differentialmonitoring-techreport.pdf"}],"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"}],"_id":"9946","status":"public","department":[{"_id":"ToHe"}],"doi":"10.15479/AT:ISTA:9946","publication_identifier":{"issn":["2664-1690"]},"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.","language":[{"iso":"eng"}],"month":"09","oa_version":"Published Version","has_accepted_license":"1","date_published":"2021-09-01T00:00:00Z","ddc":["005"],"alternative_title":["IST Austria Technical Report"],"author":[{"first_name":"Fabian","orcid":"0000-0003-1548-0177","full_name":"Mühlböck, Fabian","id":"6395C5F6-89DF-11E9-9C97-6BDFE5697425","last_name":"Mühlböck"},{"last_name":"Henzinger","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","full_name":"Henzinger, Thomas A","first_name":"Thomas A","orcid":"0000-0002-2985-7724"}],"date_updated":"2025-04-15T06:55:00Z","project":[{"grant_number":"Z211","name":"Formal methods for the design and analysis of complex systems","call_identifier":"FWF","_id":"25F42A32-B435-11E9-9278-68D0E5697425"}]},{"file":[{"date_updated":"2021-11-08T14:12:22Z","creator":"vtoman","date_created":"2021-11-08T14:12:22Z","file_name":"toman_th_final.pdf","relation":"main_file","content_type":"application/pdf","access_level":"open_access","file_id":"10225","file_size":2915234,"checksum":"4f412a1ee60952221b499a4b1268df35"},{"file_size":8616056,"checksum":"9584943f99127be2dd2963f6784c37d4","file_id":"10226","access_level":"closed","relation":"source_file","content_type":"application/zip","file_name":"toman_thesis.zip","date_created":"2021-11-08T14:12:46Z","creator":"vtoman","date_updated":"2021-11-09T09:00:50Z"}],"publication_status":"published","status":"public","abstract":[{"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.","lang":"eng"}],"_id":"10199","article_processing_charge":"No","publisher":"Institute of Science and Technology Austria","page":"166","keyword":["concurrency","verification","model checking"],"day":"31","type":"dissertation","corr_author":"1","year":"2021","date_created":"2021-10-29T20:09:01Z","citation":{"ieee":"V. Toman, “Improved verification techniques for concurrent systems,” Institute of Science and Technology Austria, 2021.","mla":"Toman, Viktor. <i>Improved Verification Techniques for Concurrent Systems</i>. Institute of Science and Technology Austria, 2021, doi:<a href=\"https://doi.org/10.15479/at:ista:10199\">10.15479/at:ista:10199</a>.","short":"V. Toman, Improved Verification Techniques for Concurrent Systems, Institute of Science and Technology Austria, 2021.","chicago":"Toman, Viktor. “Improved Verification Techniques for Concurrent Systems.” Institute of Science and Technology Austria, 2021. <a href=\"https://doi.org/10.15479/at:ista:10199\">https://doi.org/10.15479/at:ista:10199</a>.","apa":"Toman, V. (2021). <i>Improved verification techniques for concurrent systems</i>. Institute of Science and Technology Austria. <a href=\"https://doi.org/10.15479/at:ista:10199\">https://doi.org/10.15479/at:ista:10199</a>","ista":"Toman V. 2021. Improved verification techniques for concurrent systems. Institute of Science and Technology Austria.","ama":"Toman V. Improved verification techniques for concurrent systems. 2021. doi:<a href=\"https://doi.org/10.15479/at:ista:10199\">10.15479/at:ista:10199</a>"},"oa":1,"user_id":"ba8df636-2132-11f1-aed0-ed93e2281fdd","related_material":{"record":[{"id":"9987","relation":"part_of_dissertation","status":"public"},{"relation":"part_of_dissertation","id":"10191","status":"public"},{"status":"public","relation":"part_of_dissertation","id":"141"},{"status":"public","id":"10190","relation":"part_of_dissertation"}]},"title":"Improved verification techniques for concurrent systems","ec_funded":1,"file_date_updated":"2021-11-09T09:00:50Z","author":[{"id":"3AF3DA7C-F248-11E8-B48F-1D18A9856A87","full_name":"Toman, Viktor","last_name":"Toman","first_name":"Viktor","orcid":"0000-0001-9036-063X"}],"alternative_title":["ISTA Thesis"],"ddc":["000"],"date_published":"2021-10-31T00:00:00Z","date_updated":"2026-04-08T07:00:31Z","project":[{"grant_number":"665385","_id":"2564DBCA-B435-11E9-9278-68D0E5697425","call_identifier":"H2020","name":"International IST Doctoral Program"},{"call_identifier":"FWF","_id":"25F2ACDE-B435-11E9-9278-68D0E5697425","name":"Rigorous Systems Engineering","grant_number":"S11402-N23"},{"_id":"25892FC0-B435-11E9-9278-68D0E5697425","name":"Efficient Algorithms for Computer Aided Verification","grant_number":"ICT15-003"},{"name":"Formal Methods for Stochastic Models: Algorithms and Applications","call_identifier":"H2020","_id":"0599E47C-7A3F-11EA-A408-12923DDC885E","grant_number":"863818"}],"OA_place":"publisher","degree_awarded":"PhD","acknowledged_ssus":[{"_id":"SSU"}],"language":[{"iso":"eng"}],"has_accepted_license":"1","oa_version":"Published Version","month":"10","doi":"10.15479/at:ista:10199","publication_identifier":{"issn":["2663-337X"]},"supervisor":[{"first_name":"Krishnendu","orcid":"0000-0002-4561-241X","full_name":"Chatterjee, Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","last_name":"Chatterjee"}],"department":[{"_id":"GradSch"},{"_id":"KrCh"}]},{"license":"https://creativecommons.org/publicdomain/zero/1.0/","doi":"10.15479/AT:ISTA:28","department":[{"_id":"KrCh"},{"_id":"ToHe"}],"tmp":{"short":"CC0 (1.0)","name":"Creative Commons Public Domain Dedication (CC0 1.0)","legal_code_url":"https://creativecommons.org/publicdomain/zero/1.0/legalcode","image":"/images/cc_0.png"},"datarep_id":"28","date_updated":"2025-09-23T08:23:15Z","project":[{"grant_number":"279307","name":"Quantitative Graph Games: Theory and Applications","call_identifier":"FP7","_id":"2581B60A-B435-11E9-9278-68D0E5697425"},{"grant_number":"S 11407_N23","_id":"25832EC2-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","name":"Rigorous Systems Engineering"}],"author":[{"id":"42BABFB4-F248-11E8-B48F-1D18A9856A87","full_name":"Fellner, Andreas","last_name":"Fellner","first_name":"Andreas"}],"ddc":["004"],"date_published":"2015-08-13T00:00:00Z","has_accepted_license":"1","oa_version":"Published Version","month":"08","citation":{"chicago":"Fellner, Andreas. “Experimental Part of CAV 2015 Publication: Counterexample Explanation by Learning Small Strategies in Markov Decision Processes.” Institute of Science and Technology Austria, 2015. <a href=\"https://doi.org/10.15479/AT:ISTA:28\">https://doi.org/10.15479/AT:ISTA:28</a>.","apa":"Fellner, A. (2015). Experimental part of CAV 2015 publication: Counterexample Explanation by Learning Small Strategies in Markov Decision Processes. Institute of Science and Technology Austria. <a href=\"https://doi.org/10.15479/AT:ISTA:28\">https://doi.org/10.15479/AT:ISTA:28</a>","ista":"Fellner A. 2015. Experimental part of CAV 2015 publication: Counterexample Explanation by Learning Small Strategies in Markov Decision Processes, Institute of Science and Technology Austria, <a href=\"https://doi.org/10.15479/AT:ISTA:28\">10.15479/AT:ISTA:28</a>.","ama":"Fellner A. Experimental part of CAV 2015 publication: Counterexample Explanation by Learning Small Strategies in Markov Decision Processes. 2015. doi:<a href=\"https://doi.org/10.15479/AT:ISTA:28\">10.15479/AT:ISTA:28</a>","mla":"Fellner, Andreas. <i>Experimental Part of CAV 2015 Publication: Counterexample Explanation by Learning Small Strategies in Markov Decision Processes</i>. Institute of Science and Technology Austria, 2015, doi:<a href=\"https://doi.org/10.15479/AT:ISTA:28\">10.15479/AT:ISTA:28</a>.","ieee":"A. Fellner, “Experimental part of CAV 2015 publication: Counterexample Explanation by Learning Small Strategies in Markov Decision Processes.” Institute of Science and Technology Austria, 2015.","short":"A. Fellner, (2015)."},"oa":1,"year":"2015","date_created":"2018-12-12T12:31:29Z","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","related_material":{"record":[{"id":"1603","relation":"popular_science","status":"public"}]},"title":"Experimental part of CAV 2015 publication: Counterexample Explanation by Learning Small Strategies in Markov Decision Processes","ec_funded":1,"file_date_updated":"2020-07-14T12:47:00Z","publist_id":"5564","status":"public","_id":"5549","abstract":[{"lang":"eng","text":"This repository contains the experimental part of the CAV 2015 publication Counterexample Explanation by Learning Small Strategies in Markov Decision Processes.\r\nWe extended the probabilistic model checker PRISM to represent strategies of Markov Decision Processes as Decision Trees.\r\nThe archive contains a java executable version of the extended tool (prism_dectree.jar) together with a few examples of the PRISM benchmark library.\r\nTo execute the program, please have a look at the README.txt, which provides instructions and further information on the archive.\r\nThe archive contains scripts that (if run often enough) reproduces the data presented in the publication."}],"file":[{"checksum":"b8bcb43c0893023cda66c1b69c16ac62","file_size":49557109,"file_id":"5597","access_level":"open_access","relation":"main_file","content_type":"application/zip","file_name":"IST-2015-28-v1+2_Fellner_DataRep.zip","date_created":"2018-12-12T13:02:31Z","creator":"system","date_updated":"2020-07-14T12:47:00Z"}],"keyword":["Markov Decision Process","Decision Tree","Probabilistic Verification","Counterexample Explanation"],"day":"13","type":"research_data","contributor":[{"id":"44CEF464-F248-11E8-B48F-1D18A9856A87","last_name":"Kretinsky","first_name":"Jan"}],"article_processing_charge":"No","publisher":"Institute of Science and Technology Austria"}]