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)