1 citations · 1 across the 6 of their papers we have counts for
6 papers
Large Lemma Miners: Can LLMs do Induction Proofs for Hardware?
Romy Peled, Daniel Kroening, Michael Tautschnig +1
Large Language Models (LLMs) have shown potential for solving mathematical tasks. We show that LLMs can be utilized to generate proofs by induction for hardware verification and th…
Causal Explanations for Image Classifiers
Hana Chockler, David A. Kelly, Daniel Kroening +1
Existing algorithms for explaining the output of image classifiers use different definitions of explanations and a variety of techniques to find them. However, none of the existing…
Neural Model Checking
Mirco Giacobbe, Daniel Kroening, Abhinandan Pal +1
We introduce a machine learning approach to model checking temporal logic, with application to formal hardware verification. Model checking answers the question of whether every ex…
You Only Explain Once
David A. Kelly, Hana Chockler, Daniel Kroening +4
In this paper, we propose a new black-box explainability algorithm and tool, YO-ReX, for efficient explanation of the outputs of object detectors. The new algorithm computes explan…
Active Learning of Abstract System Models from Traces using Model Checking [Extended]
Natasha Yogananda Jeppu, Tom Melham, Daniel Kroening
We present a new active model-learning approach to generating abstractions of a system implementation, as finite state automata (FSAs), from execution traces. Given an implementati…
Danger Invariants
Cristina David, Daniel Kroening, Matt Lewis
Static analysers search for overapproximating proofs of safety commonly known as safety invariants. Fundamentally, such analysers summarise traces into sets of states, thus trading…