Ranking function synthesis for bit-vector relations by Cook, B, Kroening, D, Rümmer, P, Wintersteiger, C

Digitaltechnik by Biere, A, Kroening, D, Weissenbacher, G, Wintersteiger, C

Termination analysis with compositional transition invariants by Kroening, D, Sharygina, N, Tsitovich, A, Wintersteiger, C

Loop summarization using state and transition invariants by Kroening, D, Sharygina, N, Tonetta, S, Tsitovich, A, Wintersteiger, C

Loop summarization using state and transition invariants. by Kroening, D, Sharygina, N, Tonetta, S, Tsitovich, A, Wintersteiger, C

A First Step Towards a Unified Proof Checker for QBF by Jussila, T, Biere, A, Sinz, C, Kroening, D, Wintersteiger, C

Analyzing and Synthesizing Genomic Logic Functions by Paoletti, N, Yordanov, B, Hamadi, Y, Wintersteiger, C, Kugler, H