173 citations · 655 across the 66 of their papers we have counts for
19 papers · 1 filter
CounterExample Guided Neural Synthesis
Elizabeth Polgreen, Ralph Abboud, Daniel Kroening
Program synthesis is the generation of a program from a specification. Correct synthesis is difficult, and methods that provide formal guarantees suffer from scalability issues. On…
Reinforcement Learning for Temporal Logic Control Synthesis with Probabilistic Satisfaction Guarantees
Mohammadhosein Hasanbeig, Yiannis Kantaros, Alessandro Abate +3
Reinforcement Learning (RL) has emerged as an efficient method of choice for solving complex sequential decision making problems in automatic control, computer science, economics,…
Benchmarking of Java Verification Tools at the Software Verification Competition (SV-COMP)
Lucas Cordeiro, Daniel Kroening, Peter Schrammel
Empirical evaluation of verification tools by benchmarking is a common method in software verification research. The Competition on Software Verification (SV-COMP) aims at standard…
Efficient Verification of Multi-Property Designs (The Benefit of Wrong Assumptions) (Extended Version)
Eugene Goldberg, Matthias Gudemann, Daniel Kroening +1
We consider the problem of efficiently checking a set of safety properties P1,....,Pk of one design. We introduce a new approach called JA-verification where JA stands for "Just-As…
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…
Verification of the Tree-Based Hierarchical Read-Copy Update in the Linux Kernel
Lihao Liang, Paul E. McKenney, Daniel Kroening +1
Read-Copy Update (RCU) is a scalable, high-performance Linux-kernel synchronization mechanism that runs low-overhead readers concurrently with updaters. Production-quality RCU impl…