39 citations · 68 across the 11 of their papers we have counts for
12 papers
LCRL: Certified Policy Synthesis via Logically-Constrained Reinforcement Learning
Hosein Hasanbeig, Daniel Kroening, Alessandro Abate
LCRL is a software tool that implements model-free Reinforcement Learning (RL) algorithms over unknown Markov Decision Processes (MDPs), synthesising policies that satisfy a given…
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…
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…
Satisfiability Checking meets Symbolic Computation (Project Paper)
E. Abraham, J. Abbott, B. Becker +12
Symbolic Computation and Satisfiability Checking are two research areas, both having their individual scientific focus but sharing also common interests in the development, impleme…
Sound Static Deadlock Analysis for C/Pthreads (Extended Version)
Daniel Kroening, Daniel Poetzl, Peter Schrammel +1
We present a static deadlock analysis approach for C/pthreads. The design of our method has been guided by the requirement to analyse real-world code. Our approach is sound (i.e.,…
AbPress: Flexing Partial-Order Reduction and Abstraction
Daniel Kroening, Subodh Sharma, Björn Wachter
Partial-order reduction (POR) and lazy abstraction with interpolants are two complementary techniques that have been successfully employed to make model checking tools for concurre…