Termination and nontermination of infinite-state systems are complementary problems that, despite their close connection, are typically addressed by separate techniques. The core idea of this paper is to connect termination and nontermination analysis, enabling the two to share intermediate results and guide one another. We present a new termination analysis approach based on the generation of well-founded transition invariants. It leverages Craig interpolation for transition invariant generation, capturing the structural reasons for termination. The proposed technique extends safety-based nontermination analysis, enabling it to prove both termination and nontermination within a unified framework. We implemented our approach in the GOLEM verification framework and evaluated it on benchmarks from the Termination Competition (TermComp). Empirical results demonstrate that combining termination and nontermination is beneficial and yields performance comparable to state-of-the-art tools.
Konstantin Britikov, Martin Blicha, Grigory Fedyukovich et al.· 0 citations
Formal explainability of classifying neural networks (NNs) is an active area of research, providing explanations with provable guarantees of the classification within continuous regions of the input feature space. However, the existing techniques are either limited to individual input features without guarantees on their relations or the provided solutions fail to scale to deep architectures. This paper addresses these issues by introducing a flexible symbolic framework for an efficient, guided computation of explanations of the NN behavior, parametrized by the activations of internal neurons, and using logical engines such as SMT solvers. Unlike prior methods that rely on specialized NN verifiers, our method yields explanations that are not restricted in shape. Our algorithm is implementable on top of a general-purpose logical solver, isolating the NN-specific encoding from the algorithmic framework. We experimented with a wide range of benchmarks from the domains of image recognition and medicine, illustrating the advantages of the new method, particularly in computational efficiency. Notably, our approach enables logical explanation of deep networks not amenable to prior logic-based methods.
Tomáš Kolárik, Faezeh Labbaf, Fabrizio Leopardi et al.· 0 citations
This work introduces space explanations, a logic-based notion of explanation that represents sufficient conditions for a neural network to predict a given class over a (potentially large and geometrically complex) subset of the feature space and demonstrates that the interpolation-based explanations are more meaningful than those computed by state-of-the-art techniques.
Faezeh Labbaf, Tomáš Kolárik, Martin Blicha et al.· CI-BD-SOQE@FLoC· 0 citations
We use cookies to run the site and, with your consent, for analytics and to show ads.
See our Cookie Policy.
