Interpolating bit-vector formulas using uninterpreted predicates and Presburger arithmetic

Peter Backeman, Philipp Rümmer, Aleksandar Zeljic. Interpolating bit-vector formulas using uninterpreted predicates and Presburger arithmetic. Formal Methods in System Design, 57(2):121-156, 2021. [doi]

Authors

Peter Backeman

This author has not been identified. Look up 'Peter Backeman' in Google

Philipp Rümmer

This author has not been identified. Look up 'Philipp Rümmer' in Google

Aleksandar Zeljic

This author has not been identified. Look up 'Aleksandar Zeljic' in Google