@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 = {LECT NOTES COMPUT SC}, 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 = {LECT NOTES COMPUT SC}, 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: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 = {LECT NOTES COMPUT SC}, 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 = {LECT NOTES COMPUT SC}, 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 = {LECT NOTES COMPUT SC}, 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 = {LECT NOTES COMPUT SC}, 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} } @article{MTMT:34511444, title = {Aggregation Strategies of Wav2vec 2.0 Embeddings for Computational Paralinguistic Tasks}, url = {https://m2.mtmt.hu/api/publication/34511444}, author = {Kiss-Vetráb, Mercedes and Gosztolya, Gábor}, doi = {10.1007/978-3-031-48309-7_7}, journal-iso = {LECT NOTES COMPUT SC}, journal = {LECTURE NOTES IN COMPUTER SCIENCE}, volume = {14338}, unique-id = {34511444}, issn = {0302-9743}, year = {2023}, eissn = {1611-3349}, pages = {79-93}, orcid-numbers = {Kiss-Vetráb, Mercedes/0000-0002-3914-2036; Gosztolya, Gábor/0000-0002-2864-6466} } @article{MTMT:34445422, title = {Hidden Stabilizers, the Isogeny to Endomorphism Ring Problem and the Cryptanalysis of pSIDH}, url = {https://m2.mtmt.hu/api/publication/34445422}, author = {Chen, M and Imran, Muhammad and Ivanyos, Gábor and Kutas, Péter and Leroux, A and Petit, C}, doi = {10.1007/978-981-99-8727-6_4}, journal-iso = {LECT NOTES COMPUT SC}, journal = {LECTURE NOTES IN COMPUTER SCIENCE}, volume = {14440}, unique-id = {34445422}, issn = {0302-9743}, abstract = {The Isogeny to Endomorphism Ring Problem (IsERP) asks to compute the endomorphism ring of the codomain of an isogeny between supersingular curves in characteristic p given only a representation for this isogeny, i.e. some data and an algorithm to evaluate this isogeny on any torsion point. This problem plays a central role in isogeny-based cryptography; it underlies the security of pSIDH protocol (ASIACRYPT 2022) and it is at the heart of the recent attacks that broke the SIDH key exchange. Prior to this work, no efficient algorithm was known to solve IsERP for a generic isogeny degree, the hardest case seemingly when the degree is prime. In this paper, we introduce a new quantum polynomial-time algorithm to solve IsERP for isogenies whose degrees are odd and have O(log log p) many prime factors. As main technical tools, our algorithm uses a quantum algorithm for computing hidden Borel subgroups, a group action on supersingular isogenies from EUROCRYPT 2021, various algorithms for the Deuring correspondence and a new algorithm to lift arbitrary quaternion order elements modulo an odd integer N with O(log log p) many prime factors to powersmooth elements. As a main consequence for cryptography, we obtain a quantum polynomial-time key recovery attack on pSIDH. The technical tools we use may also be of independent interest.}, keywords = {Algorithms; QUANTUM; Computer Science, Information Systems; Computer Science, Theory & Methods}, year = {2023}, eissn = {1611-3349}, pages = {99-130}, orcid-numbers = {Chen, M/0009-0003-8274-0685; Ivanyos, Gábor/0000-0003-3826-1735; Kutas, Péter/0000-0002-2043-9542; Petit, C/0000-0003-3482-6743} } @article{MTMT:34417195, title = {Exploring the Challenges and Limitations of Unsupervised Machine Learning Approaches in Legal Concepts Discovery}, url = {https://m2.mtmt.hu/api/publication/34417195}, author = {Prince-Tritto, Philippe and Ponce, Hiram}, doi = {10.1007/978-3-031-47640-2_5}, journal-iso = {LECT NOTES COMPUT SC}, journal = {LECTURE NOTES IN COMPUTER SCIENCE}, volume = {14392}, unique-id = {34417195}, issn = {0302-9743}, year = {2023}, eissn = {1611-3349}, pages = {52-67} } @article{MTMT:34316890, title = {Data AUDIT: Identifying Attribute Utility- and Detectability-Induced Bias in Task Models}, url = {https://m2.mtmt.hu/api/publication/34316890}, author = {Pavlak, M. and Drenkow, N. and Petrick, N. and Farhangi, M.M. and Unberath, M.}, doi = {10.1007/978-3-031-43898-1_43}, journal-iso = {LECT NOTES COMPUT SC}, journal = {LECTURE NOTES IN COMPUTER SCIENCE}, volume = {14222}, unique-id = {34316890}, issn = {0302-9743}, year = {2023}, eissn = {1611-3349}, pages = {442-452} }