@article{MTMT:34822027,
	title = {Minimal Armstrong Databases for Cardinality Constraints},
	url = {https://m2.mtmt.hu/api/publication/34822027},
	author = {Király, Bence and Sali, Attila},
	doi = {10.1007/978-3-031-56940-1_4},
	journal-iso = {LNCS},
	journal = {LECTURE NOTES IN COMPUTER SCIENCE},
	volume = {14589},
	unique-id = {34822027},
	issn = {0302-9743},
	abstract = {Hartmann et al. proved that calculating Armstrong instance for a collection of cardinality constraints is exactly exponential problem. In fact, they presented a collection of cardinality constraints based on some special graphs, whose minimal Armstrong instance is of exponential size. Motivated by that, graph based cardinality constraints are introduced in the present paper. That is, given a simple graph on the set of attributes, max cardinality constraints on edges end vertices, respectively are set. We take up the task to determine sizes of minimum Armstrong instances of graph based cardinality constraints for several graph classes, including bipartite graphs, complete multipartite graphs. We give exact results for several graph classes or give polynomial time algorithm to construct the minimum Armstrong table for other cases. We show that Armstrong tables of graph based cardinality constraints correspond to another graph defined on the maximal independent vertex sets of the constraint graph. The row graph of an Armstrong table is defined as a pair of rows form an edge if they contain identical entries in some column. It is shown that there exists a minimal Armstrong table for a collection of graph based cardinality constraints such that the line graph of its row graph is a spanning subgraph of the graph defined on the maximal independent sets of the constraint graph. This observation is used to find minimum Armstrong tables for bipartite constraint graphs. Feasible edge colourings of graphs introduced by Folkman and Fulkerson are used to construct minimum Armstrong tables for another class of constraint graphs. © The Author(s), under exclusive license to Springer Nature Switzerland AG 2024.},
	keywords = {Polynomial approximation; Graph theory; Graphic methods; Graph-based; Armstrong instance; Armstrong instance; Cardinality constraints; EXPONENTIALS; Complete k-partite graphs; Complete k-partite graphs; Edge-colouring; Line graphs; Armstrong tables; constraint graph; Cardinality Constraint; Linegraph; feasible edge colorings; Feasible edge coloring},
	year = {2024},
	eissn = {1611-3349},
	pages = {64-81}
}

@article{MTMT:34805111,
	title = {1-Attempt and Equivalent Thinning on the Hexagonal Grid},
	url = {https://m2.mtmt.hu/api/publication/34805111},
	author = {Palágyi, Kálmán},
	doi = {10.1007/978-3-031-57793-2_30},
	journal-iso = {LNCS},
	journal = {LECTURE NOTES IN COMPUTER SCIENCE},
	volume = {2024},
	unique-id = {34805111},
	issn = {0302-9743},
	year = {2024},
	eissn = {1611-3349},
	pages = {390-401},
	orcid-numbers = {Palágyi, Kálmán/0000-0002-3274-7315}
}

@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:34823002,
	title = {Explaining Full-Disk Deep Learning Model for Solar Flare Prediction Using Attribution Methods},
	url = {https://m2.mtmt.hu/api/publication/34823002},
	author = {Pandey, C. and Angryk, R.A. and Aydin, B.},
	doi = {10.1007/978-3-031-43430-3_5},
	journal-iso = {LNCS},
	journal = {LECTURE NOTES IN COMPUTER SCIENCE},
	volume = {14175},
	unique-id = {34823002},
	issn = {0302-9743},
	year = {2023},
	eissn = {1611-3349},
	pages = {72-89}
}

@article{MTMT:34772650,
	title = {SCIVO. Skills to Career with Interests and Values Ontology},
	url = {https://m2.mtmt.hu/api/publication/34772650},
	author = {Keshan, Neha and Hendler, James A.},
	doi = {10.1007/978-3-031-47745-4_19},
	journal-iso = {LNCS},
	journal = {LECTURE NOTES IN COMPUTER SCIENCE},
	volume = {14382},
	unique-id = {34772650},
	issn = {0302-9743},
	year = {2023},
	eissn = {1611-3349},
	pages = {262-276}
}

@article{MTMT:34756865,
	title = {Analogs of Image Analysis Tools in the Search of Latent Regularities in Applied Data},
	url = {https://m2.mtmt.hu/api/publication/34756865},
	author = {Nelyubina, Elena and Ryazanov, Vladimir and Vinogradov, Alexander},
	doi = {10.1007/978-3-031-37742-6_41},
	journal-iso = {LNCS},
	journal = {LECTURE NOTES IN COMPUTER SCIENCE},
	volume = {13644},
	unique-id = {34756865},
	issn = {0302-9743},
	year = {2023},
	eissn = {1611-3349},
	pages = {529-540}
}

@article{MTMT:34754557,
	title = {Resolving Hungarian Anaphora with ChatGPT},
	url = {https://m2.mtmt.hu/api/publication/34754557},
	author = {Vadász, Noémi},
	doi = {10.1007/978-3-031-40498-6_5},
	journal-iso = {LNCS},
	journal = {LECTURE NOTES IN COMPUTER SCIENCE},
	volume = {14102},
	unique-id = {34754557},
	issn = {0302-9743},
	year = {2023},
	eissn = {1611-3349},
	pages = {45-57}
}

@article{MTMT:34719645,
	title = {Quantum Annealing vs. QAOA: 127 Qubit Higher-Order Ising Problems on NISQ Computers},
	url = {https://m2.mtmt.hu/api/publication/34719645},
	isbn = {978-3-031-32041-5},
	author = {Pelofske, Elijah and Bärtschi, Andreas and Eidenbenz, Stephan},
	journal-iso = {LNCS},
	journal = {LECTURE NOTES IN COMPUTER SCIENCE},
	volume = {13948},
	unique-id = {34719645},
	issn = {0302-9743},
	abstract = {Quantum annealing (QA) and Quantum Alternating Operator Ansatz (QAOA) are both heuristic quantum algorithms intended for sampling optimal solutions of combinatorial optimization problems. In this article we implement a rigorous direct comparison between QA on D-Wave hardware and QAOA on IBMQ hardware. These two quantum algorithms are also compared against classical simulated annealing. The studied problems are instances of a class of Ising models, with variable assignments of $$+1$$+1or $$-1$$-1, that contain cubic ZZZ interactions (higher order terms) and match both the native connectivity of the Pegasus topology D-Wave chips and the heavy hexagonal lattice of the IBMQ chips. The novel QAOA implementation on the heavy hexagonal lattice has a CNOT depth of 6 per round and allows for usage of an entire heavy hexagonal lattice. Experimentally, QAOA is executed on an ensemble of randomly generated Ising instances with a grid search over 1 and 2 round angles using all 127 programmable superconducting transmon qubits of ibm_washington. The error suppression technique digital dynamical decoupling is also tested on all QAOA circuits. QA is executed on the same Ising instances with the programmable superconducting flux qubit devices D-Wave Advantage_system4.1 and Advantage_system6.1 using modified annealing schedules with pauses. We find that QA outperforms QAOA on all problem instances. We also find that dynamical decoupling enables 2-round QAOA to marginally outperform 1-round QAOA, which is not the case without dynamical decoupling.},
	year = {2023},
	eissn = {1611-3349},
	pages = {240-258}
}