Automatic heap layout manipulation for exploitation by Heelan, S, Melham, TF, Kroening, D

“…We present a framework for benchmarking heap layout manipulation algorithms, and use it to evaluate our approach on several real-world allocators, showing that pseudo-random black box search can be highly effective. …”

Deciding floating-point logic with abstract conflict driven clause learning by Brain, M, Silva, V, Griggio, A, Haller, L, Kroening, D

“…Our new technique is faster than a bit-vector encoding approach on 80 % of the benchmarks, and is faster by one order of magnitude or more on 60 % of the benchmarks. …”

JBMC: a bounded model checking tool for verifying Java bytecode by Cordeiro, L, Kesseli, P, Kroening, D, Schrammel, P, Trtik, M

“…Experimental results show that JBMC can correctly verify a set of Java benchmarks from the literature and that it is competitive with two state-of-the-art Java verifiers. …”

Model checking concurrent linux device drivers by Witkowski, T, Blanc, N, Kroening, D, Weissenbacher, G

“…Our predicate abstraction-based tool DDVERIFY enables the automated verification of Linux device drivers and provides an accurate model of the relevant parts of the kernel. We report on benchmarks based on Linux device drivers, confirming the results that SLAM established for the Windows world. …”

Editorial. by Kroening, D, Margaria, T, Woodcock, J

“…The verification community has identified benchmarks, tools and technologies that are useful for attacking a series of problems, and has started to compare those tools.…”

Optimizing a primitive based approach to generic taint analysis by Galea, J

“…</p> <p>The optimizations are integrated into a generic taint tracker called the Taint Rabbit, and their effectiveness is evaluated on various real-world software and CPU-bound benchmarks. With average speed-ups of around 42% on SPEC CPU benchmarks, and as high as 99% on data compression tools, our results demonstrate the advancement of optimized and generic taint analysis.…”

Software verification for weak memory via program transformation by Alglave, J, Kroening, D, Nimal, V, Tautschnig, M

“…We present experiments for a broad variety of models (from x86-TSO to Power) and a vast range of verification tools, quantify the additional cost of the transformation and highlight the cases when we can drastically reduce it. Our benchmarks include work-queue management code from PostgreSQL.…”

Unfolding-based partial order reduction by Rodríguez, C, Sousa, M, Sharma, S, Kroening, D

“…Furthermore, our unfolding-based POR copes with non-terminating executions and incorporates state caching. On benchmarks with busy-waits, among others, our experiments show a dramatic reduction in the number of executions when compared to a state-of-the-art DPOR.…”

Using program synthesis for program analysis by David, C, Kroening, D, Lewis, M

“…Our experimental results show that, on benchmarks capturing static analysis problems, our program synthesiser compares positively with other general purpose synthesisers.…”

Strengthening properties using abstraction refinement by Purandare, M, Wahl, T, Kroening, D

“…We quantify the benefits of our technique on a substantial set of circuit benchmarks.…”

An interpolating sequent calculus for quantifier-free Presburger arithmetic by Brillout, A, Kroening, D, Rümmer, P, al., E

“…We have extended the Princess theorem prover to generate interpolating proofs, and applied it to a large number of publicly available Presburger arithmetic benchmarks. The results document the robustness and efficiency of our interpolation procedure. …”

Counterexample guided inductive synthesis modulo theories by Abate, A, David, C, Kesseli, P, Kroening, D, Polgreen, E

“…We demonstrate the practical value of CEGIS(T ) by automatically synthesizing programs for a set of intricate benchmarks.…”

Formal co−validation of low−level hardware/software interfaces by Horn, A, Tautschnig, M, Val, C, Liang, L, Melham, T, Grundy, J, Kroening, D

“…We illustrate and evaluate our technique on three realistic benchmarks in which software I/O is subject to hardware-specific protocol rules: a real-time clock, a temperature sensor on an I2C bus, and an Ethernet MAC. …”

Formal Co-Validation of Low-Level Hardware/Software Interfaces by Horn, A, Tautschnig, M, Val, C, Liang, L, Melham, T, Grundy, J, Kroening, D, IEEE

“…We illustrate and evaluate our technique on three realistic benchmarks in which software I/O is subject to hardware-specific protocol rules: a real-time clock, a temperature sensor on an I2C bus, and an Ethernet MAC. …”

Accelerated test execution using GPUs by Rajan, A, Sharma, S, Schrammel, P, Kroening, D

“…We observe speed-ups up to a factor of 27 compared to single-core execution on conventional CPUs with embedded systems benchmark programs.…”

The taint rabbit: optimizing generic taint analysis with dynamic fast path generation by Galea, J, Kroening, D

“…For instance, Dytan incurs an average overhead of 237x, while the Taint Rabbit achieves 1.7x on the same set of benchmarks. This compares favorably to the 1.5x overhead delivered by the bitwise, non-generic, taint engine LibDFT.…”

Probabilistic fault localisation by Landsberg, D, Chockler, H, Kroening, D

“…Furthermore, we show that it is theoretically impossible to design strictly rational sbfl measures that outperform pfl techniques on a large set of benchmarks.…”

Property-Driven Fence Insertion using Reorder Bounded Model Checking by Joshi, S, Kroening, D

“…Our experimental results show that our technique is faster and solves more instances of relevant benchmarks than earlier approaches.…”

Fixed points for multi-cycle path detection by D'Silva, V, Kroening, D

“…Our implementation performs well on several benchmarks, including an exponential improvement on circuits analysed in the literature.…”

Under-approximating loops in C programs for fast counterexample detection by Kroening, D, Lewis, M, Weissenbacher, G

“…We paired our techniques with lazy abstraction and bounded model checking, and evaluated the resulting tool on a number of buffer overflow benchmarks, demonstrating its ability to efficiently detect deep counterexamples in C programs that manipulate arrays.…”