26 citations · 64 across the 11 of their papers we have counts for
12 papers
Exposing Previously Undetectable Faults in Deep Neural Networks
Isaac Dunn, Hadrien Pouget, Daniel Kroening +1
Existing methods for testing DNNs solve the oracle problem by constraining the raw features (e.g. image pixel values) to be within a small distance of a dataset example for which t…
Hardware/Software Co-verification Using Path-based Symbolic Execution
Rajdeep Mukherjee, Saurabh Joshi, John O'Leary +2
Conventional tools for formal hardware/software co-verification use bounded model checking techniques to construct a single monolithic propositional formula. Formulas generated in…
Evaluating Robustness to Context-Sensitive Feature Perturbations of Different Granularities
Isaac Dunn, Laura Hanu, Hadrien Pouget +2
We cannot guarantee that training datasets are representative of the distribution of inputs that will be encountered during deployment. So we must have confidence that our models d…
Learning Concise Models from Long Execution Traces
Natasha Yogananda Jeppu, Tom Melham, Daniel Kroening +1
Abstract models of system-level behaviour have applications in design exploration, analysis, testing and verification. We describe a new algorithm for automatically extracting usef…
DeepSynth: Automata Synthesis for Automatic Task Segmentation in Deep Reinforcement Learning
Mohammadhosein Hasanbeig, Natasha Yogananda Jeppu, Alessandro Abate +2
This paper proposes DeepSynth, a method for effective training of deep Reinforcement Learning (RL) agents when the reward is sparse and non-Markovian, but at the same time progress…
CREST: Hardware Formal Verification with ANSI-C Reference Specifications
Andreas Tiemeyer, Tom Melham, Daniel Kroening +1
This paper presents CREST, a prototype front-end tool intended as an add-on to commercial EDA formal verifcation environments. CREST is an adaptation of the CBMC bounded model chec…
Adaptive Generation of Unrestricted Adversarial Inputs
Isaac Dunn, Hadrien Pouget, Tom Melham +1
Neural networks are vulnerable to adversarially-constructed perturbations of their inputs. Most research so far has considered perturbations of a fixed magnitude under some n…
Automatic Heap Layout Manipulation for Exploitation
Sean Heelan, Tom Melham, Daniel Kroening
Heap layout manipulation is integral to exploiting heap-based memory corruption vulnerabilities. In this paper we present the first automatic approach to the problem, based on pseu…
Lifting CDCL to Template-based Abstract Domains for Program Verification
Rajdeep Mukherjee, Peter Schrammel, Leopold Haller +2
The success of Conflict Driven Clause Learning (CDCL) for Boolean satisfiability has inspired adoption in other domains. We present a novel lifting of CDCL to program analysis call…
Equivalence Checking a Floating-point Unit against a High-level C Model (Extended Version)
Rajdeep Mukherjee, Saurabh Joshi, Andreas Griesmayer +2
Semiconductor companies have increasingly adopted a methodology that starts with a system-level design specification in C/C++/SystemC. This model is extensively simulated to ensure…
On the Semantics of ReFLect as a Basis for a Reflective Theorem Prover
Tom Melham, Raphael Cohn, Ian Childs
This paper explores the semantics of a combinatory fragment of reFLect, the lambda-calculus underlying a functional language used by Intel Corporation for hardware design and verif…
Chaining Test Cases for Reactive System Testing (extended version)
Peter Schrammel, Tom Melham, Daniel Kroening
Testing of synchronous reactive systems is challenging because long input sequences are often needed to drive them into a state at which a desired feature can be tested. This is pa…