173 citations · 655 across the 66 of their papers we have counts for
7 papers · 1 filter
Kayak: Safe Semantic Refactoring to Java Streams
Cristina David, Pascal Kesseli, Daniel Kroening
Refactorings are structured changes to existing software that leave its externally observable behaviour unchanged. Their intent is to improve readability, performance or other non-…
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…
Functional Requirements-Based Automated Testing for Avionics
Youcheng Sun, Martin Brain, Daniel Kroening +7
We propose and demonstrate a method for the reduction of testing effort in safety-critical software development using DO-178 guidance. We achieve this through the application of Bo…
Automated Formal Synthesis of Digital Controllers for State-Space Physical Plants
Alessandro Abate, Iury Bessa, Dario Cattaruzza +5
We present a sound and automated approach to synthesize safe digital feedback controllers for physical plants represented as linear, time invariant models. Models are given as dyna…
Abstract Interpretation with Unfoldings
Marcelo Sousa, César Rodríguez, Vijay D'Silva +1
We present and evaluate a technique for computing path-sensitive interference conditions during abstract interpretation of concurrent programs. In lieu of fixed point computation,…