@inproceedings{MTMT:37488250,
	title = {CHC-Based Reachability Analysis via Cycle Summarization},
	url = {https://m2.mtmt.hu/api/publication/37488250},
	author = {Britikov, Konstantin and Fedyukovich, Grigory and Sharygina, Natasha},
	booktitle = {INTEGRATED FORMAL METHODS, IFM 2025},
	doi = {10.1007/978-3-032-10794-7_11},
	unique-id = {37488250},
	year = {2026},
	pages = {205-225}
}

@inproceedings{MTMT:36615315,
	title = {Competition of Solvers for Constrained Horn Clauses (CHC-COMP 2023)},
	url = {https://m2.mtmt.hu/api/publication/36615315},
	author = {De Angelis, Emanuele and Krishnan, Hari Govind Vediramana},
	booktitle = {TOOLYMPICS CHALLENGE 2023},
	doi = {10.1007/978-3-031-67695-6_2},
	unique-id = {36615315},
	keywords = {Constraint solving; Satisfiability Modulo Theories; Constraint Logic Programming; Constrained Horn clauses},
	year = {2025},
	pages = {38-51},
	orcid-numbers = {De Angelis, Emanuele/0000-0002-7319-8439}
}

@inproceedings{MTMT:37488251,
	title = {Integrating Loop Acceleration Into Bounded Model Checking},
	url = {https://m2.mtmt.hu/api/publication/37488251},
	author = {Frohn, Florian and Giesl, Jürgen},
	booktitle = {FORMAL METHODS, PT I, FM 2024},
	doi = {10.1007/978-3-031-71162-6_4},
	unique-id = {37488251},
	abstract = {Bounded Model Checking (BMC) is a powerful technique for proving unsafety. However, finding deep counterexamples that require a large bound is challenging for BMC. On the other hand, acceleration techniques compute “shortcuts” that “compress” many execution steps into a single one. In this paper, we tightly integrate acceleration techniques into SMT-based bounded model checking. By adding suitable “shortcuts” on the fly, our approach can quickly detect deep counterexamples. Moreover, using so-called blocking clauses , our approach can prove safety of examples where BMC diverges. An empirical comparison with other state-of-the-art techniques shows that our approach is highly competitive for proving unsafety, and orthogonal to existing techniques for proving safety.},
	year = {2025},
	pages = {73-91},
	orcid-numbers = {Frohn, Florian/0000-0003-0902-1994; Giesl, Jürgen/0000-0003-0283-8520}
}

@inproceedings{MTMT:35863943,
	title = {Mode-based Reduction from Validity Checking of Fixpoint Logic Formulas to Test-Friendly Reachability Problem},
	url = {https://m2.mtmt.hu/api/publication/35863943},
	author = {Katsura, H. and Kobayashi, N. and Sakayori, K. and Sato, R.},
	booktitle = {Programming Languages and Systems},
	doi = {10.1007/978-981-97-8943-6_16},
	volume = {15194 LNCS},
	unique-id = {35863943},
	abstract = {A logical approach to automated program verification has been drawing attention recently, where various program verification problems are transformed into formulas of fixpoint logics such as CHC and νHFL(Z), so that a given program satisfies a property just if the corresponding fixpoint formula is valid. In this paper, we show a kind of converse transformation, converting fixpoint logic formulas to programs so that a formula is valid just if the resulting program never evaluates to an (error) value. This, together with the aforementioned transformation from programs to formulas, allows us to go back and forth between logical formulas and programs. In particular, our transformation enables us to use random testing to disprove a given formula, implying that the original program does not satisfy the specified property. As the programs generated by a naive transformation are not suitable for random testing, we employ mode analysis to generate more test-friendly programs. We have implemented the mode-guided transformation and confirmed its effectiveness through experiments. © The Author(s), under exclusive license to Springer Nature Singapore Pte Ltd. 2025.},
	keywords = {HYDROGEN-TRANSFER REDUCTIONS; PROPERTY; Logic programming; Software testing; Program Verification; Computer circuits; Reachability problem; random testing; FORTH (programming language); Fixpoints; Logical approaches; Logic formulas; Automated program verification; Mode-based},
	year = {2025},
	pages = {325-345}
}

@article{MTMT:37488252,
	title = {Validation of CHC Satisfiability with ATHENA},
	url = {https://m2.mtmt.hu/api/publication/37488252},
	author = {Otoni, Rodrigo and Blicha, Martin and Eugster, Patrick and Sharygina, Natasha},
	doi = {10.1145/3716505},
	journal-iso = {FORM ASP COMPUT},
	journal = {FORMAL ASPECTS OF COMPUTING},
	volume = {37},
	unique-id = {37488252},
	issn = {0934-5043},
	abstract = {Formal verification tooling increasingly relies on logic solvers as automated reasoning engines. A commonality among these solvers is the high complexity of their codebases, which makes bug occurrence disturbingly frequent. Tool competitions have showcased many examples of state-of-the-art solvers disagreeing on the satisfiability of logic formulas, be it solvers for Boolean satisfiability (SAT), satisfiability modulo theories (SMT), or constrained Horn clauses (CHC). The validation of solvers’ results is thus of paramount importance, in order to increase the confidence not only in the solvers themselves but also in the tooling which they underpin. Among the formalisms commonly used by modern verification tools, CHC is one that has seen, at the same time, extensive practical usage and very little effort in result validation. We propose a two-layered validation approach for witnesses of CHC satisfiability that validates CHC models via proof-backed SMT queries. We developed a modular evaluation framework, ATHENA, and assessed the approach’s viability via large scale experimentation, comparing three CHC solvers, five SMT solvers, and five proof checkers. Our results indicate that the approach is feasible, with the potential to be incorporated into CHC-based tooling, and also confirm the need for validation, with fourteen bugs being found in the tools used.},
	year = {2025},
	eissn = {1433-299X},
	pages = {1-20},
	orcid-numbers = {Otoni, Rodrigo/0000-0003-1097-2367; Blicha, Martin/0000-0001-8140-4098; Eugster, Patrick/0000-0003-3864-9078; Sharygina, Natasha/0000-0002-8872-4913}
}

@article{MTMT:37488253,
	title = {Логики условных вычислений с ошибками},
	url = {https://m2.mtmt.hu/api/publication/37488253},
	author = {Непейвода, Николай Николаевич},
	doi = {10.21146/2074-1472-2025-31-1-24-46},
	journal = {Logical Investigations},
	volume = {31},
	unique-id = {37488253},
	issn = {2413-2713},
	abstract = {В компьютерных программах недопустимо игнорировать практически неизбежное наличие ошибок. Как гласит аксиома Шуры-Буры: «Если программа на самом деле абсолютно правильна, она никому не нужна». А в задачах точных вычислений и в суперкомпьютерах возникает необходимость управления вычислениями от исключительных ситуаций. Для описания такого исполнения недостаточно адекватна двузначная и трехзначная логика. Некоторые ошибки, такие как переполнения или деление на ноль, могут быть обработаны и идентифицируются логическим значением u. Но такие, как «синий экран смерти», фатальны: исправлены внутри программы быть не могут. Множество значений пополняется мягкой ошибкой и фатальной ошибкой \(\bot\). Здесь рассматривается следующая семантика: это сигнал, что однозначное решение не найдено и интерпретируется как \(\{\mathfrak{t},\mathfrak{f}\}\) , а \(\bot\) — как логический провал \(\varnothing\). Рассматриваются лишь непрерывные в топологии \(\bot\) вычисления. Базисом логики принимается условный оператор if then else fi и логические константы \(\{\mathfrak{t},\mathfrak{f}, u, \bot\}\). Исследуются логики, соответствующие различным вариантам организации вычислений данного оператора. Полностью описаны взаимные выразимости этих вариантов. Показано, что различные вариации вычислений порождают, в частности, логики Клини, Лукасевича, Гёделя.},
	year = {2025},
	eissn = {2074-1472},
	pages = {24-46}
}