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

Fuld beskrivelse

Bibliografiske detaljer
Main Authors:	Brillout, A, Kroening, D, Rümmer, P, Wahl, T
Andre forfattere:	Jhala, R
Format:	Conference item
Udgivet:	Springer 2011

Lignende værker

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Preface: Special Issue on Interpolation
af: Kroening, D, et al.
Udgivet: (2016)

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

Interpolant Strength
af: D'Silva, V, et al.
Udgivet: (2010)

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

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

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

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

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

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

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

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

Interpolation in local theory extensions
af: Viorica Sofronie-Stokkermans
Udgivet: (2008-10-01)

Higher interpolation and extension for persistence modules
af: Bubenik, P, et al.
Udgivet: (2017)

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