Deciding Quantifier-Free Presburger Formulas Using Parameterized Solution Bounds

DOI10.2168/LMCS-1(2:6)2005zbMath1125.03010MaRDI QIDQ5310643

Sanjit A. Seshia, Randal E. Bryant

Publication date: 11 October 2007

Published in: Logical Methods in Computer Science (Search for Journal in Brave)

Mathematics Subject Classification ID

Analysis of algorithms and problem complexity (68Q25) Specification and verification (program logics, model checking, etc.) (68Q60) Decidability of theories and sets of sentences (03B25)

Related Items

Empirical analysis of algorithms for the shortest negative cost cycle problem, Optimal length resolution refutations of difference constraint systems, Design and results of the first satisfiability modulo theories competition (SMT-COMP 2005), Efficient theory combination via Boolean search, An Analysis of Slow Convergence in Interval Propagation, Cuts from proofs: a complete and practical technique for solving linear inequalities over integers, Interpolant Generation for UTVPI, Cutting to the chase.

Uses Software

• SIMPLIFY
• Chaff
• BerkMin