@CONFERENCE{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 Bajczi, Levente and Ádám, Zsófia and Vörös, András},
	booktitle = {Proceedings 18th International Workshop on Logical and Semantic Frameworks, with Applications and 10th Workshop on Horn Clauses for Verification and Synthesis},
	doi = {10.4204/EPTCS.402.11},
	unique-id = {33784283},
	year = {2023},
	pages = {105-117},
	orcid-numbers = {Dobos-Kovács, Mihály/0000-0002-0064-2965; Bajczi, Levente/0000-0002-6551-5860; Ádám, Zsófia/0000-0003-2354-1750}
}

@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: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}
}

@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: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}
}

@article{MTMT:31374125,
	title = {Simulation-based Safety Assessment of High-level Reliability Models},
	url = {https://m2.mtmt.hu/api/publication/31374125},
	author = {Nagy, Simon József and Graics, Bence and Marussy, Kristóf and Vörös, András},
	doi = {10.4204/EPTCS.316.9},
	journal-iso = {ELECTRON PROC THEOR COMPUT SCI},
	journal = {ELECTRONIC PROCEEDINGS IN THEORETICAL COMPUTER SCIENCE},
	volume = {316},
	unique-id = {31374125},
	abstract = {Systems engineering approaches use high-level models to capture the architecture and behavior of the system. However, when safety engineers conduct safety and reliability analysis, they have to create formal models, such as fault-trees, according to the behavior described by the high-level engineering models and environmental/fault assumptions. Instead of creating low-level analysis models, our approach builds on engineering models in safety analysis by exploiting the simulation capabilities of recent probabilistic programming and simulation advancements. Thus, it could be applied in accordance with standards and best practices for the analysis of a critical automotive system as part of an industrial collaboration, while leveraging high-level block diagrams and statechart models created by engineers. We demonstrate the applicability of our approach in a case study adapted from the automotive system from the collaboration},
	year = {2020},
	eissn = {2075-2180},
	pages = {240-260},
	orcid-numbers = {Graics, Bence/0000-0001-5546-5970; Marussy, Kristóf/0000-0002-9135-8256}
}

@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}
}