Cuts from Proofs: A Complete and Practical Technique for Solving Linear Inequalities over Integers
Abstract elided by the publisher.
Related papers
- Mind the Gap: Bit-vector Interpolation recast over Linear Integer Arithmetic TACAS 2020
- Taming the IXP network processor PLDI 2003
- The geometry of types POPL 2013
- Equality of streams is a Pi0 over 2-complete problem ICFP 2006
- On the linear ranking problem for integer linear-constraint loops POPL 2013
- Learning Union of Integer Hypercubes with Queries - (with Applications to Monadic Decomposition) CAV 2021
- Proof Tree Preserving Interpolation TACAS 2013
- Polynomial invariant generation for non-deterministic recursive programs PLDI 2020