@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 {326,
	title = {Farkas-Based Tree Interpolation},
	booktitle = {SAS 2020 - 27th Static Analysis Symposium},
	year = {2020},
	publisher = {Springer},
	organization = {Springer},
	address = {Online Conference},
	url = {https://link.springer.com/chapter/10.1007\%2F978-3-030-65474-0_16},
	author = {Sepideh Asadi and Martin Blicha and Antti Hyv{\"a}rinen and Grigory Fedyukovich and Natasha Sharygina}
}
@conference {288,
	title = {Function Summarization Modulo Theories},
	booktitle = {22nd International Conference on Logic for Programming Artificial Intelligence and Reasoning, LPAR},
	year = {2018},
	publisher = {EasyChair Publications},
	organization = {EasyChair Publications},
	address = {Ethiopia},
	keywords = {Author keywords:	 Software Verification Bounded Model Checking, Craig Interpolation, Function Summaries, Incremental Verification, Satisfiability Modulo Theories, Software Verification},
	doi = {10.29007/d3bt},
	url = {https://easychair.org/publications/paper/nNLJ},
	author = {Sepideh Asadi and Martin Blicha and Grigory Fedyukovich and Antti E. J. Hyv{\"a}rinen and Karine Even-Mendoza and Natasha Sharygina and Hana Chockler}
}
@conference {248,
	title = {Flexible Interpolation for Efficient Model Checking},
	booktitle = {MEMICS 2016},
	year = {2016},
	url = {http://verify.inf.usi.ch/sites/default/files/MEMICS2016.pdf},
	author = {Antti E. J. Hyv{\"a}rinen and Leonardo Alt and Natasha Sharygina}
}
@conference { Ondrej Sery; Gri,
	title = {FunFrog: Bounded Model Checking with Interpolation-based Function Summarization},
	booktitle = {Tenth International Symposium on Automated Technology for Verification and Analysis (ATVA)},
	year = {2012},
	note = {To appear at the conference. The pdf-version is not final.},
	address = {Thiruvananthapuram, India},
	author = {Sery, O. and Grigory Fedyukovich and Natasha Sharygina}
}
@conference {149,
	title = {Function Summaries in Software Upgrade Checking},
	booktitle = {Haifa Verification Conference (HVC)},
	year = {2011},
	publisher = {Springer},
	organization = {Springer},
	address = {Haifa Verification Conference (HVC)},
	author = {Grigory Fedyukovich and Sery, O. and Natasha Sharygina}
}
@conference {145,
	title = {Flexible Interpolation with Local Proof Transformations},
	booktitle = {International Conference of Computer Aided Design (ICCAD)},
	year = {2010},
	publisher = {IEEE Computer Society},
	organization = {IEEE Computer Society},
	address = {San Jose, USA},
	abstract = {<p><span style="color: rgb(73, 73, 73); font-family: {\textquoteright}Lucida Grande{\textquoteright}, {\textquoteright}Bitstream Vera Sans{\textquoteright}, Arial, sans-serif; ">Model checking based on Craig{\textquoteright}s interpolants ultimately relies on efficient engines, such as SMT-solvers, to log proofs of unsatisfiability and to derive the desired interpolant by means of a set of algorithms known in literature. These algorithms, however, are designed for proofs that do not contain mixed predicates. In this paper we present a technique for transforming the propositional proof produced by an SMT-solver in such a way that mixed predicates are eliminated. We show a number of cases in which mixed predicates arise as a consequence of state-of-the-art solving procedures (e.g. lemma on demand, theory combination, etc.). In such cases our technique can be applied to allow the application of known interpolation algorithms. We demonstrate with a set of experiments that our approach is viable.</span></p>
},
	author = {Bruttomesso, R. and Rollini, S.F. and Natasha Sharygina and Tsitovich, A.}
}
@conference { BPS10,
	title = {A Flexible Schema for Generating Explanations in Lazy Theory Propagation},
	booktitle = {International Conference on Formal Methods and Models for Codesign (MEMOCODE)},
	year = {2010},
	note = {to appear},
	publisher = {IEEE Computer Society},
	organization = {IEEE Computer Society},
	address = {Grenoble, France},
	author = {Bruttomesso, R. and Pek, E. and Natasha Sharygina}
}
