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

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

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)

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

Describes a project that uses

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)