@conference {415,
	title = {Interpreting Logical Explanations of Classifying Neural Networks},
	booktitle = {ESANN 2026},
	year = {2026},
	abstract = {Formal methods are routinely used to address the issue of
explainability of machine learning models. Yet, it is not always trivial
to understand how a logical explanation could be useful in practice due
to human readability challenges. This paper applies classical geometric
methods for interpreting logical explanations and illustrates the usefulness
for the users on datasets from medical and image classification domains
previously studied in the context of formal explainability.},
	author = {Fabrizio Leopardi and Faezeh Labbaf and Tom{\'a}{\v s} Kol{\'a}rik and Michael Wand and Natasha Sharygina}
}
@conference {416,
	title = {Parallel SMT Solving via Iterative Tree Partitioning},
	booktitle = {TACAS 2026},
	year = {2026},
	abstract = {We present a novel algorithm for parallel solving of SMT
problems based on a partitioning process that divides the original problem into a tree structure in an iterative way. By enabling node revisiting, the new method addresses the problem of partitioning divergence found in prior approaches that frequently leads to longer runtimes compared to sequential results. The resulting algorithm is highly flexible, offers a combination of partitioning, portfolio solving, and clause sharing, allows the use of various partitioning functions, and scales gracefully with the available resources. We implemented the new approach in the tool SMTS on top of the efficient sequential SMT solver OpenSMT. Our experimental results demonstrate a substantial improvement over OpenSMT in logics QF LRA and QF LIA even when the partitioning approach utilizes just a single solver. Notably, SMTS has consistently dominated several divisions of the annual competition of parallel SMT solvers.},
	author = {Tom{\'a}{\v s} Kol{\'a}rik and Antti E. J. Hyv{\"a}rinen and Seyedmasoud Asadzadeh and Natasha Sharygina}
}
@conference {401,
	title = {Space Explanations of Neural Network Classification},
	booktitle = {37th CAV 2025},
	year = {2025},
	abstract = {We present a novel logic-based concept called Space Explanations for classifying neural networks that gives provable guarantees of the behavior of the network in continuous areas of the input feature space. To automatically generate space explanations, we leverage on a range of flexible Craig interpolation algorithms and unsatisfiable core generation.
Based on real-life case studies, ranging from small to medium to large size, we demonstrate that the generated explanations are more meaningful than those computed by the state-of-the-art},
	author = {Faezeh Labbaf and Tom{\'a}{\v s} Kol{\'a}rik and Martin Blicha and Grigory Fedyukovich and Michael Wand and Natasha Sharygina}
}
