@conference {421,
	title = {Formally Explaining Neural Network Classification},
	booktitle = {FM 2026},
	year = {2026},
	abstract = {Neural networks (NNs) are the core of AI-based technologies. However, the degree of reliability in performing the task is an open problem. The explainability of a central task of NNs, classification, is of immense importance. While at the rise of AI-based reasoning, explainability of the NN classification has mostly been done using statistical methods, nowadays, a more reliable trend of formal logic-based methods is gaining popularity. The advantage of the formal approach is that it gives strict and provable guarantees of the classification. Formal methods is a mature field that has delivered a number of efficient computational solutions already applied in the analysis of software and hardware systems. Formal explainability methods naturally have the ability to reuse existing techniques and tools for a newly emerging field of formal explainability of NN classification.
This half-day tutorial will survey existing efforts to compute explanations of neural network classification based on logical abductive reasoning. The abduction approach is crucial for generalizing the results, capturing the underlying behavior of the classifier. We will present the existing techniques as instances of a general formalization that allows contrasting them against each other. In addition, we will discuss the issue of the quality of explanations, focusing on their key metrics and factors.
After overviewing and contrasting the existing concepts, the tutorial will proceed with presenting a practical framework, SpEXplAIn, which automatically computes Space Explanations, the most general abductionbased explanations for classifying NNs with provable guarantees of the behavior of the network in continuous areas of the input feature space. The tool leverages an SMT solver compatible with a range of flexible Craig interpolation algorithms and unsatisfiable core generation. Based on real-life case studies from different domains, we will illustrate the usefulness and flexibility of the new proof-based explanation framework.},
	url = {https://verify.inf.usi.ch/sites/default/files/papers/paper_373.pdf},
	author = {Natasha Sharygina and Faezeh Labbaf and Fabrizio Leopardi and Tom{\'a}{\v s} Kol{\'a}rik and Grigory Fedyukovich and Michael Wand}
}
@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.},
	url = {https://verify.inf.usi.ch/sites/default/files/papers/ESANN.pdf},
	author = {Fabrizio Leopardi and Faezeh Labbaf and Tom{\'a}{\v s} Kol{\'a}rik and Michael Wand 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}
}
@conference {194,
	title = {VERIGE: Verification with Invariant Generation Engine},
	booktitle = {SPIN},
	year = {2014},
	publisher = {ACM},
	organization = {ACM},
	author = {Latorre, N. and Francesco Alberti and Natasha Sharygina}
}
@conference {165,
	title = {PINCETTE - Validating Changes and Upgrades in Networked Software},
	booktitle = {17th European Conference on Software Maintenance and Reengineering},
	year = {2013},
	author = {Chockler, H. and Denaro, G. and Ling, M. and Grigory Fedyukovich and Antti E. J. Hyv{\"a}rinen and Mariani, L. and Muhammad, A. and Oriol, M. and Rajan, A. and Sery, O. and Natasha Sharygina and Tautschnig, M.}
}
