Deciding Quantifier-Free Presburger Formulas Using Parameterized Solution Bounds

DOI10.2168/LMCS-1(2:6)2005MaRDI QIDQ5310643zbMATH OpenFDO

Authors Sanjit A. Seshia, Randal E. Bryant

Publication date 11 October 2007

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

Full work available at URL https://doi.org/10.2168/LMCS-1(2:6)2005

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)

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

Cited in

(12)

• Solving Sparse Linear Constraints
• Efficient theory combination via Boolean search
• An Analysis of Slow Convergence in Interval Propagation
• Interpolant Generation for UTVPI
• 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
• scientific article; zbMATH DE number 1507246 (Why is no real title available?)
• Efficient solution of a class of quantified constraints with quantifier prefix exists-forall
• Cutting to the chase.

Describes a project that uses

Uses Software

• BerkMin
• Chaff
• SIMPLIFY

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)