var bibbase_data = {"data":"\"Loading..\"\n\n
\n\n \n\n \n\n \n \n\n \n\n \n \n\n \n\n \n
\n generated by\n \n \"bibbase.org\"\n\n \n
\n \n\n
\n\n \n\n\n
\n\n Excellent! Next you can\n create a new website with this list, or\n embed it in an existing web page by copying & pasting\n any of the following snippets.\n\n
\n JavaScript\n (easiest)\n
\n \n <script src=\"https://bibbase.org/show?bib=https://hajduakos.github.io%2Fpublications.bib&jsonp=1&theme=side&jsonp=1\"></script>\n \n
\n\n PHP\n
\n \n <?php\n $contents = file_get_contents(\"https://bibbase.org/show?bib=https://hajduakos.github.io%2Fpublications.bib&jsonp=1&theme=side\");\n print_r($contents);\n ?>\n \n
\n\n iFrame\n (not recommended)\n
\n \n <iframe src=\"https://bibbase.org/show?bib=https://hajduakos.github.io%2Fpublications.bib&jsonp=1&theme=side\"></iframe>\n \n
\n\n

\n For more details see the documention.\n

\n
\n
\n\n
\n\n This is a preview! To use this list on your own web site\n or create a new web site from it,\n create a free account. The file will be added\n and you will be able to edit it in the File Manager.\n We will show you instructions once you've created your account.\n
\n\n
\n\n

To the site owner:

\n\n

Action required! Mendeley is changing its\n API. In order to keep using Mendeley with BibBase past April\n 14th, you need to:\n

    \n
  1. renew the authorization for BibBase on Mendeley, and
  2. \n
  3. update the BibBase URL\n in your page the same way you did when you initially set up\n this page.\n
  4. \n
\n

\n\n

\n \n \n Fix it now\n

\n
\n\n
\n\n\n
\n \n \n
\n
\n  \n 2024\n \n \n (2)\n \n \n
\n
\n \n \n
\n \n\n \n \n \n \n \n \n PrivacyCAT: Privacy-Aware Code Analysis at Scale.\n \n \n \n \n\n\n \n Mao, K.; Åhs, C. T; Cela, S.; Distefano, D.; Gardner, N.; Grigore, R.; Gustafsson, P.; Hajdu, Á.; Kapus, T.; Marescotti, M.; Cunha Sampaio, G.; and Suzanne, T.\n\n\n \n\n\n\n In Proceedings of the IEEE/ACM 46th International Conference on Software Engineering: Software Engineering in Practice, 2024. \n (Accepted)\n\n\n\n
\n\n\n\n \n \n \"PrivacyCAT: pdf\n  \n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n  \n \n abstract \n \n\n \n  \n \n 3 downloads\n \n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{icse2024,\n    author    = {Mao, Ke and {\\AA}hs, Cons T and Cela, Sopot and Distefano, Dino and Gardner, Nick and Grigore, Radu and Gustafsson, Per and Hajdu, \\'Akos and Kapus, Timotej and Marescotti, Matteo and Cunha Sampaio, Gabriela and Suzanne, Thibault},\n    title     = {{P}rivacy{CAT}: Privacy-Aware Code Analysis at Scale},\n    year      = {2024},\n    booktitle = {Proceedings of the IEEE/ACM 46th International Conference on Software Engineering: Software Engineering in Practice},\n    note      = {(Accepted)},\n\n    type      = {Conference},\n\n    url_pdf   = {https://hajduakos.github.io/publications/icse2024.pdf},\n    abstract  = {Static and dynamic code analyses have been widely adopted in industry to enhance software reliability, security, and performance by automatically detecting bugs in the code. In this paper, we introduce PrivacyCAT, a code analysis system developed and deployed at WhatsApp to protect user privacy. PrivacyCAT automatically detects privacy defects in code at early stages (before reaching production and affecting users), and therefore, it prevents such vulnerabilities from evolving into privacy incidents. PrivacyCAT comprises of a collection of static and dynamic taint analysers. We report on the technical development of PrivacyCAT and the results of two years of its large-scale industrial deployment at WhatsApp. We present our experience in designing its system architecture, and continuous integration process. We discuss the unique challenges encountered in developing and deploying such kind of analyses within an industrial context. Since its deployment in 2021, PrivacyCAT has safeguarded data privacy in $74\\%$ of privacy site events (SEVs). It has prevented 493 potential privacy SEVs from being introduced into the codebases, enabling developers to maintain a high privacy standard for the code that supports over two billion WhatsApp users.},\n}\n\n
\n
\n\n\n
\n Static and dynamic code analyses have been widely adopted in industry to enhance software reliability, security, and performance by automatically detecting bugs in the code. In this paper, we introduce PrivacyCAT, a code analysis system developed and deployed at WhatsApp to protect user privacy. PrivacyCAT automatically detects privacy defects in code at early stages (before reaching production and affecting users), and therefore, it prevents such vulnerabilities from evolving into privacy incidents. PrivacyCAT comprises of a collection of static and dynamic taint analysers. We report on the technical development of PrivacyCAT and the results of two years of its large-scale industrial deployment at WhatsApp. We present our experience in designing its system architecture, and continuous integration process. We discuss the unique challenges encountered in developing and deploying such kind of analyses within an industrial context. Since its deployment in 2021, PrivacyCAT has safeguarded data privacy in $74%$ of privacy site events (SEVs). It has prevented 493 potential privacy SEVs from being introduced into the codebases, enabling developers to maintain a high privacy standard for the code that supports over two billion WhatsApp users.\n
\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n Automated End-to-End Dynamic Taint Analysis for WhatsApp.\n \n \n \n \n\n\n \n Cela, S.; Ciancone, A.; Gustafsson, P.; Hajdu, Á.; Jia, Y.; Kapus, T.; Koshtenko, M.; Lewis, W.; Mao, K.; and Martac, D.\n\n\n \n\n\n\n In Companion Proceedings of the 32nd ACM Symposium on the Foundations of Software Engineering, 2024. ACM\n (Accepted)\n\n\n\n
\n\n\n\n \n \n \"Automated pdf\n  \n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n  \n \n abstract \n \n\n \n  \n \n 2 downloads\n \n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{fse2024,\n    author    = {Cela, Sopot and Ciancone, Andrea and Gustafsson, Per and Hajdu, {\\'A}kos and Jia, Yue and Kapus, Timotej and Koshtenko, Maksym and Lewis, Will and Mao, Ke and Martac, Dragos},\n    title     = {Automated End-to-End Dynamic Taint Analysis for {W}hats{A}pp},\n    year      = {2024},\n    publisher = {ACM},\n    booktitle = {Companion Proceedings of the 32nd ACM Symposium on the Foundations of Software Engineering},\n    note      = {(Accepted)},\n\n    type      = {Conference},\n\n    url_pdf    = {https://hajduakos.github.io/publications/fse2024.pdf},\n    abstract  = {Taint analysis aims to track data flows in systems, with potential use cases for security, privacy and performance. This paper describes an end-to-end dynamic taint analysis solution for WhatsApp. We use exploratory UI testing to generate realistic interactions and inputs, serving as data sources on the clients and then we track data propagation towards sinks on both client and server sides. Finally, a reporting pipeline localizes tainted flows in the source code, applies deduplication, filters false positives based on production call sites, and files tasks to code owners. Applied to WhatsApp, our approach found 89 flows that were fixed by engineers, and caught 50% of all privacy-related flows that required escalation, including instances that would have been difficult to uncover by conventional testing.},\n}\n
\n
\n\n\n
\n Taint analysis aims to track data flows in systems, with potential use cases for security, privacy and performance. This paper describes an end-to-end dynamic taint analysis solution for WhatsApp. We use exploratory UI testing to generate realistic interactions and inputs, serving as data sources on the clients and then we track data propagation towards sinks on both client and server sides. Finally, a reporting pipeline localizes tainted flows in the source code, applies deduplication, filters false positives based on production call sites, and files tasks to code owners. Applied to WhatsApp, our approach found 89 flows that were fixed by engineers, and caught 50% of all privacy-related flows that required escalation, including instances that would have been difficult to uncover by conventional testing.\n
\n\n\n
\n\n\n\n\n\n
\n
\n\n
\n
\n  \n 2023\n \n \n (1)\n \n \n
\n
\n \n \n
\n \n\n \n \n \n \n \n \n Pragmatic verification and validation of industrial executable SysML models.\n \n \n \n \n\n\n \n Horváth, B.; Molnár, V.; Graics, B.; Hajdu, Á.; Ráth, I.; Horváth, Á.; Karban, R.; Trancho, G.; and Micskei, Z.\n\n\n \n\n\n\n Systems Engineering, 26(6): 693–714. 2023.\n \n\n\n\n
\n\n\n\n \n \n \"Pragmatic pdf\n  \n \n \n \"Pragmatic link\n  \n \n\n \n \n doi\n  \n \n\n \n link\n  \n \n\n bibtex\n \n\n \n  \n \n abstract \n \n\n \n  \n \n 4 downloads\n \n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@article{syseng2023,\n    author   = {Horv{\\'a}th, Benedek and Moln{\\'a}r, Vince and Graics, Bence and Hajdu, {\\'A}kos and R{\\'a}th, Istv{\\'a}n and Horv{\\'a}th, {\\'A}kos and Karban, Robert and Trancho, Gelys and Micskei, Zolt{\\'a}n},\n    title    = {Pragmatic verification and validation of industrial executable {SysML} models},\n    year     = {2023},\n    journal  = {Systems Engineering},\n    doi      = {10.1002/sys.21679},\n    volume   = {26},\n    number   = {6},\n    pages    = {693--714},\n\n    type     = {Journal},\n\n    url_pdf  = {https://hajduakos.github.io/publications/syseng2023.pdf},\n    url_link = {https://incose.onlinelibrary.wiley.com/doi/10.1002/sys.21679},\n\n    abstract = {In recent years, Model-Based Systems Engineering (MBSE) practices have been applied in various industries to design, simulate and verify complex systems. The verification and validation (V&V) of such systems engineering models are crucial to develop high-quality systems. However, this is a challenging problem due to the complexity of the models and semantic differences in how different tools interpret the models, which can undermine the validity of the obtained results if they go undiscovered. To address these issues, we propose (i) a subset of the SysML language for which the practical semantic integrity of tools can be achieved and (ii) a cloud-based V&V framework for this subset, lifting verification to an industrial scale. We demonstrate the feasibility of our approach on an industrial-scale model from the aerospace domain and summarize the lessons learned during transitioning formal verification tools to an industrial context.},\n}\n\n
\n
\n\n\n
\n In recent years, Model-Based Systems Engineering (MBSE) practices have been applied in various industries to design, simulate and verify complex systems. The verification and validation (V&V) of such systems engineering models are crucial to develop high-quality systems. However, this is a challenging problem due to the complexity of the models and semantic differences in how different tools interpret the models, which can undermine the validity of the obtained results if they go undiscovered. To address these issues, we propose (i) a subset of the SysML language for which the practical semantic integrity of tools can be achieved and (ii) a cloud-based V&V framework for this subset, lifting verification to an industrial scale. We demonstrate the feasibility of our approach on an industrial-scale model from the aerospace domain and summarize the lessons learned during transitioning formal verification tools to an industrial context.\n
\n\n\n
\n\n\n\n\n\n
\n
\n\n
\n
\n  \n 2022\n \n \n (3)\n \n \n
\n
\n \n \n
\n \n\n \n \n \n \n \n \n FAUSTA: Scaling Dynamic Analysis with Traffic Generation at WhatsApp.\n \n \n \n \n\n\n \n Mao, K.; Kapus, T.; Petrou, L.; Hajdu, Á.; Marescotti, M.; Löscher, A.; Harman, M.; and Distefano, D.\n\n\n \n\n\n\n In Proceedings of the 15th IEEE International Conference on Software Testing, Verification and Validation, pages 267–278, 2022. IEEE\n \n\n\n\n
\n\n\n\n \n \n \"FAUSTA: pdf\n  \n \n \n \"FAUSTA: link\n  \n \n\n \n \n doi\n  \n \n\n \n link\n  \n \n\n bibtex\n \n\n \n  \n \n abstract \n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{icst2022,\n    author     = {Ke Mao and Timotej Kapus and Lambros Petrou and {\\'A}kos Hajdu and Matteo Marescotti and Andreas L{\\"o}scher and Mark Harman and Dino Distefano},\n    title      = {{FAUSTA}: Scaling Dynamic Analysis with Traffic Generation at {W}hats{A}pp},\n    booktitle  = {Proceedings of the 15th IEEE International Conference on Software Testing, Verification and Validation},\n    year       = {2022},\n    publisher  = {IEEE},\n    pages      = {267--278},\n    doi        = {10.1109/ICST53961.2022.00036},\n\n    type       = {Conference},\n\n    url_pdf    = {https://hajduakos.github.io/publications/icst2022.pdf},\n    url_link   = {https://ieeexplore.ieee.org/document/9787859},\n    abstract   = {We introduce Fausta, an algorithmic traffic gener-ation platform that enables analysis and testing at scale. Fausta has been deployed at Meta to analyze and test the WhatsApp plat-form infrastructure since September 2020, enabling WhatsApp developers to deploy reliable code changes to a code base of millions of lines of code, supporting over 2 billion users who rely on WhatsApp for their daily communications. Fausta covers expected and unexpected program behaviors in a privacy-safe controlled environment to support multiple use cases such as reliability testing, privacy analysis and performance regression detection. It currently supports three different algorithmic input generation strategies, each of which construct realistic backend server traffic that closely simulates production data, without replaying any real user data. Fausta has been deployed and closely integrated into the WhatsApp continuous integration process, catching bugs in development before they hit production. We report on the development and deployment of Fausta's reliability use case between September 2020 and August 2021. During this period it has found 1,876 unique reliability issues, with a fix rate of 74%, indicating a high degree of true positive fault revelation. We also report on the distribution of fault types revealed by Fausta, and the correlation between coverage and faults found. Overall, we do find evidence that higher coverage is correlated with fault revelation.},\n}\n\n
\n
\n\n\n
\n We introduce Fausta, an algorithmic traffic gener-ation platform that enables analysis and testing at scale. Fausta has been deployed at Meta to analyze and test the WhatsApp plat-form infrastructure since September 2020, enabling WhatsApp developers to deploy reliable code changes to a code base of millions of lines of code, supporting over 2 billion users who rely on WhatsApp for their daily communications. Fausta covers expected and unexpected program behaviors in a privacy-safe controlled environment to support multiple use cases such as reliability testing, privacy analysis and performance regression detection. It currently supports three different algorithmic input generation strategies, each of which construct realistic backend server traffic that closely simulates production data, without replaying any real user data. Fausta has been deployed and closely integrated into the WhatsApp continuous integration process, catching bugs in development before they hit production. We report on the development and deployment of Fausta's reliability use case between September 2020 and August 2021. During this period it has found 1,876 unique reliability issues, with a fix rate of 74%, indicating a high degree of true positive fault revelation. We also report on the distribution of fault types revealed by Fausta, and the correlation between coverage and faults found. Overall, we do find evidence that higher coverage is correlated with fault revelation.\n
\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n Theta: portfolio of CEGAR-based analyses with dynamic algorithm selection (Competition Contribution).\n \n \n \n \n\n\n \n Ádam, Z.; Levente, B.; Dobos-Kovács, M.; Hajdu, Á.; and Molnár, V.\n\n\n \n\n\n\n In Tools and Algorithms for the Construction and Analysis of Systems, volume 13244, of Lecture Notes in Computer Science, pages 474–478. Springer, 2022.\n \n\n\n\n
\n\n\n\n \n \n \"Theta: pdf\n  \n \n \n \"Theta: link\n  \n \n\n \n \n doi\n  \n \n\n \n link\n  \n \n\n bibtex\n \n\n \n  \n \n abstract \n \n\n \n  \n \n 2 downloads\n \n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@incollection{tacas2022,\n    author     = {{\\'A}dam, Zs{\\'o}fia and Levente, Bajczi and Dobos-Kov{\\'a}cs, Mih{\\'a}ly and Hajdu, {\\'A}kos and Moln{\\'a}r, Vince},\n    title      = {{T}heta: portfolio of {CEGAR}-based analyses with dynamic algorithm selection (Competition Contribution)},\n    year       = {2022},\n    booktitle  = {Tools and Algorithms for the Construction and Analysis of Systems},\n    series     = {Lecture Notes in Computer Science},\n    volume     = {13244},\n    pages      = {474--478},\n    publisher  = {Springer},\n    doi        = {10.1007/978-3-030-99527-0_34},\n\n    type       = {Conference},\n\n    url_pdf    = {https://hajduakos.github.io/publications/tacas2022.pdf},\n    url_link   = {https://link.springer.com/chapter/10.1007/978-3-030-99527-0_34},\n    abstract   = {Theta is a model checking framework based on abstraction refinement algorithms. In SV-COMP 2022, we introduce: 1) reasoning at the source-level via a direct translation from C programs; 2) support for concurrent programs with interleaving semantics; 3) mitigation for non-progressing refinement loops; 4) support for SMT-LIB-compliant solvers. We combine all of the aforementioned techniques into a portfolio with dynamic algorithm selection.},\n}\n\n
\n
\n\n\n
\n Theta is a model checking framework based on abstraction refinement algorithms. In SV-COMP 2022, we introduce: 1) reasoning at the source-level via a direct translation from C programs; 2) support for concurrent programs with interleaving semantics; 3) mitigation for non-progressing refinement loops; 4) support for SMT-LIB-compliant solvers. We combine all of the aforementioned techniques into a portfolio with dynamic algorithm selection.\n
\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n InfERL: Scalable and Extensible Erlang Static Analysis.\n \n \n \n \n\n\n \n Hajdu, Á.; Marescotti, M.; Suzanne, T.; Mao, K.; Grigore, R.; Gustafsson, P.; and Distefano, D.\n\n\n \n\n\n\n In Proceedings of the 21st ACM SIGPLAN International Workshop on Erlang, pages 33–39, 2022. ACM\n \n\n\n\n
\n\n\n\n \n \n \"InfERL: pdf\n  \n \n \n \"InfERL: slides\n  \n \n \n \"InfERL: link\n  \n \n \n \"InfERL: video\n  \n \n\n \n \n doi\n  \n \n\n \n link\n  \n \n\n bibtex\n \n\n \n  \n \n abstract \n \n\n \n  \n \n 16 downloads\n \n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{erlang2022,\n    author     = {{\\'A}kos Hajdu and Matteo Marescotti and Thibault Suzanne and Ke Mao and Radu Grigore and Per Gustafsson and Dino Distefano},\n    title      = {{InfERL}: Scalable and Extensible {E}rlang Static Analysis},\n    year       = {2022},\n    booktitle  = {Proceedings of the 21st ACM SIGPLAN International Workshop on Erlang},\n    pages      = {33--39},\n    publisher  = {ACM},\n    doi        = {10.1145/3546186.3549929},\n\n    type       = {Workshop},\n\n    url_pdf    = {https://hajduakos.github.io/publications/erlang2022.pdf},\n    url_slides = {https://hajduakos.github.io/publications/slides/erlang2022.pdf},\n    url_link   = {https://dl.acm.org/doi/abs/10.1145/3546186.3549929},\n    url_video  = {https://www.youtube.com/watch?v=ZDZtauSxyaE},\n    abstract   = {In this paper we introduce InfERL, an open source, scalable, and extensible static analyzer for Erlang, based on Meta's Infer tool. InfERL has been developed at WhatsApp and it is deployed to regularly scan WhatsApp server's Erlang codebase, detecting reliability issues and checking user-defined properties. The paper describes the Erlang specific technical challenges we had to address and our design choices. We also report on our experience in running InfERL on Erlang code at scale, supporting the messaging app used everyday by over 2 billion people.},\n}\n\n
\n
\n\n\n
\n In this paper we introduce InfERL, an open source, scalable, and extensible static analyzer for Erlang, based on Meta's Infer tool. InfERL has been developed at WhatsApp and it is deployed to regularly scan WhatsApp server's Erlang codebase, detecting reliability issues and checking user-defined properties. The paper describes the Erlang specific technical challenges we had to address and our design choices. We also report on our experience in running InfERL on Erlang code at scale, supporting the messaging app used everyday by over 2 billion people.\n
\n\n\n
\n\n\n\n\n\n
\n
\n\n
\n
\n  \n 2021\n \n \n (2)\n \n \n
\n
\n \n \n
\n \n\n \n \n \n \n \n \n Gazer-Theta: LLVM-based Verifier Portfolio with BMC/CEGAR (Competition Contribution).\n \n \n \n \n\n\n \n Ádam, Z.; Sallai, G.; and Hajdu, Á.\n\n\n \n\n\n\n In Tools and Algorithms for the Construction and Analysis of Systems, volume 12652, of Lecture Notes in Computer Science, pages 435–439. Springer, 2021.\n \n\n\n\n
\n\n\n\n \n \n \"Gazer-Theta: pdf\n  \n \n \n \"Gazer-Theta: video\n  \n \n\n \n \n doi\n  \n \n\n \n link\n  \n \n\n bibtex\n \n\n \n  \n \n abstract \n \n\n \n  \n \n 21 downloads\n \n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@incollection{tacas2021,\n    author     = {{\\'A}dam, Zs{\\'o}fia and Sallai, Gyula and Hajdu, {\\'A}kos},\n    title      = {{G}azer-{T}heta: {LLVM}-based Verifier Portfolio with {BMC}/{CEGAR} (Competition Contribution)},\n    year       = {2021},\n    booktitle  = {Tools and Algorithms for the Construction and Analysis of Systems},\n    series     = {Lecture Notes in Computer Science},\n    volume     = {12652},\n    publisher  = {Springer},\n    pages      = {435--439},\n    doi        = {10.1007/978-3-030-72013-1_27},\n\n    type       = {Conference},\n\n    url_pdf    = {https://hajduakos.github.io/publications/tacas2021.pdf},\n    url_video  = {https://youtu.be/8DEtrRJixpA},\n    abstract   = {Gazer-Theta is a software model checking toolchain including various analyses for state reachability. The frontend, namely Gazer, supports C programs through an LLVM-based transformation and optimization pipeline. Gazer includes an integrated bounded model checker (BMC) and can also employ the Theta backend, a generic verification framework based on abstraction-refinement (CEGAR). On SV-COMP 2021, a portfolio of BMC, explicit-value analysis, and predicate abstraction is applied sequentially in this order.},\n}\n\n
\n
\n\n\n
\n Gazer-Theta is a software model checking toolchain including various analyses for state reachability. The frontend, namely Gazer, supports C programs through an LLVM-based transformation and optimization pipeline. Gazer includes an integrated bounded model checker (BMC) and can also employ the Theta backend, a generic verification framework based on abstraction-refinement (CEGAR). On SV-COMP 2021, a portfolio of BMC, explicit-value analysis, and predicate abstraction is applied sequentially in this order.\n
\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n Bitvector Support in the Theta Formal Verification Framework.\n \n \n \n \n\n\n \n Dobos-Kovács, M.; Hajdu, Á.; and Vörös, A.\n\n\n \n\n\n\n In Proceedings of the 10th Latin-American Symposium on Dependable Computing, 2021. IEEE\n \n\n\n\n
\n\n\n\n \n \n \"Bitvector pdf\n  \n \n \n \"Bitvector link\n  \n \n\n \n \n doi\n  \n \n\n \n link\n  \n \n\n bibtex\n \n\n \n  \n \n abstract \n \n\n \n  \n \n 3 downloads\n \n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{wafers2021,\n    author     = {Mih{\\'a}ly Dobos-Kov{\\'a}cs and {\\'A}kos Hajdu and Andr{\\'a}s V{\\"o}r{\\"o}s},\n    title      = {Bitvector Support in the {T}heta Formal Verification Framework},\n    booktitle  = {Proceedings of the 10th Latin-American Symposium on Dependable Computing},\n    year       = {2021},\n    publisher  = {IEEE},\n    doi        = {10.1109/LADC53747.2021.9672595},\n\n    type       = {Workshop},\n\n    url_pdf    = {https://hajduakos.github.io/publications/wafers2021.pdf},\n    url_link   = {https://ieeexplore.ieee.org/document/9672595},\n    abstract   = {The verification of safety-critical software systems has many challenges, such as the complex language constructs in embedded software. This paper addresses the verification problem of software systems using bitwise operations, and we present an extension to the Theta open-source formal verification framework. Our goal is to integrate bitvectors and bitwise operations in the abstraction-refinement-based formal verification methods in Theta. Supporting bitvectors is a step towards the verification of industrial embedded software systems. We extended the language support in Theta with formal semantics. In addition, the new language constructs and operators are transformed into the formal language inside Theta. We also need new algorithms to solve the verification problem: we implemented Newton-style refinement algorithms in Theta to verify software with bitvectors and bitwise operators efficiently.},\n}\n\n
\n
\n\n\n
\n The verification of safety-critical software systems has many challenges, such as the complex language constructs in embedded software. This paper addresses the verification problem of software systems using bitwise operations, and we present an extension to the Theta open-source formal verification framework. Our goal is to integrate bitvectors and bitwise operations in the abstraction-refinement-based formal verification methods in Theta. Supporting bitvectors is a step towards the verification of industrial embedded software systems. We extended the language support in Theta with formal semantics. In addition, the new language constructs and operators are transformed into the formal language inside Theta. We also need new algorithms to solve the verification problem: we implemented Newton-style refinement algorithms in Theta to verify software with bitvectors and bitwise operators efficiently.\n
\n\n\n
\n\n\n\n\n\n
\n
\n\n
\n
\n  \n 2020\n \n \n (7)\n \n \n
\n
\n \n \n
\n \n\n \n \n \n \n \n \n solc-verify: A Modular Verifier for Solidity Smart Contracts.\n \n \n \n \n\n\n \n Hajdu, Á.; and Jovanović, D.\n\n\n \n\n\n\n In Verified Software. Theories, Tools, and Experiments, volume 12301, of Lecture Notes in Computer Science, pages 161–179. Springer, 2020.\n \n\n\n\n
\n\n\n\n \n \n \"solc-verify: pdf\n  \n \n \n \"solc-verify: link\n  \n \n \n \"solc-verify: slides\n  \n \n\n \n \n doi\n  \n \n\n \n link\n  \n \n\n bibtex\n \n\n \n  \n \n abstract \n \n\n \n  \n \n 4 downloads\n \n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@incollection{vstte2019,\n    author     = {Hajdu, {\\'A}kos and Jovanovi{\\'c}, Dejan},\n    title      = {solc-verify: A Modular Verifier for {S}olidity Smart Contracts},\n    year       = {2020},\n    booktitle  = {Verified Software. Theories, Tools, and Experiments},\n    pages      = {161--179},\n    series     = {Lecture Notes in Computer Science},\n    volume     = {12301},\n    publisher  = {Springer},\n    doi        = {10.1007/978-3-030-41600-3_11},\n    isbn       = {978-3-030-41600-3},\n\n    type       = {Conference},\n\n    url_pdf    = {https://hajduakos.github.io/publications/vstte2019.pdf},\n    url_link   = {https://link.springer.com/chapter/10.1007/978-3-030-41600-3_11},\n    url_slides = {https://hajduakos.github.io/publications/slides/vstte2019.pdf},\n\n    abstract   = {We present solc-verify, a source-level verification tool for Ethereum smart contracts. Solc-verify takes smart contracts written in Solidity and discharges verification conditions using modular program analysis and SMT solvers. Built on top of the Solidity compiler, solc-verify reasons at the level of the contract source code, as opposed to the more common approaches that operate at the level of Ethereum bytecode. This enables solc-verify to effectively reason about high-level contract properties while modeling low-level language semantics precisely. The contract properties, such as contract invariants, loop invariants, and function pre- and post-conditions, can be provided as annotations in the code by the developer. This enables automated, yet user-friendly formal verification for smart contracts. We demonstrate solc-verify by examining real-world examples where our tool can effectively find bugs and prove correctness of non-trivial properties with minimal user effort.},\n}\n\n
\n
\n\n\n
\n We present solc-verify, a source-level verification tool for Ethereum smart contracts. Solc-verify takes smart contracts written in Solidity and discharges verification conditions using modular program analysis and SMT solvers. Built on top of the Solidity compiler, solc-verify reasons at the level of the contract source code, as opposed to the more common approaches that operate at the level of Ethereum bytecode. This enables solc-verify to effectively reason about high-level contract properties while modeling low-level language semantics precisely. The contract properties, such as contract invariants, loop invariants, and function pre- and post-conditions, can be provided as annotations in the code by the developer. This enables automated, yet user-friendly formal verification for smart contracts. We demonstrate solc-verify by examining real-world examples where our tool can effectively find bugs and prove correctness of non-trivial properties with minimal user effort.\n
\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n Efficient Strategies for CEGAR-based Model Checking.\n \n \n \n \n\n\n \n Hajdu, Á.; and Micskei, Z.\n\n\n \n\n\n\n Journal of Automated Reasoning, 64(6): 1051–1091. 2020.\n \n\n\n\n
\n\n\n\n \n \n \"Efficient pdf\n  \n \n \n \"Efficient link\n  \n \n\n \n \n doi\n  \n \n\n \n link\n  \n \n\n bibtex\n \n\n \n  \n \n abstract \n \n\n \n  \n \n 13 downloads\n \n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@article{jar2019,\n    author   = {{\\'A}kos Hajdu and Zolt{\\'a}n Micskei},\n    title    = {Efficient Strategies for {CEGAR}-based Model Checking},\n    journal  = {Journal of Automated Reasoning},\n    volume   = {64},\n    number   = {6},\n    pages    = {1051--1091},\n    year     = {2020},\n    doi      = {10.1007/s10817-019-09535-x},\n\n    type     = {Journal},\n\n    url_pdf  = {https://link.springer.com/content/pdf/10.1007%2Fs10817-019-09535-x.pdf},\n    url_link = {https://link.springer.com/article/10.1007/s10817-019-09535-x},\n\n    abstract = {Automated formal verification is often based on the Counterexample-Guided Abstraction Refinement (CEGAR) approach. Many variants of CEGAR have been developed over the years as different problem domains usually require different strategies for efficient verification. This has lead to generic and configurable CEGAR frameworks, which can incorporate various algorithms. In our paper we propose six novel improvements to different aspects of the CEGAR approach, including both abstraction and refinement. We implement our new contributions in the Theta framework allowing us to compare them with state-of-the-art algorithms. We conduct an experiment on a diverse set of models to address research questions related to the effectiveness and efficiency of our new strategies. Results show that our new contributions perform well in general. Moreover, we highlight certain cases where performance could not be increased or where a remarkable improvement is achieved.},\n}\n\n
\n
\n\n\n
\n Automated formal verification is often based on the Counterexample-Guided Abstraction Refinement (CEGAR) approach. Many variants of CEGAR have been developed over the years as different problem domains usually require different strategies for efficient verification. This has lead to generic and configurable CEGAR frameworks, which can incorporate various algorithms. In our paper we propose six novel improvements to different aspects of the CEGAR approach, including both abstraction and refinement. We implement our new contributions in the Theta framework allowing us to compare them with state-of-the-art algorithms. We conduct an experiment on a diverse set of models to address research questions related to the effectiveness and efficiency of our new strategies. Results show that our new contributions perform well in general. Moreover, we highlight certain cases where performance could not be increased or where a remarkable improvement is achieved.\n
\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n SMT-Friendly Formalization of the Solidity Memory Model.\n \n \n \n \n\n\n \n Hajdu, Á.; and Jovanović, D.\n\n\n \n\n\n\n In Programming Languages and Systems, volume 12075, of Lecture Notes in Computer Science, pages 224–250. Springer, 2020.\n \n\n\n\n
\n\n\n\n \n \n \"SMT-Friendly pdf\n  \n \n \n \"SMT-Friendly link\n  \n \n \n \"SMT-Friendly slides\n  \n \n \n \"SMT-Friendly video\n  \n \n\n \n \n doi\n  \n \n\n \n link\n  \n \n\n bibtex\n \n\n \n  \n \n abstract \n \n\n \n  \n \n 1 download\n \n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@incollection{esop2020,\n    author     = {Hajdu, {\\'A}kos and Jovanovi{\\'c}, Dejan},\n    title      = {{SMT}-Friendly Formalization of the {S}olidity Memory Model},\n    year       = {2020},\n    booktitle  = {Programming Languages and Systems},\n    series     = {Lecture Notes in Computer Science},\n    volume     = {12075},\n    pages      = {224--250},\n    publisher  = {Springer},\n    doi        = {10.1007/978-3-030-44914-8_9},\n\n    type       = {Conference},\n\n    url_pdf    = {https://hajduakos.github.io/publications/esop2020.pdf},\n    url_link   = {https://link.springer.com/chapter/10.1007/978-3-030-44914-8_9},\n    url_slides = {https://hajduakos.github.io/publications/slides/smt2020.pdf},\n    url_video  = {https://youtu.be/B3ML9vGituk?t=626},\n    abstract   = {Solidity is the dominant programming language for Ethereum smart contracts. This paper presents a high-level formalization of the Solidity language with a focus on the memory model. The presented formalization covers all features of the language related to managing state and memory. In addition, the formalization we provide is effective: all but few features can be encoded in the quantifier-free fragment of standard SMT theories. This enables precise and efficient reasoning about the state of smart contracts written in Solidity. The formalization is implemented in the solc-verify verifier and we provide an extensive set of tests that covers the breadth of the required semantics. We also provide an evaluation on the test set that validates the semantics and shows the novelty of the approach compared to other Solidity-level contract analysis tools. },\n}\n\n
\n
\n\n\n
\n Solidity is the dominant programming language for Ethereum smart contracts. This paper presents a high-level formalization of the Solidity language with a focus on the memory model. The presented formalization covers all features of the language related to managing state and memory. In addition, the formalization we provide is effective: all but few features can be encoded in the quantifier-free fragment of standard SMT theories. This enables precise and efficient reasoning about the state of smart contracts written in Solidity. The formalization is implemented in the solc-verify verifier and we provide an extensive set of tests that covers the breadth of the required semantics. We also provide an evaluation on the test set that validates the semantics and shows the novelty of the approach compared to other Solidity-level contract analysis tools. \n
\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n Formal Specification and Verification of Solidity Contracts with Events (short paper).\n \n \n \n \n\n\n \n Hajdu, Á.; Jovanović, D.; and Ciocarlie, G.\n\n\n \n\n\n\n In 2nd Workshop on Formal Methods for Blockchains, volume 84, of OpenAccess Series in Informatics (OASIcs), pages 2:1–2:9. Schloss Dagstuhl–Leibniz-Zentrum für Informatik, 2020.\n \n\n\n\n
\n\n\n\n \n \n \"Formal pdf\n  \n \n \n \"Formal link\n  \n \n \n \"Formal slides\n  \n \n \n \"Formal video\n  \n \n\n \n \n doi\n  \n \n\n \n link\n  \n \n\n bibtex\n \n\n \n  \n \n abstract \n \n\n \n  \n \n 10 downloads\n \n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@incollection{fmbc2020,\n    author     = {{\\'A}kos Hajdu and Jovanovi{\\'c}, Dejan and Ciocarlie, Gabriela},\n    title      = {Formal Specification and Verification of {S}olidity Contracts with Events (short paper)},\n    booktitle  = {2nd Workshop on Formal Methods for Blockchains},\n    series     = {OpenAccess Series in Informatics (OASIcs)},\n    volume     = {84},\n    pages      = {2:1--2:9},\n    publisher  = {Schloss Dagstuhl--Leibniz-Zentrum f{\\"u}r Informatik},\n    year       = {2020},\n    isbn       = {978-3-95977-169-6},\n    issn       = {2190-6807},\n    doi        = {10.4230/OASIcs.FMBC.2020.2},\n\n    type       = {Workshop},\n\n    url_pdf    = {https://drops.dagstuhl.de/opus/volltexte/2020/13415/pdf/OASIcs-FMBC-2020-2.pdf},\n    url_link   = {https://drops.dagstuhl.de/opus/volltexte/2020/13415/},\n    url_slides = {https://hajduakos.github.io/publications/slides/fmbc2020.pdf},\n    url_video  = {https://youtu.be/NNytwVBZ1no},\n    abstract   = {Events in the Solidity language provide a means of communication between the on-chain services of decentralized applications and the users of those services. Events are commonly used as an abstraction of contract execution that is relevant from the users' perspective. Users must, therefore, be able to understand the meaning and trust the validity of the emitted events. This paper presents a source-level approach for the formal specification and verification of Solidity contracts with the primary focus on events. Our approach allows the specification of events in terms of the on-chain data that they track, and the predicates that define the correspondence between the blockchain state and the abstract view provided by the events. The approach is implemented in solc-verify, a modular verifier for Solidity, and we demonstrate its applicability with various examples.}\n}\n\n
\n
\n\n\n
\n Events in the Solidity language provide a means of communication between the on-chain services of decentralized applications and the users of those services. Events are commonly used as an abstraction of contract execution that is relevant from the users' perspective. Users must, therefore, be able to understand the meaning and trust the validity of the emitted events. This paper presents a source-level approach for the formal specification and verification of Solidity contracts with the primary focus on events. Our approach allows the specification of events in terms of the on-chain data that they track, and the predicates that define the correspondence between the blockchain state and the abstract view provided by the events. The approach is implemented in solc-verify, a modular verifier for Solidity, and we demonstrate its applicability with various examples.\n
\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n MIDDLEWARE TO AUTOMATICALLY VERIFY SMART CONTRACTS ON BLOCKCHAINS.\n \n \n \n \n\n\n \n Ciocarlie, G.; Eldefrawy, K.; Lepoint, T.; Navas, J.; Hajdu, Á.; and Jovanović, D.\n\n\n \n\n\n\n June 2020.\n US Patent App. 16/227,728\n\n\n\n
\n\n\n\n \n \n \"MIDDLEWARE link\n  \n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n  \n \n abstract \n \n\n \n  \n \n 10 downloads\n \n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@misc{patent2020,\n    title     = {MIDDLEWARE TO AUTOMATICALLY VERIFY SMART CONTRACTS ON BLOCKCHAINS},\n    author    = {Ciocarlie, Gabriela and Eldefrawy, Karim and Lepoint, Tancrede and Navas, Jorge and Hajdu, {\\'A}kos and Jovanovi{\\'c}, Dejan},\n    year      = {2020},\n    month     = {June},\n    note      = {US Patent App. 16/227,728},\n\n    type      = {Patent application},\n\n    url_link  = {http://www.freepatentsonline.com/y2020/0201838.html},\n    abstract  = {A method, apparatus and system for automated verification of a smart contract on a blockchain include translating operating properties of a smart contract annotated with contract specifications at a source code level into verification conditions in an intermediate verification language, discharging the verification conditions using an SMT solver, and reporting results of the discharged verification conditions, such as successes and failures of the discharged verification conditions. The translating can include mapping statements of the smart contract to statements of the intermediate verification language and mapping expressions of the smart contract to expressions of the intermediate verification language. }\n}\n\n
\n
\n\n\n
\n A method, apparatus and system for automated verification of a smart contract on a blockchain include translating operating properties of a smart contract annotated with contract specifications at a source code level into verification conditions in an intermediate verification language, discharging the verification conditions using an SMT solver, and reporting results of the discharged verification conditions, such as successes and failures of the discharged verification conditions. The translating can include mapping statements of the smart contract to statements of the intermediate verification language and mapping expressions of the smart contract to expressions of the intermediate verification language. \n
\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n Model Checking as a Service: Towards Pragmatic Hidden Formal Methods.\n \n \n \n \n\n\n \n Horváth, B.; Graics, B.; Hajdu, Á.; Micskei, Z.; Molnár, V.; Ráth, I.; Andolfato, L.; Gomes, I.; and Karban, R.\n\n\n \n\n\n\n In Proceedings of the 23rd ACM/IEEE International Conference on Model Driven Engineering Languages and Systems: Companion Proceedings, 2020. \n \n\n\n\n
\n\n\n\n \n \n pdf\n  \n \n \n link\n  \n \n\n \n \n doi\n  \n \n\n \n link\n  \n \n\n bibtex\n \n\n \n  \n \n abstract \n \n\n \n  \n \n 8 downloads\n \n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{openmbee2020,\n    author     = {Benedek Horv{\\'a}th and Bence Graics and {\\'A}kos Hajdu and Zolt{\\'a}n Micskei and Vince Moln{\\'a}r and Istv{\\'a}n R{\\'a}th and Luigi Andolfato and Ivan Gomes and Robert Karban},\n    title      = {Model Checking as a Service: Towards Pragmatic Hidden Formal Methods},\n    booktitle  = {Proceedings of the 23rd ACM/IEEE International Conference on Model Driven Engineering Languages and Systems: Companion Proceedings},\n    articleno  = {37},\n    numpages   = {5},\n    year       = {2020},\n    doi        = {10.1145/3417990.3421407},\n\n    type       = {Workshop},\n\n    url_pdf    = {https://hajduakos.github.io/publications/openmbee2020.pdf},\n    url_link   = {https://doi.org/10.1145/3417990.3421407},\n    abstract   = {Executable models can be used to support all engineering activities in Model-Based Systems Engineering. Testing and simulation of such models can provide early feedback about design choices. However, in today's complex systems, failures could arise due to subtle errors that are hard to find without checking all possible execution paths. Formal methods, and especially model checking can uncover such subtle errors, yet their usage in practice is limited due to the specialized expertise and high computing power required. Therefore we created an automated, cloud-based environment that can verify complex reachability properties on SysML State Machines using hidden model checkers. The approach and the prototype is illustrated using an example from the aerospace domain.},\n}\n\n
\n
\n\n\n
\n Executable models can be used to support all engineering activities in Model-Based Systems Engineering. Testing and simulation of such models can provide early feedback about design choices. However, in today's complex systems, failures could arise due to subtle errors that are hard to find without checking all possible execution paths. Formal methods, and especially model checking can uncover such subtle errors, yet their usage in practice is limited due to the specialized expertise and high computing power required. Therefore we created an automated, cloud-based environment that can verify complex reachability properties on SysML State Machines using hidden model checkers. The approach and the prototype is illustrated using an example from the aerospace domain.\n
\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n Using Fault Injection to Assess Blockchain Systems in Presence of Faulty Smart Contracts.\n \n \n \n \n\n\n \n Hajdu, Á.; Ivaki, N.; Kocsis, I.; Klenik, A.; Gönczy, L.; Laranjeiro, N.; Madeira, H.; and Pataricza, A.\n\n\n \n\n\n\n IEEE Access, 8: 190760–190783. 2020.\n \n\n\n\n
\n\n\n\n \n \n \"Using pdf\n  \n \n \n \"Using link\n  \n \n\n \n \n doi\n  \n \n\n \n link\n  \n \n\n bibtex\n \n\n \n  \n \n abstract \n \n\n \n  \n \n 2 downloads\n \n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@article{access2020,\n    author     = {{\\'A}kos Hajdu and Naghmeh Ivaki and Imre Kocsis and Attila Klenik and L{\\'a}szl{\\'o} G{\\"o}nczy and Nuno Laranjeiro and Henrique Madeira and Andr{\\'a}s Pataricza},\n    title      = {Using Fault Injection to Assess Blockchain Systems in Presence of Faulty Smart Contracts},\n    journal    = {IEEE Access},\n    year       = {2020},\n    volume     = {8},\n    pages      = {190760--190783},\n    doi        = {10.1109/ACCESS.2020.3032239},\n\n    type       = {Journal},\n\n    url_pdf    = {https://arxiv.org/abs/2006.11597.pdf},\n    url_link   = {https://ieeexplore.ieee.org/document/9229414},\n    abstract   = {Blockchain has become particularly popular due to its promise to support businesscritical services in very different domains (e.g., retail, healthcare). Blockchain systems rely on complex middleware, like Ethereum or Hyperledger Fabric, that allow running smart contracts, which specify business logic in cooperative applications. The presence of software defects in these contracts has notably caused failures, including severe security problems. In this paper, we use software-implemented fault injection (SWIFI) to assess the behavior of permissioned blockchain systems in the presence of faulty smart contracts. We emulate the occurrence of general software faults and also blockchain-specific software faults (e.g., missing require on transaction sender) in smart contracts code and observe the impact on the overall system dependability in terms of reliability and integrity. We also analyze the effectiveness of formal verification and runtime protection mechanisms in detecting the injected faults. Results indicate that formal verification and runtime protections have to complement built-in platform checks to guarantee proper dependability of blockchain systems. The work presented in this paper allows smart contract developers to become aware of possible faults in smart contracts and to understand the impact of their presence. It also provides valuable information for middleware developers to improve the overall fault tolerance of their systems.},\n}\n\n
\n
\n\n\n
\n Blockchain has become particularly popular due to its promise to support businesscritical services in very different domains (e.g., retail, healthcare). Blockchain systems rely on complex middleware, like Ethereum or Hyperledger Fabric, that allow running smart contracts, which specify business logic in cooperative applications. The presence of software defects in these contracts has notably caused failures, including severe security problems. In this paper, we use software-implemented fault injection (SWIFI) to assess the behavior of permissioned blockchain systems in the presence of faulty smart contracts. We emulate the occurrence of general software faults and also blockchain-specific software faults (e.g., missing require on transaction sender) in smart contracts code and observe the impact on the overall system dependability in terms of reliability and integrity. We also analyze the effectiveness of formal verification and runtime protection mechanisms in detecting the injected faults. Results indicate that formal verification and runtime protections have to complement built-in platform checks to guarantee proper dependability of blockchain systems. The work presented in this paper allows smart contract developers to become aware of possible faults in smart contracts and to understand the impact of their presence. It also provides valuable information for middleware developers to improve the overall fault tolerance of their systems.\n
\n\n\n
\n\n\n\n\n\n
\n
\n\n
\n
\n  \n 2019\n \n \n (1)\n \n \n
\n
\n \n \n
\n \n\n \n \n \n \n \n \n Software Model Checking with a Combination of Explicit Values and Predicates.\n \n \n \n \n\n\n \n Bajkai, V. D.; and Hajdu, Á.\n\n\n \n\n\n\n In Proceedings of the 26th PhD Mini-Symposium, pages 4–7, 2019. Budapest University of Technology and Economics, Department of Measurement and Information Systems\n \n\n\n\n
\n\n\n\n \n \n \"Software pdf\n  \n \n \n \"Software link\n  \n \n\n \n \n doi\n  \n \n\n \n link\n  \n \n\n bibtex\n \n\n \n  \n \n abstract \n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{minisy2019,\n    author     = {Bajkai, Vikt{\\'o}ria Dorina and Hajdu, {\\'A}kos},\n    title      = {Software Model Checking with a Combination of Explicit Values and Predicates},\n    year       = {2019},\n    booktitle  = {Proceedings of the 26th PhD Mini-Symposium},\n    location   = {Budapest, Hungary},\n    publisher  = {Budapest University of Technology and Economics, Department of Measurement and Information Systems},\n    pages      = {4--7},\n    isbn       = {978-963-313-314-9},\n    doi        = {10.5281/zenodo.2597969},\n\n    type       = {Local event},\n\n    url_pdf    = {https://hajduakos.github.io/publications/minisy2019.pdf},\n    url_link   = {http://doi.org/10.5281/zenodo.2597969},\n\n    abstract   = {Formal verification techniques can both reveal bugs or prove their absence in programs with a sound mathematical basis. However, their high computational complexity often prevents their application on real-world software. Counterexample-guided abstraction refinement (CEGAR) aims to improve efficiency by automatically constructing and refining abstractions for the program. There are several existing abstract domains, such as explicit-values and predicates, but different abstract domains are suitable for different kinds of software. Therefore, product domains have also emerged, which combine different kinds of abstractions in a single algorithm. In this paper, we present a new variant of the CEGAR algorithm, which is a combination of explicit-value analysis and predicate abstraction. We perform an experiment with a wide range of software systems and we compare the results to the existing methods. Measurements show that our new algorithm can efficiently combine the advantages of the different domains.},\n}\n\n
\n
\n\n\n
\n Formal verification techniques can both reveal bugs or prove their absence in programs with a sound mathematical basis. However, their high computational complexity often prevents their application on real-world software. Counterexample-guided abstraction refinement (CEGAR) aims to improve efficiency by automatically constructing and refining abstractions for the program. There are several existing abstract domains, such as explicit-values and predicates, but different abstract domains are suitable for different kinds of software. Therefore, product domains have also emerged, which combine different kinds of abstractions in a single algorithm. In this paper, we present a new variant of the CEGAR algorithm, which is a combination of explicit-value analysis and predicate abstraction. We perform an experiment with a wide range of software systems and we compare the results to the existing methods. Measurements show that our new algorithm can efficiently combine the advantages of the different domains.\n
\n\n\n
\n\n\n\n\n\n
\n
\n\n
\n
\n  \n 2018\n \n \n (3)\n \n \n
\n
\n \n \n
\n \n\n \n \n \n \n \n \n Industrial Applications of the PetriDotNet Modelling and Analysis Tool.\n \n \n \n \n\n\n \n Vörös, A.; Darvas, D.; Hajdu, Á.; Klenik, A.; Marussy, K.; Molnár, V.; Bartha, T.; and Majzik, I.\n\n\n \n\n\n\n Science of Computer Programming, 157: 17–40. 2018.\n \n\n\n\n
\n\n\n\n \n \n \"Industrial pdf\n  \n \n \n \"Industrial link\n  \n \n\n \n \n doi\n  \n \n\n \n link\n  \n \n\n bibtex\n \n\n \n  \n \n abstract \n \n\n \n  \n \n 1 download\n \n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@article{scp2017,\n    author   = {Andr{\\'a}s V\\"{o}r\\"{o}s and D{\\'a}niel Darvas and {\\'A}kos Hajdu and Attila Klenik and Krist{\\'o}f Marussy and Vince Moln{\\'a}r and Tam{\\'a}s Bartha and Istv{\\'a}n Majzik},\n    title    = {Industrial Applications of the {P}etri{D}ot{N}et Modelling and Analysis Tool},\n    year     = {2018},\n    journal  = {Science of Computer Programming},\n    volume   = {157},\n    pages    = {17--40},\n    issn     = {0167-6423},\n    doi      = {10.1016/j.scico.2017.09.003},\n\n    type     = {Journal},\n\n    url_pdf  = {https://hajduakos.github.io/publications/scp2017.pdf},\n    url_link = {http://www.sciencedirect.com/science/article/pii/S0167642317301910},\n\n    abstract = {Since their invention, Petri nets have provided modelling and analysis methods to support the design of correct, reliable and robust systems. This motivated our work to develop PetriDotNet, a Petri net editor and analysis tool. In this paper we overview the supported modelling formalisms and the analysis methods included in PetriDotNet. Next, we present eight different industrial case studies, demonstrating the wide variety of scenarios where Petri nets and PetriDotNet can help the design, development and analysis of industrial systems. Our original goal with PetriDotNet was to provide an educational tool to our students, however our efforts led to a framework being able to serve both academic and industrial needs.},\n}\n\n
\n
\n\n\n
\n Since their invention, Petri nets have provided modelling and analysis methods to support the design of correct, reliable and robust systems. This motivated our work to develop PetriDotNet, a Petri net editor and analysis tool. In this paper we overview the supported modelling formalisms and the analysis methods included in PetriDotNet. Next, we present eight different industrial case studies, demonstrating the wide variety of scenarios where Petri nets and PetriDotNet can help the design, development and analysis of industrial systems. Our original goal with PetriDotNet was to provide an educational tool to our students, however our efforts led to a framework being able to serve both academic and industrial needs.\n
\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n A Preliminary Analysis on the Effect of Randomness in a CEGAR Framework.\n \n \n \n \n\n\n \n Hajdu, Á.; and Micskei, Z.\n\n\n \n\n\n\n In Proceedings of the 25th PhD Mini-Symposium, pages 32–35, 2018. Budapest University of Technology and Economics, Department of Measurement and Information Systems\n \n\n\n\n
\n\n\n\n \n \n \"A pdf\n  \n \n \n \"A link\n  \n \n \n \"A slides\n  \n \n\n \n \n doi\n  \n \n\n \n link\n  \n \n\n bibtex\n \n\n \n  \n \n abstract \n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{minisy2018,\n    author     = {Hajdu, {\\'A}kos and Micskei, Zolt{\\'a}n},\n    title      = {A Preliminary Analysis on the Effect of Randomness in a {CEGAR} Framework},\n    year       = {2018},\n    booktitle  = {Proceedings of the 25th PhD Mini-Symposium},\n    location   = {Budapest, Hungary},\n    publisher  = {Budapest University of Technology and Economics, Department of Measurement and Information Systems},\n    pages      = {32--35},\n    doi        = {10.5281/zenodo.1219261},\n    isbn       = {978-963-313-285-2},\n\n    type       = {Local event},\n\n    url_pdf    = {https://hajduakos.github.io/publications/minisy2018.pdf},\n    url_link   = {https://doi.org/10.5281/zenodo.1219261},\n    url_slides = {https://hajduakos.github.io/publications/slides/minisy2018.pdf},\n\n    abstract   = {Formal verification techniques can check the correctness of systems in a mathematically precise way. Counterexample-Guided Abstraction Refinement (CEGAR) is an automatic algorithm that reduces the complexity of systems by constructing and refining abstractions. CEGAR is a generic approach, having many variants and strategies developed over the years. However, as the variants become more and more advanced, one may not be sure whether the performance of a strategy can be attributed to the strategy itself or to other, unintentional factors. In this paper we perform an experiment by evaluating the performance of different strategies while randomizing certain external factors such as the search strategy and variable naming. We show that randomization introduces a great variation in the output metrics, and that in several cases this might even influence whether the algorithm successfully terminates.},\n}\n\n
\n
\n\n\n
\n Formal verification techniques can check the correctness of systems in a mathematically precise way. Counterexample-Guided Abstraction Refinement (CEGAR) is an automatic algorithm that reduces the complexity of systems by constructing and refining abstractions. CEGAR is a generic approach, having many variants and strategies developed over the years. However, as the variants become more and more advanced, one may not be sure whether the performance of a strategy can be attributed to the strategy itself or to other, unintentional factors. In this paper we perform an experiment by evaluating the performance of different strategies while randomizing certain external factors such as the search strategy and variable naming. We show that randomization introduces a great variation in the output metrics, and that in several cases this might even influence whether the algorithm successfully terminates.\n
\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n Backward reachability analysis for timed automata with data variables.\n \n \n \n \n\n\n \n Farkas, R.; Tóth, T.; Hajdu, Á.; and Vörös, A.\n\n\n \n\n\n\n In Proceedings of the 18th International Workshop on Automated Verification of Critical Systems, volume 76, of Electronic Communications of the EASST, pages 1–20. EASST, 2018.\n \n\n\n\n
\n\n\n\n \n \n \"Backward pdf\n  \n \n \n \"Backward link\n  \n \n\n \n \n doi\n  \n \n\n \n link\n  \n \n\n bibtex\n \n\n \n  \n \n abstract \n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@incollection{avocs2018,\n    author     = {Farkas, Rebeka and T{\\'o}th, Tam{\\'a}s and Hajdu, {\\'A}kos and V{\\"o}r{\\"o}s, Andr{\\'a}s},\n    title      = {Backward reachability analysis for timed automata with data variables},\n    year       = {2018},\n    booktitle  = {Proceedings of the 18th International Workshop on Automated Verification of Critical Systems},\n    series     = {Electronic Communications of the EASST},\n    issn       = {1863-2122},\n    volume     = {76},\n    publisher  = {EASST},\n    pages      = {1--20},\n    doi        = {10.14279/tuj.eceasst.76.1076},\n\n    type       = {Workshop},\n\n    url_pdf    = {https://hajduakos.github.io/publications/avocs2018.pdf},\n    url_link   = {https://journal.ub.tu-berlin.de/eceasst/article/view/1076},\n\n    abstract   = {Efficient techniques for reachability analysis of timed automata are zone-based methods that explore the reachable state space from the initial state, and SMT-based methods that perform backward search from the target states. It is also possible to perform backward exploration based on zones, but calculating predecessor states for systems with data variables is computationally expensive, prohibiting the successful application of this approach so far. In this paper we overcome this limitation by combining zone-based backward exploration with the weakest precondition operation for data variables. This combination allows us to handle diagonal constraints efficiently as opposed to zone-based forward search where most approaches require additional operations to ensure correctness. We demonstrate the applicability and compare the efficiency of the algorithm to existing forward exploration approaches by measurements performed on industrial case studies. Although the large number of states often prevents successful verification, we show that data variables can be efficienlty handled by the weakest precondition operation. This way our new approach complements existing techniques.}\n}\n\n
\n
\n\n\n
\n Efficient techniques for reachability analysis of timed automata are zone-based methods that explore the reachable state space from the initial state, and SMT-based methods that perform backward search from the target states. It is also possible to perform backward exploration based on zones, but calculating predecessor states for systems with data variables is computationally expensive, prohibiting the successful application of this approach so far. In this paper we overcome this limitation by combining zone-based backward exploration with the weakest precondition operation for data variables. This combination allows us to handle diagonal constraints efficiently as opposed to zone-based forward search where most approaches require additional operations to ensure correctness. We demonstrate the applicability and compare the efficiency of the algorithm to existing forward exploration approaches by measurements performed on industrial case studies. Although the large number of states often prevents successful verification, we show that data variables can be efficienlty handled by the weakest precondition operation. This way our new approach complements existing techniques.\n
\n\n\n
\n\n\n\n\n\n
\n
\n\n
\n
\n  \n 2017\n \n \n (5)\n \n \n
\n
\n \n \n
\n \n\n \n \n \n \n \n \n Exploratory Analysis of the Performance of a Configurable CEGAR Framework.\n \n \n \n \n\n\n \n Hajdu, Á.; and Micskei, Z.\n\n\n \n\n\n\n In Proceedings of the 24th PhD Mini-Symposium, pages 34–37, 2017. Budapest University of Technology and Economics, Department of Measurement and Information Systems\n \n\n\n\n
\n\n\n\n \n \n \"Exploratory pdf\n  \n \n \n \"Exploratory link\n  \n \n \n \"Exploratory slides\n  \n \n\n \n \n doi\n  \n \n\n \n link\n  \n \n\n bibtex\n \n\n \n  \n \n abstract \n \n\n \n  \n \n 2 downloads\n \n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{minisy2017,\n    author     = {Hajdu, {\\'A}kos and Micskei, Zolt{\\'a}n},\n    title      = {Exploratory Analysis of the Performance of a Configurable {CEGAR} Framework},\n    year       = {2017},\n    booktitle  = {Proceedings of the 24th PhD Mini-Symposium},\n    location   = {Budapest, Hungary},\n    publisher  = {Budapest University of Technology and Economics, Department of Measurement and Information Systems},\n    pages      = {34--37},\n    doi        = {10.5281/zenodo.291895},\n    isbn       = {978-963-313-243-2},\n\n    type       = {Local event},\n\n    url_pdf    = {https://hajduakos.github.io/publications/minisy2017.pdf},\n    url_link   = {https://doi.org/10.5281/zenodo.291895},\n    url_slides = {https://hajduakos.github.io/publications/slides/minisy2017.pdf},\n\n    abstract   = {Formal verification techniques can check the correctness of systems in a mathematically precise way. However, their computational complexity often prevents their successful application. The counterexample-guided abstraction refinement (CEGAR) algorithm aims to overcome this problem by automatically building abstractions for the system to reduce its complexity. Previously, we developed a generic CEGAR framework, which incorporates many configurations of the algorithm. In this paper we focus on an exploratory analysis of our framework. We identify parameters of the systems and algorithm configurations, overview some possible analysis methods and present preliminary results. We show that different variants are more efficient for certain tasks and we also describe how the properties of the system and parameters of the algorithm affect the success of verification.},\n}\n\n
\n
\n\n\n
\n Formal verification techniques can check the correctness of systems in a mathematically precise way. However, their computational complexity often prevents their successful application. The counterexample-guided abstraction refinement (CEGAR) algorithm aims to overcome this problem by automatically building abstractions for the system to reduce its complexity. Previously, we developed a generic CEGAR framework, which incorporates many configurations of the algorithm. In this paper we focus on an exploratory analysis of our framework. We identify parameters of the systems and algorithm configurations, overview some possible analysis methods and present preliminary results. We show that different variants are more efficient for certain tasks and we also describe how the properties of the system and parameters of the algorithm affect the success of verification.\n
\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n Activity-Based Abstraction Refinement for Timed Systems.\n \n \n \n \n\n\n \n Farkas, R.; and Hajdu, Á.\n\n\n \n\n\n\n In Proceedings of the 24th PhD Mini-Symposium, pages 18–21, 2017. Budapest University of Technology and Economics, Department of Measurement and Information Systems\n \n\n\n\n
\n\n\n\n \n \n \"Activity-Based pdf\n  \n \n \n \"Activity-Based link\n  \n \n\n \n \n doi\n  \n \n\n \n link\n  \n \n\n bibtex\n \n\n \n  \n \n abstract \n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{minisy2017fr,\n    author     = {Farkas, Rebeka and Hajdu, {\\'A}kos},\n    title      = {Activity-Based Abstraction Refinement for Timed Systems},\n    year       = {2017},\n    booktitle  = {Proceedings of the 24th PhD Mini-Symposium},\n    location   = {Budapest, Hungary},\n    publisher  = {Budapest University of Technology and Economics, Department of Measurement and Information Systems},\n    pages      = {18--21},\n    doi        = {10.5281/zenodo.291891},\n    isbn       = {978-963-313-243-2},\n\n    type       = {Local event},\n\n    url_pdf    = {https://hajduakos.github.io/publications/minisy2017fr.pdf},\n    url_link   = {https://doi.org/10.5281/zenodo.291891},\n\n    abstract   = {Formal analysis of real time systems is important as they are widely used in safety critical domains. Such systems combine discrete behaviours represented by control states and timed behaviours represented by clock variables. The counterexample-guided abstraction refinement (CEGAR) algorithm utilizes the fundamental technique of abstraction to system verification. We propose a CEGAR-based algorithm for reachability analysis of timed systems. The algorithm is specialized to handle the time related behaviours efficiently by introducing a refinement technique tailored specially to clock variables. The performance of the presented algorithm is demonstrated by runtime measurements on models commonly used for benchmarking such algorithms.},\n}\n\n
\n
\n\n\n
\n Formal analysis of real time systems is important as they are widely used in safety critical domains. Such systems combine discrete behaviours represented by control states and timed behaviours represented by clock variables. The counterexample-guided abstraction refinement (CEGAR) algorithm utilizes the fundamental technique of abstraction to system verification. We propose a CEGAR-based algorithm for reachability analysis of timed systems. The algorithm is specialized to handle the time related behaviours efficiently by introducing a refinement technique tailored specially to clock variables. The performance of the presented algorithm is demonstrated by runtime measurements on models commonly used for benchmarking such algorithms.\n
\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n Exploiting Hierarchy in the Abstraction-Based Verification of Statecharts Using SMT Solvers.\n \n \n \n \n\n\n \n Czipó, B.; Hajdu, Á.; Tóth, T.; and Majzik, I.\n\n\n \n\n\n\n In Proceedings of the 14th International Workshop on Formal Engineering Approaches to Software Components and Architectures, volume 245, of Electronic Proceedings in Theoretical Computer Science, pages 31–45. Open Publishing Association, 2017.\n \n\n\n\n
\n\n\n\n \n \n \"Exploiting pdf\n  \n \n \n \"Exploiting link\n  \n \n \n \"Exploiting slides\n  \n \n\n \n \n doi\n  \n \n\n \n link\n  \n \n\n bibtex\n \n\n \n  \n \n abstract \n \n\n \n  \n \n 3 downloads\n \n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@incollection{fesca2017,\n    author     = {Czip{\\'o}, Bence and Hajdu, {\\'A}kos and T{\\'o}th, Tam{\\'a}s and Majzik, Istv{\\'a}n},\n    year       = {2017},\n    title      = {Exploiting Hierarchy in the Abstraction-Based Verification of Statecharts Using {SMT} Solvers},\n    booktitle  = {Proceedings of the 14th International Workshop on Formal Engineering Approaches to Software Components and Architectures},\n    series     = {Electronic Proceedings in Theoretical Computer Science},\n    volume     = {245},\n    publisher  = {Open Publishing Association},\n    pages      = {31--45},\n    doi        = {10.4204/EPTCS.245.3},\n\n    type       = {Workshop},\n\n    url_pdf    = {https://hajduakos.github.io/publications/fesca2017.pdf},\n    url_link   = {http://eptcs.web.cse.unsw.edu.au/paper.cgi?FESCA2017.3},\n    url_slides = {https://hajduakos.github.io/publications/slides/fesca2017.pdf},\n\n    abstract   = {Statecharts are frequently used as a modeling formalism in the design of state-based systems. Formal verification techniques are also often applied to prove certain properties about the behavior of the system. One of the most efficient techniques for formal verification is Counterexample-Guided Abstraction Refinement (CEGAR), which reduces the complexity of systems by automatically building and refining abstractions. In our paper we present a novel adaptation of the CEGAR approach to hierarchical statechart models. First we introduce an encoding of the statechart to logical formulas that preserves information about the state hierarchy. Based on this encoding we propose abstraction and refinement techniques that utilize the hierarchical structure of statecharts and also handle variables in the model. The encoding allows us to use SMT solvers for the systematic exploration and verification of the abstract model, including also bounded model checking. We demonstrate the applicability and efficiency of our abstraction techniques with measurements on an industry-motivated example.},\n}\n\n
\n
\n\n\n
\n Statecharts are frequently used as a modeling formalism in the design of state-based systems. Formal verification techniques are also often applied to prove certain properties about the behavior of the system. One of the most efficient techniques for formal verification is Counterexample-Guided Abstraction Refinement (CEGAR), which reduces the complexity of systems by automatically building and refining abstractions. In our paper we present a novel adaptation of the CEGAR approach to hierarchical statechart models. First we introduce an encoding of the statechart to logical formulas that preserves information about the state hierarchy. Based on this encoding we propose abstraction and refinement techniques that utilize the hierarchical structure of statecharts and also handle variables in the model. The encoding allows us to use SMT solvers for the systematic exploration and verification of the abstract model, including also bounded model checking. We demonstrate the applicability and efficiency of our abstraction techniques with measurements on an industry-motivated example.\n
\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n Towards Evaluating Size Reduction Techniques for Software Model Checking.\n \n \n \n \n\n\n \n Sallai, G.; Hajdu, Á.; Tóth, T.; and Micskei, Z.\n\n\n \n\n\n\n In Proceedings of the Fifth International Workshop on Verification and Program Transformation, volume 253, of Electronic Proceedings in Theoretical Computer Science, pages 75–91. Open Publishing Association, 2017.\n \n\n\n\n
\n\n\n\n \n \n \"Towards pdf\n  \n \n \n \"Towards link\n  \n \n \n \"Towards slides\n  \n \n\n \n \n doi\n  \n \n\n \n link\n  \n \n\n bibtex\n \n\n \n  \n \n abstract \n \n\n \n  \n \n 2 downloads\n \n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@incollection{vpt2017,\n    author     = {Sallai, Gyula and Hajdu, {\\'A}kos and T{\\'o}th, Tam{\\'a}s and Micskei, Zolt{\\'a}n},\n    year       = {2017},\n    title      = {Towards Evaluating Size Reduction Techniques for Software Model Checking},\n    booktitle  = {Proceedings of the Fifth International Workshop on Verification and Program Transformation},\n    series     = {Electronic Proceedings in Theoretical Computer Science},\n    volume     = {253},\n    publisher  = {Open Publishing Association},\n    pages      = {75--91},\n    doi        = {10.4204/EPTCS.253.7},\n\n    type       = {Workshop},\n\n    url_pdf    = {https://hajduakos.github.io/publications/vpt2017.pdf},\n    url_link   = {http://eptcs.web.cse.unsw.edu.au/paper.cgi?VPT2017.7},\n    url_slides = {https://hajduakos.github.io/publications/slides/vpt2017.pdf},\n\n    abstract   = {Formal verification techniques are widely used for detecting design flaws in software systems. Formal verification can be done by transforming an already implemented source code to a formal model and attempting to prove certain properties of the model (e.g. that no erroneous state can occur during execution). Unfortunately, transformations from source code to a formal model often yield large and complex models, making the verification process inefficient and costly. In order to reduce the size of the resulting model, optimization transformations can be used. Such optimizations include common algorithms known from compiler design and different program slicing techniques. Our paper describes a framework for transforming C programs to a formal model, enhanced by various optimizations for size reduction. We evaluate and compare several optimization algorithms regarding their effect on the size of the model and the efficiency of the verification. Results show that different optimizations are more suitable for certain models, justifying the need for a framework that includes several algorithms.}\n}\n\n
\n
\n\n\n
\n Formal verification techniques are widely used for detecting design flaws in software systems. Formal verification can be done by transforming an already implemented source code to a formal model and attempting to prove certain properties of the model (e.g. that no erroneous state can occur during execution). Unfortunately, transformations from source code to a formal model often yield large and complex models, making the verification process inefficient and costly. In order to reduce the size of the resulting model, optimization transformations can be used. Such optimizations include common algorithms known from compiler design and different program slicing techniques. Our paper describes a framework for transforming C programs to a formal model, enhanced by various optimizations for size reduction. We evaluate and compare several optimization algorithms regarding their effect on the size of the model and the efficiency of the verification. Results show that different optimizations are more suitable for certain models, justifying the need for a framework that includes several algorithms.\n
\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n Theta: a Framework for Abstraction Refinement-Based Model Checking.\n \n \n \n \n\n\n \n Tóth, T.; Hajdu, Á.; Vörös, A.; Micskei, Z.; and Majzik, I.\n\n\n \n\n\n\n In Proceedings of the 17th Conference on Formal Methods in Computer-Aided Design, pages 176–179, 2017. \n \n\n\n\n
\n\n\n\n \n \n \"Theta: pdf\n  \n \n \n \"Theta: link\n  \n \n \n \"Theta: slides\n  \n \n \n \"Theta: video\n  \n \n\n \n \n doi\n  \n \n\n \n link\n  \n \n\n bibtex\n \n\n \n  \n \n abstract \n \n\n \n  \n \n 4 downloads\n \n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{fmcad2017,\n    author     = {T{\\'o}th, Tam{\\'a}s and Hajdu, {\\'A}kos and V{\\"o}r{\\"o}s, Andr{\\'a}s and Micskei, Zolt{\\'a}n and Majzik, Istv{\\'a}n},\n    year       = {2017},\n    title      = {Theta: a Framework for Abstraction Refinement-Based Model Checking},\n    booktitle  = {Proceedings of the 17th Conference on Formal Methods in Computer-Aided Design},\n    isbn       = {978-0-9835678-7-5},\n    pages      = {176--179},\n    doi        = {10.23919/FMCAD.2017.8102257},\n\n    type       = {Conference},\n\n    url_pdf    = {https://hajduakos.github.io/publications/fmcad2017.pdf},\n    url_link   = {http://www.cs.utexas.edu/users/hunt/FMCAD/FMCAD17/proceedings/},\n    url_slides = {https://hajduakos.github.io/publications/slides/fmcad2017.pdf},\n    url_video  = {https://oc-presentation.ltcc.tuwien.ac.at/engage/theodul/ui/core.html?id=c658c37e-ae70-11e7-a0dd-bb49f3cb440c},\n\n    abstract   = {In this paper, we present Theta, a configurable model checking framework. The goal of the framework is to support the design, execution and evaluation of abstraction refinement-based reachability analysis algorithms for models of different formalisms. It enables the definition of input formalisms, abstract domains, model interpreters, and strategies for abstraction and refinement. Currently it contains front-end support for transition systems, control flow automata and timed automata. The built-in abstract domains include predicates, explicit values, zones and their combinations, along with various refinement strategies implemented for each. The configurability of the framework allows the integration of several abstraction and refinement methods, this way supporting the evaluation of their advantages and shortcomings. We demonstrate the applicability of the framework by use cases for the safety checking of PLC, hardware, C programs and timed automata models.},\n}\n\n
\n
\n\n\n
\n In this paper, we present Theta, a configurable model checking framework. The goal of the framework is to support the design, execution and evaluation of abstraction refinement-based reachability analysis algorithms for models of different formalisms. It enables the definition of input formalisms, abstract domains, model interpreters, and strategies for abstraction and refinement. Currently it contains front-end support for transition systems, control flow automata and timed automata. The built-in abstract domains include predicates, explicit values, zones and their combinations, along with various refinement strategies implemented for each. The configurability of the framework allows the integration of several abstraction and refinement methods, this way supporting the evaluation of their advantages and shortcomings. We demonstrate the applicability of the framework by use cases for the safety checking of PLC, hardware, C programs and timed automata models.\n
\n\n\n
\n\n\n\n\n\n
\n
\n\n
\n
\n  \n 2016\n \n \n (2)\n \n \n
\n
\n \n \n
\n \n\n \n \n \n \n \n \n A Configurable CEGAR Framework with Interpolation-based Refinements.\n \n \n \n \n\n\n \n Hajdu, Á.; Tóth, T.; Vörös, A.; and Majzik, I.\n\n\n \n\n\n\n In Formal Techniques for Distributed Objects, Components and Systems, volume 9688, of Lecture Notes in Computer Science, pages 158–174. Springer, 2016.\n \n\n\n\n
\n\n\n\n \n \n \"A pdf\n  \n \n \n \"A link\n  \n \n \n \"A slides\n  \n \n\n \n \n doi\n  \n \n\n \n link\n  \n \n\n bibtex\n \n\n \n  \n \n abstract \n \n\n \n  \n \n 6 downloads\n \n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@incollection{forte2016,\n    author     = {Hajdu, {\\'A}kos and T{\\'o}th, Tam{\\'a}s and V{\\"o}r{\\"o}s, Andr{\\'a}s and Majzik, Istv{\\'a}n},\n    title      = {A Configurable {CEGAR} Framework with Interpolation-based Refinements},\n    year       = {2016},\n    booktitle  = {Formal Techniques for Distributed Objects, Components and Systems},\n    series     = {Lecture Notes in Computer Science},\n    volume     = {9688},\n    pages      = {158--174},\n    publisher  = {Springer},\n    isbn       = {978-3-319-39570-8},\n    doi        = {10.1007/978-3-319-39570-8_11},\n\n    type       = {Conference},\n\n    url_pdf    = {https://hajduakos.github.io/publications/forte2016.pdf},\n    url_link   = {http://link.springer.com/chapter/10.1007/978-3-319-39570-8_11},\n    url_slides = {https://hajduakos.github.io/publications/slides/forte2016.pdf},\n\n    abstract   = {Correctness of software components in a distributed system is a key issue to ensure overall reliability. Formal verification techniques such as model checking can show design flaws at early stages of development. Abstraction is a key technique for reducing complexity by hiding information, which is not relevant for verification. Counterexample-Guided Abstraction Refinement (CEGAR) is a verification algorithm that starts from a coarse abstraction and refines it iteratively until the proper precision is obtained. Many abstraction types and refinement strategies exist for systems with different characteristics. In this paper we show how these algorithms can be combined into a configurable CEGAR framework. In our framework we also present a new CEGAR configuration based on a combination of abstractions, being able to perform better for certain models. We demonstrate the use of the framework by comparing several configurations of the algorithms on various problems, identifying their advantages and shortcomings.},\n}\n\n
\n
\n\n\n
\n Correctness of software components in a distributed system is a key issue to ensure overall reliability. Formal verification techniques such as model checking can show design flaws at early stages of development. Abstraction is a key technique for reducing complexity by hiding information, which is not relevant for verification. Counterexample-Guided Abstraction Refinement (CEGAR) is a verification algorithm that starts from a coarse abstraction and refines it iteratively until the proper precision is obtained. Many abstraction types and refinement strategies exist for systems with different characteristics. In this paper we show how these algorithms can be combined into a configurable CEGAR framework. In our framework we also present a new CEGAR configuration based on a combination of abstractions, being able to perform better for certain models. We demonstrate the use of the framework by comparing several configurations of the algorithms on various problems, identifying their advantages and shortcomings.\n
\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n PetriDotNet 1.5: Extensible Petri Net Editor and Analyser for Education and Research.\n \n \n \n \n\n\n \n Vörös, A.; Darvas, D.; Molnár, V.; Klenik, A.; Hajdu, Á.; Jámbor, A.; Bartha, T.; and Majzik, I.\n\n\n \n\n\n\n In Application and Theory of Petri Nets and Concurrency, volume 9698, of Lecture Notes in Computer Science, pages 123–132. Springer, 2016.\n \n\n\n\n
\n\n\n\n \n \n \"PetriDotNet pdf\n  \n \n \n \"PetriDotNet link\n  \n \n\n \n \n doi\n  \n \n\n \n link\n  \n \n\n bibtex\n \n\n \n  \n \n abstract \n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@incollection{icatpn2016,\n    author    = {V{\\"o}r{\\"o}s, Andr{\\'a}s and Darvas, D{\\'a}niel and Moln{\\'a}r, Vince and Klenik, Attila and Hajdu, {\\'A}kos and J{\\'a}mbor, Attila and Bartha, Tam{\\'a}s and Majzik, Istv{\\'a}n},\n    title     = {{PetriDotNet} 1.5: Extensible {P}etri Net Editor and Analyser for Education and Research},\n    year      = {2016},\n    booktitle = {Application and Theory of Petri Nets and Concurrency},\n    series    = {Lecture Notes in Computer Science},\n    volume    = {9698},\n    pages     = {123--132},\n    publisher = {Springer},\n    isbn      = {978-3-319-39086-4},\n    doi       = {10.1007/978-3-319-39086-4_9},\n\n    type      = {Conference},\n\n    url_pdf   = {https://hajduakos.github.io/publications/icatpn2016.pdf},\n    url_link  = {http://link.springer.com/chapter/10.1007/978-3-319-39086-4_9},\n\n    abstract  = {PetriDotNet is an extensible Petri net editor and analysis tool originally developed to support the education of formal methods. The ease of use and simple extensibility fostered more and more algorithmic developments. Thanks to the continuous interest of developers (especially M.Sc. and Ph.D. students who choose PetriDotNet as the framework of their thesis project), by now PetriDotNet became an analysis platform, providing various cutting-edge model checking algorithms and stochastic analysis algorithms. As a result, industrial application of the tool also emerged in recent years. In this paper we overview the main features and the architecture of PetriDotNet, and compare it with other available tools.},\n}\n\n
\n
\n\n\n
\n PetriDotNet is an extensible Petri net editor and analysis tool originally developed to support the education of formal methods. The ease of use and simple extensibility fostered more and more algorithmic developments. Thanks to the continuous interest of developers (especially M.Sc. and Ph.D. students who choose PetriDotNet as the framework of their thesis project), by now PetriDotNet became an analysis platform, providing various cutting-edge model checking algorithms and stochastic analysis algorithms. As a result, industrial application of the tool also emerged in recent years. In this paper we overview the main features and the architecture of PetriDotNet, and compare it with other available tools.\n
\n\n\n
\n\n\n\n\n\n
\n
\n\n
\n
\n  \n 2015\n \n \n (2)\n \n \n
\n
\n \n \n
\n \n\n \n \n \n \n \n \n New search strategies for the Petri net CEGAR approach.\n \n \n \n \n\n\n \n Hajdu, Á.; Vörös, A.; and Bartha, T.\n\n\n \n\n\n\n In Application and Theory of Petri Nets and Concurrency, volume 9115, of Lecture Notes in Computer Science, pages 309–328. Springer, 2015.\n \n\n\n\n
\n\n\n\n \n \n \"New pdf\n  \n \n \n \"New link\n  \n \n \n \"New slides\n  \n \n\n \n \n doi\n  \n \n\n \n link\n  \n \n\n bibtex\n \n\n \n  \n \n abstract \n \n\n \n  \n \n 2 downloads\n \n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@incollection{icatpn2015,\n    author     = {{\\'A}kos Hajdu and Andr{\\'a}s V{\\"o}r{\\"o}s and Tam{\\'a}s Bartha},\n    title      = {New search strategies for the {P}etri net {CEGAR} approach},\n    year       = {2015},\n    booktitle  = {Application and Theory of Petri Nets and Concurrency},\n    series     = {Lecture Notes in Computer Science},\n    volume     = {9115},\n    publisher  = {Springer},\n    isbn       = {978-3-319-19488-2},\n    pages      = {309--328},\n    doi        = {10.1007/978-3-319-19488-2_16},\n\n    type       = {Conference},\n\n    url_pdf    = {https://hajduakos.github.io/publications/icatpn2015.pdf},\n    url_link   = {http://link.springer.com/chapter/10.1007/978-3-319-19488-2_16},\n    url_slides = {https://hajduakos.github.io/publications/slides/icatpn2015.pdf},\n\n    abstract   = {Petri nets are a successful formal method for the modeling and verification of asynchronous, concurrent and distributed systems. Reachability analysis can provide important information about the behavior of the model. However, reachability analysis is a computationally hard problem, especially when the state space is infinite. Abstraction-based techniques are often applied to overcome complexity. In this paper we analyze an algorithm, which uses counterexample guided abstraction refinement. This algorithm proved its efficiency on the model checking contest. We examine the algorithm from a theoretical and practical point of view. On the theoretical side, we show that the algorithm cannot decide reachability for relatively simple instances. We propose a new iteration strategy to explore the invariant space, which extends the set of decidable problems. We also give proofs on the theoretical limits of our approach. On the practical side, we examine different search strategies and we present our new, complex strategy with superior performance compared to traditional strategies. Measurements show that our new contributions perform well for traditional benchmark models as well.},\n}\n\n
\n
\n\n\n
\n Petri nets are a successful formal method for the modeling and verification of asynchronous, concurrent and distributed systems. Reachability analysis can provide important information about the behavior of the model. However, reachability analysis is a computationally hard problem, especially when the state space is infinite. Abstraction-based techniques are often applied to overcome complexity. In this paper we analyze an algorithm, which uses counterexample guided abstraction refinement. This algorithm proved its efficiency on the model checking contest. We examine the algorithm from a theoretical and practical point of view. On the theoretical side, we show that the algorithm cannot decide reachability for relatively simple instances. We propose a new iteration strategy to explore the invariant space, which extends the set of decidable problems. We also give proofs on the theoretical limits of our approach. On the practical side, we examine different search strategies and we present our new, complex strategy with superior performance compared to traditional strategies. Measurements show that our new contributions perform well for traditional benchmark models as well.\n
\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n Making the TTreeReader interface more accessible.\n \n \n \n \n\n\n \n Hajdu, Á.\n\n\n \n\n\n\n Technical Report CERN-STUDENTS-Note-2015-039, European Organization for Nuclear Research (CERN), Aug 2015.\n \n\n\n\n
\n\n\n\n \n \n \"Making pdf\n  \n \n \n \"Making link\n  \n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n  \n \n abstract \n \n\n \n  \n \n 1 download\n \n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@techreport{cern2015,\n    author      = {Hajdu, {\\'A}kos},\n    title       = {Making the {TT}ree{R}eader interface more accessible},\n    number      = {CERN-STUDENTS-Note-2015-039},\n    year        = {2015},\n    month       = {Aug},\n    institution = {European Organization for Nuclear Research (CERN)},\n\n    type        = {Tech. rep.},\n\n    url_pdf     = {http://cds.cern.ch/record/2044503/files/report.pdf},\n    url_link    = {http://cds.cern.ch/record/2044503},\n\n    abstract    = {The ROOT framework is the main data analysis tool for High Energy Physics. One of its main features is TTree, a collection type enabling efficient analysis on petabytes of data. ROOT has a new interface called TTreeReader to access data in a type-safe and efficient way. This Summer Student project aims at implementing a utility interface to generate source file skeletons as a starting point for the users. This will make the TTreeReader much more accessible for the users of ROOT.},\n}\n\n
\n
\n\n\n
\n The ROOT framework is the main data analysis tool for High Energy Physics. One of its main features is TTree, a collection type enabling efficient analysis on petabytes of data. ROOT has a new interface called TTreeReader to access data in a type-safe and efficient way. This Summer Student project aims at implementing a utility interface to generate source file skeletons as a starting point for the users. This will make the TTreeReader much more accessible for the users of ROOT.\n
\n\n\n
\n\n\n\n\n\n
\n
\n\n
\n
\n  \n 2014\n \n \n (2)\n \n \n
\n
\n \n \n
\n \n\n \n \n \n \n \n \n Extensions to the CEGAR Approach on Petri Nets.\n \n \n \n \n\n\n \n Hajdu, Á.; Vörös, A.; Bartha, T.; and Mártonka, Z.\n\n\n \n\n\n\n Acta Cybernetica, 21(3): 401–417. 2014.\n \n\n\n\n
\n\n\n\n \n \n \"Extensions pdf\n  \n \n \n \"Extensions link\n  \n \n\n \n \n doi\n  \n \n\n \n link\n  \n \n\n bibtex\n \n\n \n  \n \n abstract \n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@article{acta2014,\n    author   = {{\\'A}kos Hajdu and Andr{\\'a}s V{\\"o}r{\\"o}s and Tam{\\'a}s Bartha and Zolt{\\'a}n M{\\'a}rtonka},\n    title    = {Extensions to the {CEGAR} Approach on {P}etri Nets},\n    year     = {2014},\n    pages    = {401--417},\n    journal  = {Acta Cybernetica},\n    volume   = {21},\n    number   = {3},\n    issn     = {0324-721X},\n    doi      = {10.14232/actacyb.21.3.2014.8},\n\n    type     = {Journal},\n\n    url_pdf  = {https://hajduakos.github.io/publications/acta2014.pdf},\n    url_link = {http://www.inf.u-szeged.hu/actacybernetica/edb/vol21n3/pdf/Hajdu_2014_ActaCybernetica.pdf},\n\n    abstract = {Formal verification is becoming more prevalent and often compulsory in the safety-critical system and software development processes. Reachability analysis can provide information about safety and invariant properties of the developed system. However, checking the reachability is a computationally hard problem, especially in the case of asynchronous or infinite state systems. Petri nets are widely used for the modeling and verification of such systems. In this paper we examine a recently published approach for the reachability checking of Petri net markings. We give proofs concerning the completeness and the correctness properties of the algorithm, and we introduce algorithmic improvements. We also extend the algorithm to handle new classes of problems: submarking coverability and reachability of Petri nets with inhibitor arcs.},\n}\n\n
\n
\n\n\n
\n Formal verification is becoming more prevalent and often compulsory in the safety-critical system and software development processes. Reachability analysis can provide information about safety and invariant properties of the developed system. However, checking the reachability is a computationally hard problem, especially in the case of asynchronous or infinite state systems. Petri nets are widely used for the modeling and verification of such systems. In this paper we examine a recently published approach for the reachability checking of Petri net markings. We give proofs concerning the completeness and the correctness properties of the algorithm, and we introduce algorithmic improvements. We also extend the algorithm to handle new classes of problems: submarking coverability and reachability of Petri nets with inhibitor arcs.\n
\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n Petri Net Based Trajectory Optimization.\n \n \n \n \n\n\n \n Hajdu, Á.; Német, R.; Varró-Gyapay, S.; and Vörös, A.\n\n\n \n\n\n\n In ASCONIKK 2014: Extended Abstracts. Future Internet Services, pages 11–19, 2014. University of Pannonia\n \n\n\n\n
\n\n\n\n \n \n \"Petri pdf\n  \n \n \n \"Petri link\n  \n \n \n \"Petri slides\n  \n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n  \n \n abstract \n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{asconikk2014,\n    author     = {{\\'A}kos Hajdu and R{\\'o}bert N{\\'e}met and Szilvia Varr{\\'o}-Gyapay and Andr{\\'a}s V{\\"o}r{\\"o}s},\n    title      = {{P}etri Net Based Trajectory Optimization},\n    booktitle  = {ASCONIKK 2014: Extended Abstracts. Future Internet Services},\n    year       = {2014},\n    location   = {Veszpr\\'em, Hungary},\n    publisher  = {University of Pannonia},\n    pages      = {11--19},\n    isbn       = {978-963-396-047-9},\n\n    type       = {Conference},\n\n    url_pdf    = {https://hajduakos.github.io/publications/vocal2014.pdf},\n    url_link   = {http://nikk.mik.uni-pannon.hu/images/II_final_.pdf},\n    url_slides = {https://hajduakos.github.io/publications/slides/vocal2014.pdf},\n\n    abstract   = {Optimization problems are becoming more prevalent in the design of complex systems. Petri nets are widely used for the modeling of such systems. An optimization problem can be translated to find an optimal trajectory where a cost is assigned to each step. The reachability problem of Petri nets answers whether a given state is reachable from the initial state. However, reachability analysis is a computationally hard problem, especially in the case of asynchronous or infinite state systems. In this paper we examine a recently published algorithm that solves reachability using abstraction methods and we extend this approach to be able to handle optimal trajectory problems.},\n}\n\n
\n
\n\n\n
\n Optimization problems are becoming more prevalent in the design of complex systems. Petri nets are widely used for the modeling of such systems. An optimization problem can be translated to find an optimal trajectory where a cost is assigned to each step. The reachability problem of Petri nets answers whether a given state is reachable from the initial state. However, reachability analysis is a computationally hard problem, especially in the case of asynchronous or infinite state systems. In this paper we examine a recently published algorithm that solves reachability using abstraction methods and we extend this approach to be able to handle optimal trajectory problems.\n
\n\n\n
\n\n\n\n\n\n
\n
\n\n
\n
\n  \n 2013\n \n \n (1)\n \n \n
\n
\n \n \n
\n \n\n \n \n \n \n \n \n Extensions to the CEGAR Approach on Petri Nets.\n \n \n \n \n\n\n \n Hajdu, Á.; Vörös, A.; Bartha, T.; and Mártonka, Z.\n\n\n \n\n\n\n In Proceedings of the 13th Symposium on Programming Languages and Software Tools, pages 274–288, 2013. University of Szeged\n \n\n\n\n
\n\n\n\n \n \n \"Extensions pdf\n  \n \n \n \"Extensions link\n  \n \n \n \"Extensions slides\n  \n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n  \n \n abstract \n \n\n \n  \n \n 1 download\n \n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{splst2013,\n    author     = {{\\'A}kos Hajdu and Andr{\\'a}s V{\\"o}r{\\"o}s and Tam{\\'a}s Bartha and Zolt{\\'a}n M{\\'a}rtonka},\n    title      = {Extensions to the {CEGAR} Approach on {P}etri Nets},\n    year       = {2013},\n    pages      = {274--288},\n    publisher  = {University of Szeged},\n    booktitle  = {Proceedings of the 13th Symposium on Programming Languages and Software Tools},\n    isbn       = {978-963-306-228-9},\n\n    type       = {Conference},\n\n    url_pdf    = {https://hajduakos.github.io/publications/splst2013.pdf},\n    url_link   = {http://www.inf.u-szeged.hu/projectdirs/splst13/splst13proc.pdf},\n    url_slides = {https://hajduakos.github.io/publications/slides/splst2013.pdf},\n\n    abstract   = {Formal verification is becoming more prevalent and often compulsory in the safety-critical system and software development processes. Reachability analysis can provide information about safety and invariant properties of the developed system. However, checking the reachability is a computationally hard problem, especially in the case of asynchronous or infinite state systems. Petri nets are widely used for the modeling and verification of such systems. In this paper we examine a recently published approach for the reachability checking of Petri net markings. We give proofs concerning the completeness and the correctness properties of the algorithm, and we introduce algorithmic improvements. We also extend the algorithm to handle new classes of problems: submarking coverability and reachability of Petri nets with inhibitor arcs.},\n}\n\n
\n
\n\n\n
\n Formal verification is becoming more prevalent and often compulsory in the safety-critical system and software development processes. Reachability analysis can provide information about safety and invariant properties of the developed system. However, checking the reachability is a computationally hard problem, especially in the case of asynchronous or infinite state systems. Petri nets are widely used for the modeling and verification of such systems. In this paper we examine a recently published approach for the reachability checking of Petri net markings. We give proofs concerning the completeness and the correctness properties of the algorithm, and we introduce algorithmic improvements. We also extend the algorithm to handle new classes of problems: submarking coverability and reachability of Petri nets with inhibitor arcs.\n
\n\n\n
\n\n\n\n\n\n
\n
\n\n\n\n\n
\n\n\n \n\n \n \n \n \n\n
\n"}; document.write(bibbase_data.data);