15 citations · 18 across the 7 of their papers we have counts for
8 papers
Neuron Activation-based Computation of Logical Explanations for Deep Neural Networks
Tomáš Kolárik, Faezeh Labbaf, Fabrizio Leopardi +3
Formal explainability of classifying neural networks (NNs) is an active area of research, providing explanations with provable guarantees of the classification within continuous re…
Termination analysis with interpolation-based transition invariant generation
Konstantin Britikov, Martin Blicha, Grigory Fedyukovich +1
Termination and nontermination of infinite-state systems are complementary problems that, despite their close connection, are typically addressed by separate techniques. The core i…
Space Explanations of Neural Network Classification
Faezeh Labbaf, Tomáš Kolárik, Martin Blicha +3
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 o…
Competition Report: CHC-COMP-21
Grigory Fedyukovich, Philipp Rümmer
CHC-COMP-21 is the fourth competition of solvers for Constrained Horn Clauses. In this year, 7 solvers participated at the competition, and were evaluated in 7 separate tracks on p…
Solving Constrained Horn Clauses over ADTs by Finite Model Finding
Yurii Kostyukov, Dmitry Mordvinov, Grigory Fedyukovich
First-order logic is a natural way of expressing the properties of computation, traditionally used in various program logics for expressing the correctness properties and certifica…
Beyond the Elementary Representations of Program Invariants over Algebraic Data Types
Yurii Kostyukov, Dmitry Mordvinov, Grigory Fedyukovich
First-order logic is a natural way of expressing properties of computation. It is traditionally used in various program logics for expressing the correctness properties and certifi…