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)

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)

• Bounding quantification in parametric expansions of Presburger arithmetic
• Solving Sparse Linear Constraints
• 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
• scientific article; zbMATH DE number 1507246 (Why is no real title available?)
• Interpolant Generation for UTVPI
• Empirical analysis of algorithms for the shortest negative cost cycle problem
• Cuts from proofs: a complete and practical technique for solving linear inequalities over integers
• An Analysis of Slow Convergence in Interval Propagation
• Efficient solution of a class of quantified constraints with quantifier prefix exists-forall
• Cutting to the chase.

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)