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

Szczegółowa specyfikacja

Opis bibliograficzny
Główni autorzy:	Brillout, A, Kroening, D, Rümmer, P, Wahl, T
Kolejni autorzy:	Jhala, R
Format:	Conference item
Wydane:	Springer 2011

Podobne zapisy

An Interpolating Sequent Calculus for Quantifier-Free Presburger Arithmetic.
od: Brillout, A, i wsp.
Wydane: (2011)

An interpolating sequent calculus for quantifier-free Presburger arithmetic
od: Brillout, A, i wsp.
Wydane: (2011)

Quantifier elimination for counting extensions of Presburger arithmetic
od: Chistikov, D, i wsp.
Wydane: (2022)

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

Abstraction−based Satisfiability Solving of Presburger Arithmetic
od: Kroening, D, i wsp.
Wydane: (2004)

On Presburger arithmetic extended with non-unary counting quantifiers
od: Peter Habermehl, i wsp.
Wydane: (2023-07-01)

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

The complexity of Presburger arithmetic with power or powers
od: Benedikt, M, i wsp.
Wydane: (2023)

Super-exponential Complexity of Presburger Arithmetic
od: Fischer, Michael J., i wsp.
Wydane: (2023)

On the decidability of Presburger arithmetic expanded with powers
od: Karimov, T, i wsp.
Wydane: (2025)

Presburger Arithmetic with algebraic scalar multiplications
od: Philipp Hieronymi, i wsp.
Wydane: (2021-07-01)

An Algorithm for Deciding BAPA: Boolean Algebra with Presburger Arithmetic
od: Kuncak, Viktor, i wsp.
Wydane: (2005)

Unification modulo presburger arithmetic and other decidable theories
od: Mauricio Ayala Rincón, i wsp.
Wydane: (2001-12-01)

Parametric Presburger arithmetic: logic, combinatorics, and quasi-polynomial behavior
od: Tristram Bogart, i wsp.
Wydane: (2017-01-01)

Deciding Quantifier-Free Presburger Formulas Using Parameterized Solution Bounds
od: Sanjit A. Seshia, i wsp.
Wydane: (2005-12-01)

Presburger arithmetic with stars, rational subsets of graph groups, and nested zero tests
od: Haase, C, i wsp.
Wydane: (2019)

Quadratic Word Equations with Length Constraints, Counter Systems, and Presburger Arithmetic with Divisibility
od: Anthony W. Lin, i wsp.
Wydane: (2021-10-01)

Extensions of interpolation between the arithmetic-geometric mean inequality for matrices
od: Mojtaba Bakherad, i wsp.
Wydane: (2017-09-01)

Enrichments of Boolean algebras by Presburger predicates
od: Derakhshan, J, i wsp.
Wydane: (2017)

Model theory of finite-by-Presburger Abelian groups and finite extensions of $p$-adic fields
od: Derakhshan, J, i wsp.
Wydane: (2016)

Mutation-based test case generation for simulink models
od: Brillout, A, i wsp.
Wydane: (2010)

Deciding whether the ordering is necessary in a Presburger formula
od: Christian Choffrut, i wsp.
Wydane: (2010-01-01)

Quantifier-Free Interpolation of a Theory of Arrays
od: Roberto Bruttomesso, i wsp.
Wydane: (2012-04-01)

Interpolation and Uniform Interpolation in Quantifier-Free Fragments of Combined First-Order Theories
od: Silvio Ghilardi, i wsp.
Wydane: (2022-01-01)

On two-variable guarded fragment logic with expressive local Presburger constraints
od: Chia-Hsuan Lu, i wsp.
Wydane: (2024-08-01)

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

Preface: Special Issue on Interpolation
od: Kroening, D, i wsp.
Wydane: (2016)

Efficient Interpolant Generation in Satisfiability Modulo Linear Integer Arithmetic
od: Alberto Griggio, i wsp.
Wydane: (2012-08-01)

Interpolant Strength
od: D'Silva, V, i wsp.
Wydane: (2010)

Lifting Propositional Interpolants to the Word−Level
od: Kroening, D, i wsp.
Wydane: (2007)

Automatic analysis of DMA races using model checking and k-induction
od: Donaldson, A, i wsp.
Wydane: (2011)

Automatic analysis of DMA races using model checking and k-induction.
od: Donaldson, A, i wsp.
Wydane: (2011)

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

ISA Extensions for Finite Field Arithmetic
od: Erdem Alkim, i wsp.
Wydane: (2020-06-01)

Beyond Reachability: Shape Abstraction in the Presence of Pointer Arithmetic
od: Calcagno, C, i wsp.
Wydane: (2006)

Deciding Bit−Vector Arithmetic with Abstraction
od: Bryant, R, i wsp.
Wydane: (2007)

Coverage in interpolation-based model checking
od: Chockler, H, i wsp.
Wydane: (2010)

An Interpolating Decision Procedure for Transitive Relations with Uninterpreted Functions
od: Kroening, D, i wsp.
Wydane: (2010)

An interpolating decision procedure for transitive relations with uninterpreted functions
od: Kroening, D, i wsp.
Wydane: (2009)

Interpolation in local theory extensions
od: Viorica Sofronie-Stokkermans
Wydane: (2008-10-01)