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

書目詳細資料
Main Authors:	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, et al.
出版: (2011)

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

Quantifier elimination for counting extensions of Presburger arithmetic
由: Chistikov, D, et al.
出版: (2022)

Quantifier-Free Boolean Algebra with Presburger Arithmetic is NP-Complete
由: Kuncak, Viktor
出版: (2007)

Abstraction−based Satisfiability Solving of Presburger Arithmetic
由: Kroening, D, et al.
出版: (2004)

On Presburger arithmetic extended with non-unary counting quantifiers
由: Peter Habermehl, et al.
出版: (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, et al.
出版: (2023)

Super-exponential Complexity of Presburger Arithmetic
由: Fischer, Michael J., et al.
出版: (2023)

On the decidability of Presburger arithmetic expanded with powers
由: Karimov, T, et al.
出版: (2025)

Presburger Arithmetic with algebraic scalar multiplications
由: Philipp Hieronymi, et al.
出版: (2021-07-01)

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

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

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

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

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

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

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

Enrichments of Boolean algebras by Presburger predicates
由: Derakhshan, J, et al.
出版: (2017)

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

Mutation-based test case generation for simulink models
由: Brillout, A, et al.
出版: (2010)

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

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

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

On two-variable guarded fragment logic with expressive local Presburger constraints
由: Chia-Hsuan Lu, et al.
出版: (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, et al.
出版: (2016)

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

Interpolant Strength
由: D'Silva, V, et al.
出版: (2010)

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

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

Lifting Propositional Interpolants to the Word−Level
由: Kroening, D, et al.
出版: (2007)

About the possibility of the extension of the additive arithmetic
由: Livija Maliaukienė
出版: (2002-12-01)

ISA Extensions for Finite Field Arithmetic
由: Erdem Alkim, et al.
出版: (2020-06-01)

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

Deciding Bit−Vector Arithmetic with Abstraction
由: Bryant, R, et al.
出版: (2007)

Coverage in interpolation-based model checking
由: Chockler, H, et al.
出版: (2010)

Interpolation in local theory extensions
由: Viorica Sofronie-Stokkermans
出版: (2008-10-01)

Higher interpolation and extension for persistence modules
由: Bubenik, P, et al.
出版: (2017)

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