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

Полное описание

Библиографические подробности
Главные авторы:	Brillout, A, Kroening, D, Rümmer, P, Wahl, T
Другие авторы:	Jhala, R
Формат:	Conference item
Опубликовано:	Springer 2011

Схожие документы

An Interpolating Sequent Calculus for Quantifier-Free Presburger Arithmetic.
по: Brillout, A, и др.
Опубликовано: (2011)

An interpolating sequent calculus for quantifier-free Presburger arithmetic
по: Brillout, A, и др.
Опубликовано: (2011)

Quantifier elimination for counting extensions of Presburger arithmetic
по: Chistikov, D, и др.
Опубликовано: (2022)

Quantifier-Free Boolean Algebra with Presburger Arithmetic is NP-Complete
по: Kuncak, Viktor
Опубликовано: (2007)

Abstraction−based Satisfiability Solving of Presburger Arithmetic
по: Kroening, D, и др.
Опубликовано: (2004)

On Presburger arithmetic extended with non-unary counting quantifiers
по: Peter Habermehl, и др.
Опубликовано: (2023-07-01)

Extensions of Presburger arithmetic and model checking one-counter automata
по: Lechner, A
Опубликовано: (2016)

The complexity of Presburger arithmetic with power or powers
по: Benedikt, M, и др.
Опубликовано: (2023)

Super-exponential Complexity of Presburger Arithmetic
по: Fischer, Michael J., и др.
Опубликовано: (2023)

On the decidability of Presburger arithmetic expanded with powers
по: Karimov, T, и др.
Опубликовано: (2025)

Presburger Arithmetic with algebraic scalar multiplications
по: Philipp Hieronymi, и др.
Опубликовано: (2021-07-01)

An Algorithm for Deciding BAPA: Boolean Algebra with Presburger Arithmetic
по: Kuncak, Viktor, и др.
Опубликовано: (2005)

Unification modulo presburger arithmetic and other decidable theories
по: Mauricio Ayala Rincón, и др.
Опубликовано: (2001-12-01)

Deciding Quantifier-Free Presburger Formulas Using Parameterized Solution Bounds
по: Sanjit A. Seshia, и др.
Опубликовано: (2005-12-01)

Parametric Presburger arithmetic: logic, combinatorics, and quasi-polynomial behavior
по: Tristram Bogart, и др.
Опубликовано: (2017-01-01)

Presburger arithmetic with stars, rational subsets of graph groups, and nested zero tests
по: Haase, C, и др.
Опубликовано: (2019)

Quadratic Word Equations with Length Constraints, Counter Systems, and Presburger Arithmetic with Divisibility
по: Anthony W. Lin, и др.
Опубликовано: (2021-10-01)

Extensions of interpolation between the arithmetic-geometric mean inequality for matrices
по: Mojtaba Bakherad, и др.
Опубликовано: (2017-09-01)

Enrichments of Boolean algebras by Presburger predicates
по: Derakhshan, J, и др.
Опубликовано: (2017)

Model theory of finite-by-Presburger Abelian groups and finite extensions of $p$-adic fields
по: Derakhshan, J, и др.
Опубликовано: (2016)

Mutation-based test case generation for simulink models
по: Brillout, A, и др.
Опубликовано: (2010)

Deciding whether the ordering is necessary in a Presburger formula
по: Christian Choffrut, и др.
Опубликовано: (2010-01-01)

Quantifier-Free Interpolation of a Theory of Arrays
по: Roberto Bruttomesso, и др.
Опубликовано: (2012-04-01)

Interpolation and Uniform Interpolation in Quantifier-Free Fragments of Combined First-Order Theories
по: Silvio Ghilardi, и др.
Опубликовано: (2022-01-01)

On two-variable guarded fragment logic with expressive local Presburger constraints
по: Chia-Hsuan Lu, и др.
Опубликовано: (2024-08-01)

The General Vector Addition System Reachability Problem by Presburger Inductive Invariants
по: leroux jerome
Опубликовано: (2010-09-01)

Preface: Special Issue on Interpolation
по: Kroening, D, и др.
Опубликовано: (2016)

Efficient Interpolant Generation in Satisfiability Modulo Linear Integer Arithmetic
по: Alberto Griggio, и др.
Опубликовано: (2012-08-01)

Interpolant Strength
по: D'Silva, V, и др.
Опубликовано: (2010)

Automatic analysis of DMA races using model checking and k-induction
по: Donaldson, A, и др.
Опубликовано: (2011)

Automatic analysis of DMA races using model checking and k-induction.
по: Donaldson, A, и др.
Опубликовано: (2011)

Lifting Propositional Interpolants to the Word−Level
по: Kroening, D, и др.
Опубликовано: (2007)

About the possibility of the extension of the additive arithmetic
по: Livija Maliaukienė
Опубликовано: (2002-12-01)

ISA Extensions for Finite Field Arithmetic
по: Erdem Alkim, и др.
Опубликовано: (2020-06-01)

Beyond Reachability: Shape Abstraction in the Presence of Pointer Arithmetic
по: Calcagno, C, и др.
Опубликовано: (2006)

Deciding Bit−Vector Arithmetic with Abstraction
по: Bryant, R, и др.
Опубликовано: (2007)

Coverage in interpolation-based model checking
по: Chockler, H, и др.
Опубликовано: (2010)

Interpolation in local theory extensions
по: Viorica Sofronie-Stokkermans
Опубликовано: (2008-10-01)

Higher interpolation and extension for persistence modules
по: Bubenik, P, и др.
Опубликовано: (2017)

An Interpolating Decision Procedure for Transitive Relations with Uninterpreted Functions
по: Kroening, D, и др.
Опубликовано: (2010)