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

Mô tả đầy đủ

Chi tiết về thư mục
Những tác giả chính:	Brillout, A, Kroening, D, Rümmer, P, Wahl, T
Tác giả khác:	Jhala, R
Định dạng:	Conference item
Được phát hành:	Springer 2011

Những quyển sách tương tự

An Interpolating Sequent Calculus for Quantifier-Free Presburger Arithmetic.
Bằng: Brillout, A, et al.
Được phát hành: (2011)

An interpolating sequent calculus for quantifier-free Presburger arithmetic
Bằng: Brillout, A, et al.
Được phát hành: (2011)

Quantifier elimination for counting extensions of Presburger arithmetic
Bằng: Chistikov, D, et al.
Được phát hành: (2022)

Quantifier-Free Boolean Algebra with Presburger Arithmetic is NP-Complete
Bằng: Kuncak, Viktor
Được phát hành: (2007)

Abstraction−based Satisfiability Solving of Presburger Arithmetic
Bằng: Kroening, D, et al.
Được phát hành: (2004)

On Presburger arithmetic extended with non-unary counting quantifiers
Bằng: Peter Habermehl, et al.
Được phát hành: (2023-07-01)

Extensions of Presburger arithmetic and model checking one-counter automata
Bằng: Lechner, A
Được phát hành: (2016)

The complexity of Presburger arithmetic with power or powers
Bằng: Benedikt, M, et al.
Được phát hành: (2023)

Super-exponential Complexity of Presburger Arithmetic
Bằng: Fischer, Michael J., et al.
Được phát hành: (2023)

On the decidability of Presburger arithmetic expanded with powers
Bằng: Karimov, T, et al.
Được phát hành: (2025)

Presburger Arithmetic with algebraic scalar multiplications
Bằng: Philipp Hieronymi, et al.
Được phát hành: (2021-07-01)

An Algorithm for Deciding BAPA: Boolean Algebra with Presburger Arithmetic
Bằng: Kuncak, Viktor, et al.
Được phát hành: (2005)

Unification modulo presburger arithmetic and other decidable theories
Bằng: Mauricio Ayala Rincón, et al.
Được phát hành: (2001-12-01)

Deciding Quantifier-Free Presburger Formulas Using Parameterized Solution Bounds
Bằng: Sanjit A. Seshia, et al.
Được phát hành: (2005-12-01)

Parametric Presburger arithmetic: logic, combinatorics, and quasi-polynomial behavior
Bằng: Tristram Bogart, et al.
Được phát hành: (2017-01-01)

Presburger arithmetic with stars, rational subsets of graph groups, and nested zero tests
Bằng: Haase, C, et al.
Được phát hành: (2019)

Quadratic Word Equations with Length Constraints, Counter Systems, and Presburger Arithmetic with Divisibility
Bằng: Anthony W. Lin, et al.
Được phát hành: (2021-10-01)

Extensions of interpolation between the arithmetic-geometric mean inequality for matrices
Bằng: Mojtaba Bakherad, et al.
Được phát hành: (2017-09-01)

Enrichments of Boolean algebras by Presburger predicates
Bằng: Derakhshan, J, et al.
Được phát hành: (2017)

Model theory of finite-by-Presburger Abelian groups and finite extensions of $p$-adic fields
Bằng: Derakhshan, J, et al.
Được phát hành: (2016)

Mutation-based test case generation for simulink models
Bằng: Brillout, A, et al.
Được phát hành: (2010)

Deciding whether the ordering is necessary in a Presburger formula
Bằng: Christian Choffrut, et al.
Được phát hành: (2010-01-01)

Quantifier-Free Interpolation of a Theory of Arrays
Bằng: Roberto Bruttomesso, et al.
Được phát hành: (2012-04-01)

Interpolation and Uniform Interpolation in Quantifier-Free Fragments of Combined First-Order Theories
Bằng: Silvio Ghilardi, et al.
Được phát hành: (2022-01-01)

On two-variable guarded fragment logic with expressive local Presburger constraints
Bằng: Chia-Hsuan Lu, et al.
Được phát hành: (2024-08-01)

The General Vector Addition System Reachability Problem by Presburger Inductive Invariants
Bằng: leroux jerome
Được phát hành: (2010-09-01)

Preface: Special Issue on Interpolation
Bằng: Kroening, D, et al.
Được phát hành: (2016)

Efficient Interpolant Generation in Satisfiability Modulo Linear Integer Arithmetic
Bằng: Alberto Griggio, et al.
Được phát hành: (2012-08-01)

Interpolant Strength
Bằng: D'Silva, V, et al.
Được phát hành: (2010)

Automatic analysis of DMA races using model checking and k-induction
Bằng: Donaldson, A, et al.
Được phát hành: (2011)

Automatic analysis of DMA races using model checking and k-induction.
Bằng: Donaldson, A, et al.
Được phát hành: (2011)

Lifting Propositional Interpolants to the Word−Level
Bằng: Kroening, D, et al.
Được phát hành: (2007)

About the possibility of the extension of the additive arithmetic
Bằng: Livija Maliaukienė
Được phát hành: (2002-12-01)

ISA Extensions for Finite Field Arithmetic
Bằng: Erdem Alkim, et al.
Được phát hành: (2020-06-01)

Beyond Reachability: Shape Abstraction in the Presence of Pointer Arithmetic
Bằng: Calcagno, C, et al.
Được phát hành: (2006)

Deciding Bit−Vector Arithmetic with Abstraction
Bằng: Bryant, R, et al.
Được phát hành: (2007)

Coverage in interpolation-based model checking
Bằng: Chockler, H, et al.
Được phát hành: (2010)

Interpolation in local theory extensions
Bằng: Viorica Sofronie-Stokkermans
Được phát hành: (2008-10-01)

Higher interpolation and extension for persistence modules
Bằng: Bubenik, P, et al.
Được phát hành: (2017)

An Interpolating Decision Procedure for Transitive Relations with Uninterpreted Functions
Bằng: Kroening, D, et al.
Được phát hành: (2010)