@article{MTMT:34768972,
	title = {ConcurrentWitness2Test: Test-Harnessing the Power of Concurrency (Competition Contribution)},
	url = {https://m2.mtmt.hu/api/publication/34768972},
	author = {Bajczi, Levente and Ádám, Zsófia and Micskei, Zoltán Imre},
	doi = {10.1007/978-3-031-57256-2_16},
	journal-iso = {LNCS},
	journal = {LECTURE NOTES IN COMPUTER SCIENCE},
	volume = {14572},
	unique-id = {34768972},
	issn = {0302-9743},
	abstract = {ConcurrentWitness2Test is a violation witness validator for concurrent software. Taking both nondeterminism of data and interleaving-based nondeterminism into account, the tool aims to use the metadata described in the violation witnesses to synthesize an executable test harness. While plagued by some initial challenges yet to overcome, the validation performance of ConcurrentWitness2Test corroborates the usefulness of the proposed approach.},
	year = {2024},
	eissn = {1611-3349},
	pages = {330-334},
	orcid-numbers = {Bajczi, Levente/0000-0002-6551-5860; Ádám, Zsófia/0000-0003-2354-1750; Micskei, Zoltán Imre/0000-0003-1846-261X}
}

@article{MTMT:34768428,
	title = {Theta: Abstraction Based Techniques for Verifying Concurrency (Competition Contribution)},
	url = {https://m2.mtmt.hu/api/publication/34768428},
	author = {Bajczi, Levente and Telbisz, Csanád Ferenc and Somorjai, Márk and Ádám, Zsófia and Dobos-Kovács, Mihály and Szekeres, Dániel and Mondok, Milán and Molnár, Vince},
	doi = {10.1007/978-3-031-57256-2_30},
	journal-iso = {LNCS},
	journal = {LECTURE NOTES IN COMPUTER SCIENCE},
	volume = {14572},
	unique-id = {34768428},
	issn = {0302-9743},
	abstract = {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.},
	year = {2024},
	eissn = {1611-3349},
	pages = {412-417},
	orcid-numbers = {Bajczi, Levente/0000-0002-6551-5860; Telbisz, Csanád Ferenc/0000-0002-6260-5908; Ádám, Zsófia/0000-0003-2354-1750; Dobos-Kovács, Mihály/0000-0002-0064-2965; Szekeres, Dániel/0000-0002-2912-028X; Mondok, Milán/0000-0001-5396-2172; Molnár, Vince/0000-0002-8204-7595}
}

@article{MTMT:34768422,
	title = {EmergenTheta: Verification Beyond Abstraction Refinement (Competition Contribution)},
	url = {https://m2.mtmt.hu/api/publication/34768422},
	author = {Bajczi, Levente and Szekeres, Dániel and Mondok, Milán and Ádám, Zsófia and Somorjai, Márk and Telbisz, Csanád Ferenc and Dobos-Kovács, Mihály and Molnár, Vince},
	doi = {10.1007/978-3-031-57256-2_23},
	journal-iso = {LNCS},
	journal = {LECTURE NOTES IN COMPUTER SCIENCE},
	volume = {14572},
	unique-id = {34768422},
	issn = {0302-9743},
	abstract = {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.},
	year = {2024},
	eissn = {1611-3349},
	pages = {371-375},
	orcid-numbers = {Bajczi, Levente/0000-0002-6551-5860; Szekeres, Dániel/0000-0002-2912-028X; Mondok, Milán/0000-0001-5396-2172; Ádám, Zsófia/0000-0003-2354-1750; Telbisz, Csanád Ferenc/0000-0002-6260-5908; Dobos-Kovács, Mihály/0000-0002-0064-2965; Molnár, Vince/0000-0002-8204-7595}
}

@article{MTMT:34727894,
	title = {Application of Mutation testing in Safety-Critical Embedded Systems: A Case Study},
	url = {https://m2.mtmt.hu/api/publication/34727894},
	author = {Serban, Andrada Alexia and Micskei, Zoltán Imre},
	doi = {10.12700/APH.21.8.2024.8.5},
	journal-iso = {ACTA POLYTECH HUNG},
	journal = {ACTA POLYTECHNICA HUNGARICA},
	volume = {21},
	unique-id = {34727894},
	issn = {1785-8860},
	year = {2024},
	eissn = {1785-8860},
	pages = {87-106},
	orcid-numbers = {Micskei, Zoltán Imre/0000-0003-1846-261X}
}

@article{MTMT:34560592,
	title = {Transaction Conflict Control in Hyperledger Fabric: a Taxonomy, Gaps, and Design for Conflict Prevention},
	url = {https://m2.mtmt.hu/api/publication/34560592},
	author = {Debreczeni, Máté Imre and Klenik, Attila and Kocsis, Imre},
	doi = {10.1109/ACCESS.2024.3361318},
	journal-iso = {IEEE ACCESS},
	journal = {IEEE ACCESS},
	volume = {12},
	unique-id = {34560592},
	issn = {2169-3536},
	abstract = {The execute-order-validate approach to blockchain consensus, most notably implemented by Hyperledger Fabric, facilitates highly scalable execution of smart contract – in Fabric terminology, ”chaincode” – invocations in cross-organizational blockchains; at the expense of requiring multi-version concurrency control conflict handling during block validation. Consequently, the system-level goodput can be significantly lower than throughput. Although several solutions have been proposed for handling and avoiding conflicts in Hyperledger Fabric, a systematic and holistic approach is missing. We introduce the notion of conflict-controlled operation, propose a novel taxonomy of its means based on the codified principles of dependable computing and categorize the known approaches. Based on this taxonomy, we identified the critical gaps in the state-of-the-art. Design-time conflict prevention is one such gap, and we propose the application of a model-driven engineering process for this purpose. For the last, storage mapping stage of the process, we propose entity attribute partitioning for conflict prevention, describe a data mapper-style chaincode layer and empirically evaluate our solution. Authors},
	keywords = {taxonomy; peer-to-peer computing; SYSTEMATICS; Concurrency control; Fabrics; Peer to peer networks; Taxonomies; Digital storage; blockchain; systematic; smart contracts; Model-Driven engineering; smart contract; Dependable computing; Distributed ledger; Blockchains; Hyperledger fabric; Block-chain; Goodput; Good put; multi-version; Hyperledg fabric; attribute affinity; multi-version concurrency control; Attribute affinity; Multi-version concurrency control},
	year = {2024},
	eissn = {2169-3536},
	pages = {18987-19008},
	orcid-numbers = {Klenik, Attila/0000-0003-2051-2823}
}

@inproceedings{MTMT:34504488,
	title = {Model-Based Testing of Asynchronously Communicating Distributed Controllers},
	url = {https://m2.mtmt.hu/api/publication/34504488},
	author = {Graics, Bence and Mondok, Milán and Molnár, Vince and Majzik, István},
	booktitle = {Formal Aspects of Component Software},
	doi = {10.1007/978-3-031-52183-6_2},
	unique-id = {34504488},
	year = {2024},
	pages = {23-44},
	orcid-numbers = {Graics, Bence/0000-0001-5546-5970; Mondok, Milán/0000-0001-5396-2172; Molnár, Vince/0000-0002-8204-7595}
}

@article{MTMT:34375495,
	title = {Concretization of Abstract Traffic Scene Specifications Using Metaheuristic Search},
	url = {https://m2.mtmt.hu/api/publication/34375495},
	author = {Babikian, Aren A. and Semeráth, Oszkár and Varró, Dániel},
	doi = {10.1109/TSE.2023.3331254},
	journal-iso = {IEEE T SOFTWARE ENG},
	journal = {IEEE TRANSACTIONS ON SOFTWARE ENGINEERING},
	volume = {50},
	unique-id = {34375495},
	issn = {0098-5589},
	abstract = {Existing safety assurance approaches for autonomous vehicles (AVs) perform system-level safety evaluation by placing the AV-under-test in challenging traffic scenarios captured by abstract scenario specifications and investigated in realistic traffic simulators. As a first step towards scenario-based testing of AVs, the initial scene of a traffic scenario must be concretized. In this context, the scene concretization challenge takes as input a high-level specification of abstract traffic scenes and aims to map them to concrete scenes where exact numeric initial values are defined for each attribute of a vehicle (e.g. position or velocity). In this paper, we propose a traffic scene concretization approach that places vehicles on realistic road maps such that they satisfy an extensible set of abstract constraints defined by an expressive scene specification language which also supports static detection of inconsistencies. Then, abstract constraints are mapped to corresponding numeric constraints, which are solved by metaheuristic search with customizable objective functions and constraint aggregation strategies. We conduct a series of experiments over three realistic road maps to compare eight configurations of our approach with three variations of the state-of-the-art Scenic tool, and to evaluate its scalability.},
	keywords = {Multiobjective optimization; evolutionary algorithm; Computer Science, Software Engineering; Scenario Description Language; Assurance for autonomous vehicles; traffic scene concretization},
	year = {2024},
	eissn = {1939-3520},
	pages = {48-68},
	orcid-numbers = {Varró, Dániel/0000-0002-8790-252X}
}

@article{MTMT:34292157,
	title = {Blockchain-Based, Confidentiality-Preserving Orchestration of Collaborative Workflows},
	url = {https://m2.mtmt.hu/api/publication/34292157},
	author = {Toldi, Balázs Ádám and Kocsis, Imre},
	doi = {10.36244/ICJ.2023.3.8},
	journal-iso = {INFOCOMM J},
	journal = {INFOCOMMUNICATIONS JOURNAL},
	volume = {15},
	unique-id = {34292157},
	issn = {2061-2079},
	abstract = {Business process collaboration between independent parties is challenging when participants do not completely trust each other. Tracking actions and enforcing the activity authorizations of participants via blockchain-hosted smart contracts is an emerging solution to this lack of trust, with most state-of-the-art approaches generating the orchestrating smart contract logic from Business Process Model and Notation (BPMN) models. However, compared to centralized business process orchestration services, smart contract state typically leaks potentially sensitive information about the state of the collaboration, limiting the applicability of decentralized process orchestration. This paper presents a novel, collaboration confidentiality-preserving approach where the process orchestrator smart contract only stores encrypted and hashed process states and validates participant actions against a BPMN model using zero-knowledge proofs. We cover a subset of BPMN, which is sufficient from the practical point of view, support messagepassing between participants, and provide an open-source, endto-end prototype implementation that automatically generates the key software artifacts.},
	year = {2023},
	eissn = {2061-2125},
	pages = {72-81}
}

@inproceedings{MTMT:34144059,
	title = {Configurable Model-Based Test Generation for Distributed Controllers Using Declarative Model Queries and Model Checkers},
	url = {https://m2.mtmt.hu/api/publication/34144059},
	author = {Graics, Bence and Molnár, Vince and Majzik, István},
	booktitle = {Formal Methods for Industrial Critical Systems},
	doi = {10.1007/978-3-031-43681-9_5},
	unique-id = {34144059},
	year = {2023},
	pages = {76-95},
	orcid-numbers = {Graics, Bence/0000-0001-5546-5970}
}

@inproceedings{MTMT:34112239,
	title = {CBDC Bridging between Hyperledger Fabric and Permissioned EVM-based Blockchains},
	url = {https://m2.mtmt.hu/api/publication/34112239},
	author = {Augusto, André and Belchior, Rafael and Kocsis, Imre and Gönczy, László and Vasconcelos, André and Correia, Miguel},
	booktitle = {2023 IEEE International Conference on Blockchain and Cryptocurrency (ICBC)},
	doi = {10.1109/ICBC56567.2023.10174953},
	unique-id = {34112239},
	year = {2023},
	pages = {1-9}
}