@inproceedings{MTMT:35500643,
	title = {Towards the Formal Verification of SysML v2 Models},
	url = {https://m2.mtmt.hu/api/publication/35500643},
	author = {Molnár, Vince and Graics, Bence and Vörös, András and Tonetta, Stefano and Cristoforetti, Luca and Kimberly, Greg and Dyer, Pamela and Giammarco, Kristin and Koethe, Manfred and Hester, John and Smith, Jamie and Grimm, Christoph},
	booktitle = {MODELS Companion '24: Proceedings of the ACM/IEEE 27th International Conference on Model Driven Engineering Languages and Systems},
	doi = {10.1145/3652620.3687820},
	unique-id = {35500643},
	year = {2024},
	pages = {1086-1095},
	orcid-numbers = {Molnár, Vince/0000-0002-8204-7595; Graics, Bence/0000-0001-5546-5970; Tonetta, Stefano/0000-0001-9091-7899; Cristoforetti, Luca/0000-0002-8519-6342; Kimberly, Greg/0009-0008-2192-4276; Dyer, Pamela/0009-0004-7603-4327; Giammarco, Kristin/0000-0002-8859-8320; Koethe, Manfred/0009-0003-1223-3530; Hester, John/0009-0007-7032-0340; Smith, Jamie/0009-0009-3945-5639; Grimm, Christoph/0000-0002-5930-7563}
}

@article{MTMT:33784283,
	title = {Bottoms Up for CHCs: Novel Transformation of Linear Constrained Horn Clauses to Software Verification},
	url = {https://m2.mtmt.hu/api/publication/33784283},
	author = {Somorjai, Márk and Dobos-Kovács, Mihály and Ádám, Zsófia and Bajczi, Levente and Vörös, András},
	doi = {10.4204/EPTCS.402.11},
	journal-iso = {ELECTRON PROC THEOR COMPUT SCI},
	journal = {ELECTRONIC PROCEEDINGS IN THEORETICAL COMPUTER SCIENCE},
	volume = {402},
	unique-id = {33784283},
	abstract = {Constrained Horn Clauses (CHCs) have conventionally been used as a low-level representation in formal verification. Most existing solvers use a diverse set of specialized techniques, including direct state space traversal or under-approximating abstraction, necessitating purpose-built complex algorithms. Other solvers successfully simplified the verification workflow by translating the problem to inputs for other verification tasks, leveraging the strengths of existing algorithms. One such approach transforms the CHC problem into a recursive program roughly emulating a top-down solver for the deduction task; and verifying the reachability of a safety violation specified as a control location. We propose an alternative bottom-up approach for linear CHCs, and evaluate the two options in the open-source model checking framework THETA on both synthetic and industrial examples. We find that there is a more than twofold increase in the number of solved tasks when the novel bottom-up approach is used in the verification workflow, in contrast with the top-down technique. © Márk Somorjai et al.},
	year = {2024},
	eissn = {2075-2180},
	pages = {105-117},
	orcid-numbers = {Dobos-Kovács, Mihály/0000-0002-0064-2965; Ádám, Zsófia/0000-0003-2354-1750; Bajczi, Levente/0000-0002-6551-5860}
}

@inproceedings{MTMT:33575796,
	title = {Evaluation of SMT solvers in abstraction-based software model checking},
	url = {https://m2.mtmt.hu/api/publication/33575796},
	author = {Dobos-Kovács, Mihály and Vörös, András},
	booktitle = {Proceedings of the 11th Latin-American Symposium on Dependable Computing, LADC '22},
	doi = {10.1145/3569902.3570187},
	unique-id = {33575796},
	year = {2022},
	pages = {109-116},
	orcid-numbers = {Dobos-Kovács, Mihály/0000-0002-0064-2965}
}

@inproceedings{MTMT:32679018,
	title = {Dependability Modeling of Cyber-Physical Systems in the Gamma Framework},
	url = {https://m2.mtmt.hu/api/publication/32679018},
	author = {Szabó, Richárd and Vörös, András},
	booktitle = {Proceedings of the 29th Minisymposium of the Department of Measurement and Information Systems Budapest University of Technology and Economics},
	unique-id = {32679018},
	year = {2022},
	pages = {20-23},
	orcid-numbers = {Szabó, Richárd/0000-0003-1307-3332}
}

@inproceedings{MTMT:32527201,
	title = {Towards Interactive Learning for Model-based Software Engineering},
	url = {https://m2.mtmt.hu/api/publication/32527201},
	author = {Barcsa-Szabó, Áron and Várady, Balázs and Farkas, Rebeka and Molnár, Vince and Vörös, András},
	booktitle = {Proceedings of the 28th PhD Mini-Symposium},
	unique-id = {32527201},
	abstract = {Model-based technologies improve the efficiency of the design and development of IT systems by making it possible to automate verification, code generation and system analysis based on a formal model. A simple way of describing the behavior of systems is state-based modeling, which - due to the advancements of formal analysis techniques in recent years - can be widely and effectively utilized when analyzing systems. A possible way of synthesizing such models is to apply active automata learning algorithms. Acquiring a correct formal model of a system can be challenging because of the different theoretical and practical obstacles of both manual and automated approaches. We propose a semi-automated solution, that applies automata learning to provide an interactive environment for model development.},
	year = {2021},
	pages = {28-31},
	orcid-numbers = {Molnár, Vince/0000-0002-8204-7595}
}

@inproceedings{MTMT:31868691,
	title = {Model-Driven Development of Heterogeneous Cyber-Physical Systems},
	url = {https://m2.mtmt.hu/api/publication/31868691},
	author = {Csuvarszki, János Csanád and Graics, Bence and Vörös, András},
	booktitle = {Proceedings of the 28th PhD Mini-Symposium},
	unique-id = {31868691},
	abstract = {Cyber-physical systems (CPS) are becoming more prevalent for the reliable execution of critical tasks, e.g., in the aerospace and medical fields. The development of such systems is challenging, due to the heterogeneity of the components ranging from sensors and embedded controllers to cloud solutions. Model-driven approaches can provide a high-level abstraction to combat the challenges. This paper proposes a model-driven development approach supporting the precise modeling of CPS and the automatic derivation of implementation from the resulting models. The approach introduces a composition semantics tailored to heterogeneous architectures for the precise description of component interactions. Automated code generators allow the execution of standalone software components on real-time controllers and support the synthesis of standalone hardware components, enabling both the derivation of embedded software and the description of logical circuit behavior. Component interactions are supported by multiple communication solutions generally used in critical, real-time embedded systems. The approach is implemented in the Gamma framework and its applicability is demonstrated in two case studies.},
	year = {2021},
	pages = {24-27},
	orcid-numbers = {Graics, Bence/0000-0001-5546-5970}
}

@inproceedings{MTMT:32678888,
	title = {Bitvector Support in the Theta Formal Verification Framework},
	url = {https://m2.mtmt.hu/api/publication/32678888},
	author = {Dobos-Kovács, Mihály and Hajdu, Ákos and Vörös, András},
	booktitle = {2021 10th Latin-American Symposium on Dependable Computing (LADC)},
	doi = {10.1109/LADC53747.2021.9672595},
	unique-id = {32678888},
	year = {2021},
	pages = {01-08},
	orcid-numbers = {Dobos-Kovács, Mihály/0000-0002-0064-2965; Hajdu, Ákos/0000-0001-8001-8865}
}

@inproceedings{MTMT:32678847,
	title = {Demonstrator for dependable edge-based cyber-physical systems},
	url = {https://m2.mtmt.hu/api/publication/32678847},
	author = {Nagy, Simon József and Szabó, Richárd and Vajda, Mate Levente and Vörös, András},
	booktitle = {2021 10th Latin-American Symposium on Dependable Computing (LADC)},
	doi = {10.1109/LADC53747.2021.9672569},
	unique-id = {32678847},
	year = {2021},
	pages = {1-8},
	orcid-numbers = {Szabó, Richárd/0000-0003-1307-3332}
}

@inproceedings{MTMT:32678929,
	title = {Towards formally analyzed Cyber-Physical Systems},
	url = {https://m2.mtmt.hu/api/publication/32678929},
	author = {Szabó, Richárd and Vörös, András},
	booktitle = {Student Forum Proceedings- EDCC 2021},
	unique-id = {32678929},
	year = {2021},
	pages = {1-4},
	orcid-numbers = {Szabó, Richárd/0000-0003-1307-3332}
}

@article{MTMT:31343505,
	title = {Mixed-Semantics Composition of Statecharts for the Component-Based Design of Reactive Systems},
	url = {https://m2.mtmt.hu/api/publication/31343505},
	author = {Graics, Bence and Molnár, Vince and Vörös, András and Majzik, István and Varró, Dániel},
	doi = {10.1007/s10270-020-00806-5},
	journal-iso = {SOFTW SYST MODEL},
	journal = {SOFTWARE AND SYSTEMS MODELING},
	volume = {19},
	unique-id = {31343505},
	issn = {1619-1366},
	abstract = {The increasing complexity of reactive systems can be mitigated with the use of components and composition languages in model-driven engineering. Designing composition languages is a challenge itself as both practical applicability (support for different composition approaches in various application domains), and precise formal semantics (support for verification and code generation) have to be taken into account. In our Gamma Statechart Composition Framework, we designed and implemented a composition language for the synchronous, cascade synchronous, and asynchronous composition of statechart-based reactive components. We formalized the semantics of this composition language that provides the basis for generating composition-related Java source code as well as mapping the composite system to a back-end model checker for formal verification and model-based test case generation. In this paper, we present the composition language with its formal semantics, putting special emphasis on design decisions related to the language and their effects on verifiability and applicability. Furthermore, we demonstrate the design and verification functionality of the composition framework by presenting case studies from the cyber-physical system domain.},
	keywords = {Formal Semantics; formal verification; Component-based design; composition language; statecharts},
	year = {2020},
	eissn = {1619-1374},
	pages = {1483-1517},
	orcid-numbers = {Graics, Bence/0000-0001-5546-5970; Molnár, Vince/0000-0002-8204-7595; Varró, Dániel/0000-0002-8790-252X}
}