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)