@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} } @article {164, title = {Loop summarization using state and transition invariants}, journal = {Formal Methods in System Design}, volume = {42}, year = {2013}, issn = {0925-9856}, author = {Kroening, D. and Natasha Sharygina and Tonetta, S. and Tsitovich, A. and Wintersteiger, C.M.} } @conference { twks11, title = {Loop Summarization and Termination Analysis}, booktitle = {International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS)}, volume = {6605}, year = {2011}, pages = {81-95}, publisher = {Springer}, organization = {Springer}, address = {Saarbr{\"u} Germany}, url = {http://dx.doi.org/10.1007/978-3-642-19835-9_9}, author = {Aliaksei Tsitovich and Natasha Sharygina and Christoph M. Wintersteiger and Kroening, Daniel} } @conference {154, title = {Termination Analysis with Compositional Transition Invariants}, booktitle = {International Conference on Computer-Aided Verification (CAV)}, year = {2010}, publisher = {Springer}, organization = {Springer}, address = {Edinburgh, UK}, abstract = {

Modern termination provers rely on a safety checker to construct disjunctively well-founded transition invariants. This safety check\ is known to be the bottleneck of the procedure. We present an alternative algorithm that uses a light-weight check based on transitivity of\ ranking relations to prove program termination. We provide an experimental evaluation over a set of 87 Windows drivers, and demonstrate\ that our algorithm is often able to conclude termination by examining\ only a small fraction of the program. As a consequence, our algorithm is\ able to outperform known approaches by multiple orders of magnitude.\ 

}, author = {Kroening, D. and Natasha Sharygina and Tsitovich, A. and Wintersteiger, C.M.} } @conference {153, title = {Loopfrog: A Static Analyzer for ANSI-C Programs}, booktitle = {The 24th IEEE/ACM International Conference on Automated Software Engineering}, year = {2009}, publisher = {IEEE Computer Society}, organization = {IEEE Computer Society}, address = {Auckland, New Zealand}, abstract = {

Practical software verification is dominated by two major classes of techniques. The first is model checking, which provides total precision, but suffers from the state space explosion problem. The second is abstract interpretation, which is usually much less demanding, but often returns a high number of false positives.

We present Loopfrog, a static analyzer that combines the best of both worlds: the precision of model checking and the performance of abstract interpretation. In contrast to traditional static analyzers, it also provides "leaping" counterexamples to aid in the diagnosis of errors.

}, author = {Kroening, D. and Natasha Sharygina and Tonetta, S. and Tsitovich, A. and Wintersteiger, C.M.} } @conference {152, title = {Loop Summarization using Abstract Transformers}, booktitle = {6th International Symposium on Automated Technology for Verification and Analysis (ATVA)}, year = {2008}, publisher = {Springer, Volume 5311}, organization = {Springer, Volume 5311}, address = {Seoul, South Korea}, abstract = {

Existing program analysis tools that implement abstraction rely on saturating procedures to compute over-approximations of fixpoints. As an alternative, we propose a new algorithm to compute an over-approximation of the set of reachable states of a program by replacing loops in the control flow graph by their abstract transformer. Our technique is able to generate diagnostic information in case of property violations, which we call leaping counterexamples. We have implemented this technique and report experimental results on a set of large ANSI-C programs using abstract domains that focus on properties related to string-buffers.

}, author = {Kroening, D. and Natasha Sharygina and Tonetta, S. and Tsitovich, A. and Wintersteiger, C.M.} }