Deciding Quantifier-Free Presburger Formulas Using Parameterized Solution Bounds

DOI10.2168/LMCS-1(2:6)2005zbMATH Open1125.03010MaRDI QIDQ5310643FDOQ5310643

Sanjit A. Seshia, Randal E. Bryant

Publication date: 11 October 2007

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

Recommendations

• scientific article; zbMATH DE number 1979550
• Solving Sparse Linear Constraints
• Computer Aided Verification
• Interpolant based decision procedure for quantifier-free Presburger arithmetic
• scientific article; zbMATH DE number 1979549

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)

Cited In (12)

• Efficient theory combination via Boolean search
• Interpolant Generation for UTVPI
• An Analysis of Slow Convergence in Interval Propagation
• Empirical analysis of algorithms for the shortest negative cost cycle problem
• Design and results of the first satisfiability modulo theories competition (SMT-COMP 2005)
• Optimal length resolution refutations of difference constraint systems
• Cuts from proofs: a complete and practical technique for solving linear inequalities over integers
• Bounding quantification in parametric expansions of Presburger arithmetic
• Title not available (Why is that?)
• Efficient solution of a class of quantified constraints with quantifier prefix exists-forall
• Cutting to the chase.
• Solving Sparse Linear Constraints

Uses Software

• SIMPLIFY
• Chaff
• BerkMin

This page was built for publication: Deciding Quantifier-Free Presburger Formulas Using Parameterized Solution Bounds

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5310643)