research
∙
02/05/2023
CBMC: The C Bounded Model Checker
The C Bounded Model Checker (CBMC) demonstrates the violation of asserti...
share
research
∙
02/05/2023
JBMC: A Bounded Model Checking Tool for Java Bytecode
JBMC is an open-source SAT- and SMT-based bounded model checking tool fo...
research
∙
02/05/2023
2LS for Program Analysis
2LS ("tools") is a verification tool for C programs, built upon the CPRO...
research
∙
09/21/2022
LCRL: Certified Policy Synthesis via Logically-Constrained Reinforcement Learning
LCRL is a software tool that implements model-free Reinforcement Learnin...
research
∙
12/11/2021
Active Learning of Abstract System Models from Traces using Model Checking [Extended]
We present a new active model-learning approach to generating abstractio...
research
∙
06/01/2021
Exposing Previously Undetectable Faults in Deep Neural Networks
Existing methods for testing DNNs solve the oracle problem by constraini...
research
∙
03/05/2021
Compositional Explanations for Image Classifiers
Existing algorithms for explaining the output of image classifiers perfo...
research
∙
02/07/2021
Neural Termination Analysis
We introduce a novel approach to the automated termination analysis of c...
research
∙
01/20/2021
Shielding Atari Games with Bounded Prescience
Deep reinforcement learning (DRL) is applied in safety-critical domains ...
research
∙
08/31/2020
Ranking Policy Decisions
Policies trained via Reinforcement Learning (RL) are often needlessly co...
research
∙
07/12/2020
The Taint Rabbit: Optimizing Generic Taint Analysis with Dynamic Fast Path Generation
Generic taint analysis is a pivotal technique in software security. Howe...
research
∙
02/26/2020
Cautious Reinforcement Learning with Logical Constraints
This paper presents the concept of an adaptive safe padding that forces ...
research
∙
01/29/2020
Semantic Adversarial Perturbations using Learnt Representations
Adversarial examples for image classifiers are typically created by sear...
research
∙
01/25/2020
CounterExample Guided Neural Synthesis
Program synthesis is the generation of a program from a specification. C...
research
∙
01/15/2020
Learning Concise Models from Long Execution Traces
Abstract models of system-level behaviour have applications in design ex...
research
∙
01/05/2020
Hardware/Software Co-verification Using Path-based Symbolic Execution
Conventional tools for formal hardware/software co-verification use boun...
research
∙
11/22/2019
DeepSynth: Automata Synthesis for Automatic Task Segmentation in Deep Reinforcement Learning
We propose a method for effective training of deep Reinforcement Learnin...
research
∙
11/22/2019
DeepSynth: Program Synthesis for Automatic Task Segmentation in Deep Reinforcement Learning
We propose a method for efficient training of deep Reinforcement Learnin...
research
∙
09/23/2019
Modular Deep Reinforcement Learning with Temporal Logic Specifications
We propose an actor-critic, model-free, and online Reinforcement Learnin...
research
∙
09/11/2019
Reinforcement Learning for Temporal Logic Control Synthesis with Probabilistic Satisfaction Guarantees
Reinforcement Learning (RL) has emerged as an efficient method of choice...
research
∙
08/06/2019
Explaining Deep Neural Networks Using Spectrum-Based Fault Localization
Deep neural networks (DNNs) increasingly replace traditionally developed...
research
∙
08/04/2019
CREST: Hardware Formal Verification with ANSI-C Reference Specifications
This paper presents CREST, a prototype front-end tool intended as an add...
research
∙
05/07/2019
Generating Realistic Unrestricted Adversarial Inputs using Dual-Objective GAN Training
The correctness of deep neural networks is well-known to be vulnerable t...
research
∙
02/02/2019
Certified Reinforcement Learning with Logic Guidance
This paper proposes the first model-free Reinforcement Learning (RL) fra...
research
∙
12/18/2018
Safety and Trustworthiness of Deep Neural Networks: A Survey
In the past few years, significant progress has been made on deep neural...
research
∙
09/20/2018
Logically-Constrained Neural Fitted Q-Iteration
This paper proposes a method for efficient training of the Q-function fo...
research
∙
09/11/2018
Benchmarking of Java Verification Tools at the Software Verification Competition (SV-COMP)
Empirical evaluation of verification tools by benchmarking is a common m...
research
∙
05/09/2018
Evaluating Manual Intervention to Address the Challenges of Bug Finding with KLEE
Symbolic execution has shown its ability to find security-relevant flaws...
research
∙
04/30/2018
Concolic Testing for Deep Neural Networks
Concolic testing alternates between CONCrete program execution and symbO...
research
∙
04/23/2018
Automatic Heap Layout Manipulation for Exploitation
Heap layout manipulation is integral to exploiting heap-based memory cor...
research
∙
04/16/2018
Global Robustness Evaluation of Deep Neural Networks with Provable Guarantees for L0 Norm
Deployment of deep neural networks (DNNs) in safety or security-critical...
research
∙
03/10/2018
Testing Deep Neural Networks
Deep neural networks (DNNs) have a wide range of applications, and softw...
research
∙
01/24/2018
Logically-Correct Reinforcement Learning
We propose a novel Reinforcement Learning (RL) algorithm to synthesize p...
research
∙
12/20/2017
Kayak: Safe Semantic Refactoring to Java Streams
Refactorings are structured changes to existing software that leave its ...
research
∙
11/15/2017
Efficient Verification of Multi-Property Designs (The Benefit of Wrong Assumptions) (Extended Version)
We consider the problem of efficiently checking a set of safety properti...
research
∙
10/10/2016