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://mondokm.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://mondokm.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://mondokm.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
  2. update the BibBase URL\n in your page the same way you did when you initially set up\n this page.\n
    3. \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 (3)\n \n \n
\n
\n \n \n
\n \n\n \n \n \n \n \n \n Model-Based Testing of Asynchronously Communicating Distributed Controllers.\n \n \n \n \n\n\n \n Graics, B.; Mondok, M.; Molnár, V.; and Majzik, I.\n\n\n \n\n\n\n In Cámara, J.; and Jongmans, S., editor(s), Formal Aspects of Component Software, pages 23–44, Cham, 2024. Springer Nature Switzerland\n \n\n\n\n
\n\n\n\n \n \n \"Model-BasedPaper\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 
@InProceedings{facs23,\nauthor="Graics, Bence\nand Mondok, Mil{\\'a}n\nand Moln{\\'a}r, Vince\nand Majzik, Istv{\\'a}n",\neditor="C{\\'a}mara, Javier\nand Jongmans, Sung-Shik",\ntitle="Model-Based Testing of Asynchronously Communicating Distributed Controllers",\nbooktitle="Formal Aspects of Component Software",\nyear="2024",\npublisher="Springer Nature Switzerland",\naddress="Cham",\npages="23--44",\nabstract="Programmable controllers are gaining prevalence even in distributed safety-critical infrastructures, e.g., in the railway and aerospace industries. Such systems are generally integrated using multiple loosely-coupled reactive components and must satisfy various critical requirements. Thus, their systematic testing is an essential task, which can be encumbered by their distributed characteristics. This paper presents a model-based integration test generation approach leveraging hidden formal methods based on the collaborating statechart models of the components. Statecharts can be integrated using various composition modes (e.g., synchronous and asynchronous) and then transformed (via a symbolic transition systems formalism -- XSTS) into the input formalisms of model checker back-ends, namely UPPAAL, Theta and Spin in an automated way. The model checkers are utilized for test generation based on multiple coverage criteria. The approach is implemented in our open source Gamma Statechart Composition Framework and evaluated on industrial-scale distributed controller subsystems from the railway industry.",\nisbn="978-3-031-52183-6",\nurl="https://link.springer.com/chapter/10.1007/978-3-031-52183-6_2",\ndoi="10.1007/978-3-031-52183-6_2"\n}\n\n
\n
\n\n\n
\n Programmable controllers are gaining prevalence even in distributed safety-critical infrastructures, e.g., in the railway and aerospace industries. Such systems are generally integrated using multiple loosely-coupled reactive components and must satisfy various critical requirements. Thus, their systematic testing is an essential task, which can be encumbered by their distributed characteristics. This paper presents a model-based integration test generation approach leveraging hidden formal methods based on the collaborating statechart models of the components. Statecharts can be integrated using various composition modes (e.g., synchronous and asynchronous) and then transformed (via a symbolic transition systems formalism – XSTS) into the input formalisms of model checker back-ends, namely UPPAAL, Theta and Spin in an automated way. The model checkers are utilized for test generation based on multiple coverage criteria. The approach is implemented in our open source Gamma Statechart Composition Framework and evaluated on industrial-scale distributed controller subsystems from the railway industry.\n
\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n Theta: Abstraction Based Techniques for Verifying Concurrency (Competition Contribution).\n \n \n \n \n\n\n \n Bajczi, L.; Telbisz, C.; Somorjai, M.; Ádám, Z.; Dobos-Kovács, M.; Szekeres, D.; Mondok, M.; and Molnár, V.\n\n\n \n\n\n\n In Finkbeiner, B.; and Kovács, L., editor(s), Tools and Algorithms for the Construction and Analysis of Systems, pages 412–417, Cham, 2024. Springer Nature Switzerland\n \n\n\n\n
\n\n\n\n \n \n \"Theta:Paper\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{svcomp24-theta,\nauthor="Bajczi, Levente\nand Telbisz, Csan{\\'a}d\nand Somorjai, M{\\'a}rk\nand {\\'A}d{\\'a}m, Zs{\\'o}fia\nand Dobos-Kov{\\'a}cs, Mih{\\'a}ly\nand Szekeres, D{\\'a}niel\nand Mondok, Mil{\\'a}n\nand Moln{\\'a}r, Vince",\neditor="Finkbeiner, Bernd\nand Kov{\\'a}cs, Laura",\ntitle="Theta: Abstraction Based Techniques for Verifying Concurrency (Competition Contribution)",\nbooktitle="Tools and Algorithms for the Construction and Analysis of Systems",\nyear="2024",\npublisher="Springer Nature Switzerland",\naddress="Cham",\npages="412--417",\nabstract="Theta is a model checking framework, with a strong emphasis on effectively handling concurrency in software using abstraction refinement algorithms. In SV-COMP 2024, we use 1) an abstraction-aware partial order reduction; 2) a dynamic statement reduction technique; and 3) enhanced support for call stacks to handle recursive programs. We integrate these techniques in an improved architecture with inherent support for portfolio-based verification using dynamic algorithm selection, with a diverse selection of supported SMT solvers as well. In this paper we detail the advances of Theta regarding concurrent and recursive software support.",\nisbn="978-3-031-57256-2",\nurl="https://link.springer.com/chapter/10.1007/978-3-031-57256-2_30",\ndoi="10.1007/978-3-031-57256-2_30"\n}\n\n
\n
\n\n\n
\n Theta is a model checking framework, with a strong emphasis on effectively handling concurrency in software using abstraction refinement algorithms. In SV-COMP 2024, we use 1) an abstraction-aware partial order reduction; 2) a dynamic statement reduction technique; and 3) enhanced support for call stacks to handle recursive programs. We integrate these techniques in an improved architecture with inherent support for portfolio-based verification using dynamic algorithm selection, with a diverse selection of supported SMT solvers as well. In this paper we detail the advances of Theta regarding concurrent and recursive software support.\n
\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n EmergenTheta: Verification Beyond Abstraction Refinement (Competition Contribution).\n \n \n \n \n\n\n \n Bajczi, L.; Szekeres, D.; Mondok, M.; Ádám, Z.; Somorjai, M.; Telbisz, C.; Dobos-Kovács, M.; and Molnár, V.\n\n\n \n\n\n\n In Finkbeiner, B.; and Kovács, L., editor(s), Tools and Algorithms for the Construction and Analysis of Systems, pages 371–375, Cham, 2024. Springer Nature Switzerland\n \n\n\n\n
\n\n\n\n \n \n \"EmergenTheta:Paper\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 
@InProceedings{svcomp24-emergentheta,\nauthor="Bajczi, Levente\nand Szekeres, D{\\'a}niel\nand Mondok, Mil{\\'a}n\nand {\\'A}d{\\'a}m, Zs{\\'o}fia\nand Somorjai, M{\\'a}rk\nand Telbisz, Csan{\\'a}d\nand Dobos-Kov{\\'a}cs, Mih{\\'a}ly\nand Moln{\\'a}r, Vince",\neditor="Finkbeiner, Bernd\nand Kov{\\'a}cs, Laura",\ntitle="EmergenTheta: Verification Beyond Abstraction Refinement (Competition Contribution)",\nbooktitle="Tools and Algorithms for the Construction and Analysis of Systems",\nyear="2024",\npublisher="Springer Nature Switzerland",\naddress="Cham",\npages="371--375",\nabstract="Theta is a model checking framework conventionally based on abstraction refinement techniques. While abstraction is useful for a large number of verification problems, the over-reliance on the technique led to Theta being unable to meaningfully adapt. Identifying this problem in previous years of SV-COMP has led us to create EmergenTheta, a sandbox for the new approaches we want Theta to support. By differentiating between mature and emerging techniques, we can experiment more freely without hurting the reliability of the overall framework. In this paper we detail the development route to EmergenTheta, and its first debut on SV-COMP'24 in the ReachSafety category.",\nisbn="978-3-031-57256-2",\nurl="https://link.springer.com/chapter/10.1007/978-3-031-57256-2_23",\ndoi="10.1007/978-3-031-57256-2_23"\n}\n\n\n
\n
\n\n\n
\n Theta is a model checking framework conventionally based on abstraction refinement techniques. While abstraction is useful for a large number of verification problems, the over-reliance on the technique led to Theta being unable to meaningfully adapt. Identifying this problem in previous years of SV-COMP has led us to create EmergenTheta, a sandbox for the new approaches we want Theta to support. By differentiating between mature and emerging techniques, we can experiment more freely without hurting the reliability of the overall framework. In this paper we detail the development route to EmergenTheta, and its first debut on SV-COMP'24 in the ReachSafety category.\n
\n\n\n
\n\n\n\n\n\n
\n
\n\n
\n
\n  \n 2020\n \n \n (1)\n \n \n
\n
\n \n \n
\n \n\n \n \n \n \n \n \n Abstraction-Based Model Checking of Linear Temporal Properties.\n \n \n \n \n\n\n \n Mondok, M.; and Vörös, A.\n\n\n \n\n\n\n In Renczes, B., editor(s), Proceedings of the 27th PhD Mini-Symposium, pages 29–32, 2020. Budapest University of Technology and Economics, Department of Measurement and Information Systems\n \n\n\n\n
\n\n\n\n \n \n \"Abstraction-Based 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 17 downloads\n \n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n 
@inproceedings{minisy2020mm,\n    author     = {Mondok, Mil\\'an and V\\"or\\"os, Andr\\'as},\n    title      = {Abstraction-Based Model Checking of Linear Temporal Properties},\n    year       = {2020},\n    booktitle  = {Proceedings of the 27th PhD Mini-Symposium},\n    location   = {Budapest, Hungary},\n    publisher  = {Budapest University of Technology and Economics, Department of Measurement and Information Systems},\n    editor     = {Renczes, Bal\\'azs},\n    pages      = {29--32},\n\n    type       = {Local event},\n    url_pdf    = {publications/minisy2020mm.pdf},\n    abstract   = {Even though the expressiveness of linear temporal logic (LTL) supports engineering application, model checking of such properties is a computationally complex task and state space explosion often hinders successful verification. LTL model checking consists of constructing automata from the property and the system, generating the synchronous product of the two automata and checking its language emptiness. We propose a novel LTL model checking algorithm that uses abstraction to tackle the challenge of state space explosion. This algorithm combines the advantages of two commonly used model checking approaches, counterexample-guided abstraction refinement and automata theoretic LTL model checking. The main challenge in combining these is the refinement of "lasso"-shaped counterexamples, for which task we propose a novel refinement strategy based on interpolation.},\n}\n\n
\n
\n\n\n
\n Even though the expressiveness of linear temporal logic (LTL) supports engineering application, model checking of such properties is a computationally complex task and state space explosion often hinders successful verification. LTL model checking consists of constructing automata from the property and the system, generating the synchronous product of the two automata and checking its language emptiness. We propose a novel LTL model checking algorithm that uses abstraction to tackle the challenge of state space explosion. This algorithm combines the advantages of two commonly used model checking approaches, counterexample-guided abstraction refinement and automata theoretic LTL model checking. The main challenge in combining these is the refinement of \"lasso\"-shaped counterexamples, for which task we propose a novel refinement strategy based on interpolation.\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);