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

Disgrifiad llawn

Manylion Llyfryddiaeth
Prif Awduron:	Brillout, A, Kroening, D, Rümmer, P, Wahl, T
Awduron Eraill:	Jhala, R
Fformat:	Conference item
Cyhoeddwyd:	Springer 2011

Eitemau Tebyg

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Preface: Special Issue on Interpolation
gan: Kroening, D, et al.
Cyhoeddwyd: (2016)

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

Interpolant Strength
gan: D'Silva, V, et al.
Cyhoeddwyd: (2010)

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

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

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

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

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

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

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

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

Interpolation in local theory extensions
gan: Viorica Sofronie-Stokkermans
Cyhoeddwyd: (2008-10-01)

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

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