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...

Descripció completa

Dades bibliogràfiques
Autors principals:	Brillout, A, Kroening, D, Rümmer, P, Wahl, T
Altres autors:	Jhala, R
Format:	Conference item
Publicat:	Springer 2011

Ítems similars

An Interpolating Sequent Calculus for Quantifier-Free Presburger Arithmetic.
per: Brillout, A, et al.
Publicat: (2011)

An interpolating sequent calculus for quantifier-free Presburger arithmetic
per: Brillout, A, et al.
Publicat: (2011)

Quantifier elimination for counting extensions of Presburger arithmetic
per: Chistikov, D, et al.
Publicat: (2022)

Quantifier-Free Boolean Algebra with Presburger Arithmetic is NP-Complete
per: Kuncak, Viktor
Publicat: (2007)

Abstraction−based Satisfiability Solving of Presburger Arithmetic
per: Kroening, D, et al.
Publicat: (2004)

On Presburger arithmetic extended with non-unary counting quantifiers
per: Peter Habermehl, et al.
Publicat: (2023-07-01)

Extensions of Presburger arithmetic and model checking one-counter automata
per: Lechner, A
Publicat: (2016)

The complexity of Presburger arithmetic with power or powers
per: Benedikt, M, et al.
Publicat: (2023)

Super-exponential Complexity of Presburger Arithmetic
per: Fischer, Michael J., et al.
Publicat: (2023)

On the decidability of Presburger arithmetic expanded with powers
per: Karimov, T, et al.
Publicat: (2025)

Presburger Arithmetic with algebraic scalar multiplications
per: Philipp Hieronymi, et al.
Publicat: (2021-07-01)

An Algorithm for Deciding BAPA: Boolean Algebra with Presburger Arithmetic
per: Kuncak, Viktor, et al.
Publicat: (2005)

Unification modulo presburger arithmetic and other decidable theories
per: Mauricio Ayala Rincón, et al.
Publicat: (2001-12-01)

Parametric Presburger arithmetic: logic, combinatorics, and quasi-polynomial behavior
per: Tristram Bogart, et al.
Publicat: (2017-01-01)

Deciding Quantifier-Free Presburger Formulas Using Parameterized Solution Bounds
per: Sanjit A. Seshia, et al.
Publicat: (2005-12-01)

Presburger arithmetic with stars, rational subsets of graph groups, and nested zero tests
per: Haase, C, et al.
Publicat: (2019)

Quadratic Word Equations with Length Constraints, Counter Systems, and Presburger Arithmetic with Divisibility
per: Anthony W. Lin, et al.
Publicat: (2021-10-01)

Extensions of interpolation between the arithmetic-geometric mean inequality for matrices
per: Mojtaba Bakherad, et al.
Publicat: (2017-09-01)

Enrichments of Boolean algebras by Presburger predicates
per: Derakhshan, J, et al.
Publicat: (2017)

Model theory of finite-by-Presburger Abelian groups and finite extensions of $p$-adic fields
per: Derakhshan, J, et al.
Publicat: (2016)

Mutation-based test case generation for simulink models
per: Brillout, A, et al.
Publicat: (2010)

Deciding whether the ordering is necessary in a Presburger formula
per: Christian Choffrut, et al.
Publicat: (2010-01-01)

Quantifier-Free Interpolation of a Theory of Arrays
per: Roberto Bruttomesso, et al.
Publicat: (2012-04-01)

Interpolation and Uniform Interpolation in Quantifier-Free Fragments of Combined First-Order Theories
per: Silvio Ghilardi, et al.
Publicat: (2022-01-01)

On two-variable guarded fragment logic with expressive local Presburger constraints
per: Chia-Hsuan Lu, et al.
Publicat: (2024-08-01)

The General Vector Addition System Reachability Problem by Presburger Inductive Invariants
per: leroux jerome
Publicat: (2010-09-01)

Preface: Special Issue on Interpolation
per: Kroening, D, et al.
Publicat: (2016)

Efficient Interpolant Generation in Satisfiability Modulo Linear Integer Arithmetic
per: Alberto Griggio, et al.
Publicat: (2012-08-01)

Interpolant Strength
per: D'Silva, V, et al.
Publicat: (2010)

Automatic analysis of DMA races using model checking and k-induction
per: Donaldson, A, et al.
Publicat: (2011)

Automatic analysis of DMA races using model checking and k-induction.
per: Donaldson, A, et al.
Publicat: (2011)

Lifting Propositional Interpolants to the Word−Level
per: Kroening, D, et al.
Publicat: (2007)

About the possibility of the extension of the additive arithmetic
per: Livija Maliaukienė
Publicat: (2002-12-01)

ISA Extensions for Finite Field Arithmetic
per: Erdem Alkim, et al.
Publicat: (2020-06-01)

Beyond Reachability: Shape Abstraction in the Presence of Pointer Arithmetic
per: Calcagno, C, et al.
Publicat: (2006)

Deciding Bit−Vector Arithmetic with Abstraction
per: Bryant, R, et al.
Publicat: (2007)

Coverage in interpolation-based model checking
per: Chockler, H, et al.
Publicat: (2010)

Interpolation in local theory extensions
per: Viorica Sofronie-Stokkermans
Publicat: (2008-10-01)

Higher interpolation and extension for persistence modules
per: Bubenik, P, et al.
Publicat: (2017)

An Interpolating Decision Procedure for Transitive Relations with Uninterpreted Functions
per: Kroening, D, et al.
Publicat: (2010)