15 citations · 28 across the 11 of their papers we have counts for
13 papers
Verification of Compiler-to-Accelerator Mappings for Machine Learning Accelerators
Akash Gaonkar, Mike He, Yi Li +8
To meet the performance needs of modern machine learning (ML) applications, ML compiler frameworks support compiler-to-accelerator mappings that offload parts of application code t…
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…
Synthesis of Infinite-State Systems with Random Behavior
Andreas Katis, Grigory Fedyukovich, Jeffrey Chen +3
Diversity in the exhibited behavior of a given system is a desirable characteristic in a variety of application contexts. Synthesis of conformant implementations often proceeds by…
Proceedings of the Sixth Workshop on Horn Clauses for Verification and Synthesis and Third Workshop on Program Equivalence and Relational Reasoning
Emanuele De Angelis, Grigory Fedyukovich, Nikos Tzevelekos +1
This volume contains the joint post-proceedings of the 3rd Workshop on Program Equivalence and Relational Reasoning (PERR) and the 6th Workshop on Horn Clauses for Verification and…
Validity-Guided Synthesis of Reactive Systems from Assume-Guarantee Contracts
Andreas Katis, Grigory Fedyukovich, Huajun Guo +4
Automated synthesis of reactive systems from specifications has been a topic of research for decades. Recently, a variety of approaches have been proposed to extend synthesis of re…
Verifying Safety of Functional Programs with Rosette/Unbound
Dmitry Mordvinov, Grigory Fedyukovich
The goal of unbounded program verification is to discover an inductive invariant that safely over-approximates all possible program behaviors. Functional languages featuring higher…
Approaching Symbolic Parallelization by Synthesis of Recurrence Decompositions
Grigory Fedyukovich, Rastislav Bodík
We present GraSSP, a novel approach to perform automated parallelization relying on recent advances in formal verification and synthesis. GraSSP augments an existing sequential pro…
Synthesis from Assume-Guarantee Contracts using Skolemized Proofs of Realizability
Andreas Katis, Grigory Fedyukovich, Andrew Gacek +3
The realizability problem in requirements engineering is to determine the existence of an implementation that meets the given formal requirements. A step forward after realizabilit…