Beyond quantifier-free interpolation in extensions of presburger arithmetic

Beyond quantifier-free interpolation in extensions of presburger arithmetic

Craig interpolation has emerged as an effective means of generating candidate program invariants. We present interpolation procedures for the theories of Presburger arithmetic combined with (i) uninterpreted predicates (QPA+UP), (ii) uninterpreted functions (QPA+UF) and (iii) extensional arrays (QPA...

Cur síos iomlán

Sonraí bibleagrafaíochta
Príomhchruthaitheoirí:	Brillout, A, Kroening, D, Rümmer, P, Wahl, T
Rannpháirtithe:	Jhala, R
Formáid:	Conference item
Foilsithe / Cruthaithe:	Springer 2011

Míreanna comhchosúla

An Interpolating Sequent Calculus for Quantifier-Free Presburger Arithmetic.
de réir: Brillout, A, et al.
Foilsithe / Cruthaithe: (2011)

An interpolating sequent calculus for quantifier-free Presburger arithmetic
de réir: Brillout, A, et al.
Foilsithe / Cruthaithe: (2011)

Quantifier elimination for counting extensions of Presburger arithmetic
de réir: Chistikov, D, et al.
Foilsithe / Cruthaithe: (2022)

Quantifier-Free Boolean Algebra with Presburger Arithmetic is NP-Complete
de réir: Kuncak, Viktor
Foilsithe / Cruthaithe: (2007)

Abstraction−based Satisfiability Solving of Presburger Arithmetic
de réir: Kroening, D, et al.
Foilsithe / Cruthaithe: (2004)

On Presburger arithmetic extended with non-unary counting quantifiers
de réir: Peter Habermehl, et al.
Foilsithe / Cruthaithe: (2023-07-01)

Extensions of Presburger arithmetic and model checking one-counter automata
de réir: Lechner, A
Foilsithe / Cruthaithe: (2016)

The complexity of Presburger arithmetic with power or powers
de réir: Benedikt, M, et al.
Foilsithe / Cruthaithe: (2023)

Super-exponential Complexity of Presburger Arithmetic
de réir: Fischer, Michael J., et al.
Foilsithe / Cruthaithe: (2023)

On the decidability of Presburger arithmetic expanded with powers
de réir: Karimov, T, et al.
Foilsithe / Cruthaithe: (2025)

Presburger Arithmetic with algebraic scalar multiplications
de réir: Philipp Hieronymi, et al.
Foilsithe / Cruthaithe: (2021-07-01)

An Algorithm for Deciding BAPA: Boolean Algebra with Presburger Arithmetic
de réir: Kuncak, Viktor, et al.
Foilsithe / Cruthaithe: (2005)

Unification modulo presburger arithmetic and other decidable theories
de réir: Mauricio Ayala Rincón, et al.
Foilsithe / Cruthaithe: (2001-12-01)

Deciding Quantifier-Free Presburger Formulas Using Parameterized Solution Bounds
de réir: Sanjit A. Seshia, et al.
Foilsithe / Cruthaithe: (2005-12-01)

Parametric Presburger arithmetic: logic, combinatorics, and quasi-polynomial behavior
de réir: Tristram Bogart, et al.
Foilsithe / Cruthaithe: (2017-01-01)

Presburger arithmetic with stars, rational subsets of graph groups, and nested zero tests
de réir: Haase, C, et al.
Foilsithe / Cruthaithe: (2019)

Quadratic Word Equations with Length Constraints, Counter Systems, and Presburger Arithmetic with Divisibility
de réir: Anthony W. Lin, et al.
Foilsithe / Cruthaithe: (2021-10-01)

Extensions of interpolation between the arithmetic-geometric mean inequality for matrices
de réir: Mojtaba Bakherad, et al.
Foilsithe / Cruthaithe: (2017-09-01)

Enrichments of Boolean algebras by Presburger predicates
de réir: Derakhshan, J, et al.
Foilsithe / Cruthaithe: (2017)

Model theory of finite-by-Presburger Abelian groups and finite extensions of $p$-adic fields
de réir: Derakhshan, J, et al.
Foilsithe / Cruthaithe: (2016)

Mutation-based test case generation for simulink models
de réir: Brillout, A, et al.
Foilsithe / Cruthaithe: (2010)

Deciding whether the ordering is necessary in a Presburger formula
de réir: Christian Choffrut, et al.
Foilsithe / Cruthaithe: (2010-01-01)

Quantifier-Free Interpolation of a Theory of Arrays
de réir: Roberto Bruttomesso, et al.
Foilsithe / Cruthaithe: (2012-04-01)

Interpolation and Uniform Interpolation in Quantifier-Free Fragments of Combined First-Order Theories
de réir: Silvio Ghilardi, et al.
Foilsithe / Cruthaithe: (2022-01-01)

On two-variable guarded fragment logic with expressive local Presburger constraints
de réir: Chia-Hsuan Lu, et al.
Foilsithe / Cruthaithe: (2024-08-01)

The General Vector Addition System Reachability Problem by Presburger Inductive Invariants
de réir: leroux jerome
Foilsithe / Cruthaithe: (2010-09-01)

Preface: Special Issue on Interpolation
de réir: Kroening, D, et al.
Foilsithe / Cruthaithe: (2016)

Efficient Interpolant Generation in Satisfiability Modulo Linear Integer Arithmetic
de réir: Alberto Griggio, et al.
Foilsithe / Cruthaithe: (2012-08-01)

Interpolant Strength
de réir: D'Silva, V, et al.
Foilsithe / Cruthaithe: (2010)

Automatic analysis of DMA races using model checking and k-induction
de réir: Donaldson, A, et al.
Foilsithe / Cruthaithe: (2011)

Automatic analysis of DMA races using model checking and k-induction.
de réir: Donaldson, A, et al.
Foilsithe / Cruthaithe: (2011)

Lifting Propositional Interpolants to the Word−Level
de réir: Kroening, D, et al.
Foilsithe / Cruthaithe: (2007)

About the possibility of the extension of the additive arithmetic
de réir: Livija Maliaukienė
Foilsithe / Cruthaithe: (2002-12-01)

ISA Extensions for Finite Field Arithmetic
de réir: Erdem Alkim, et al.
Foilsithe / Cruthaithe: (2020-06-01)

Beyond Reachability: Shape Abstraction in the Presence of Pointer Arithmetic
de réir: Calcagno, C, et al.
Foilsithe / Cruthaithe: (2006)

Deciding Bit−Vector Arithmetic with Abstraction
de réir: Bryant, R, et al.
Foilsithe / Cruthaithe: (2007)

Coverage in interpolation-based model checking
de réir: Chockler, H, et al.
Foilsithe / Cruthaithe: (2010)

Interpolation in local theory extensions
de réir: Viorica Sofronie-Stokkermans
Foilsithe / Cruthaithe: (2008-10-01)

Higher interpolation and extension for persistence modules
de réir: Bubenik, P, et al.
Foilsithe / Cruthaithe: (2017)

An Interpolating Decision Procedure for Transitive Relations with Uninterpreted Functions
de réir: Kroening, D, et al.
Foilsithe / Cruthaithe: (2010)