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

Descrizione completa

Dettagli Bibliografici
Autori principali:	Brillout, A, Kroening, D, Rümmer, P, Wahl, T
Altri autori:	Jhala, R
Natura:	Conference item
Pubblicazione:	Springer 2011

Documenti analoghi

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Preface: Special Issue on Interpolation
di: Kroening, D, et al.
Pubblicazione: (2016)

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

Interpolant Strength
di: D'Silva, V, et al.
Pubblicazione: (2010)

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

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

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

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

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

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

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

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

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

An interpolating decision procedure for transitive relations with uninterpreted functions
di: Kroening, D, et al.
Pubblicazione: (2009)

Interpolation in local theory extensions
di: Viorica Sofronie-Stokkermans
Pubblicazione: (2008-10-01)