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)