VIRAS: Conflict-Driven Quantifier Elimination for Integer-Real Arithmetic.

Johannes Schoisswohl, Laura Kovcs, Konstantin Korovin

Browse the full LPAR paper archive.