An interpolating sequent calculus for quantifier-free Presburger arithmetic

An interpolating sequent calculus for quantifier-free Presburger arithmetic

Show other versions (1)

Craig interpolation has become a versatile tool in formal verification, used for instance to generate program assertions that serve as candidates for loop invariants. In this paper, we consider Craig interpolation for quantifier-free Presburger arithmetic (QFPA). Until recently, quantifier eliminati...

Bibliografske podrobnosti
Main Authors:	Brillout, A, Kroening, D, Rümmer, P, al., E
Format:	Journal article
Izdano:	Springer 2011

Podobne knjige/članki

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

Beyond quantifier-free interpolation in extensions of presburger arithmetic
od: Brillout, A, et al.
Izdano: (2011)

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

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

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

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

Algebra and sequent calculus for epistemic actions
od: Baltag, A, et al.
Izdano: (2005)

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

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

A Cut−Free Sequent Calculus for Algebraic Dynamic Epistemic Logic
od: Dyckhoff, R, et al.
Izdano: (2010)

Implementation of a cut−free sequent calculus for logics with adjoint modalities
od: Kriener, M, et al.
Izdano: (2009)

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

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

Grammar Logics in Nested Sequent Calculus: Proof Theory and Decision Procedures
od: Tiu, A, et al.
Izdano: (2012)

A labelled sequent calculus for BBI : proof theory and proof search
od: Hóu, Zhé, et al.
Izdano: (2020)

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

Stoic sequent logic and proof theory
od: Bobzien, S
Izdano: (2019)

The GHZ/W−calculus contains rational arithmetic
od: Coecke, B, et al.
Izdano: (2011)

The GHZ/W−calculus contains rational arithmetic
od: Coecke, B, et al.
Izdano: (2010)

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

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

Preface: Special Issue on Interpolation
od: Kroening, D, et al.
Izdano: (2016)

Interpolant Strength
od: D'Silva, V, et al.
Izdano: (2010)

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

Stochastic And Modified Sequent Peak Algorithm For Reservoir Planning Analysis Considering Performance Indices
od: Oskoui, Issa Saket
Izdano: (2016)

Quantifying the consistency and rheology of liquid foods using fractional calculus
od: Engmann, Jan, et al.
Izdano: (2018)

Restructuring Resolution Refutations for Interpolation
od: D'Silva, V, et al.
Izdano: (2008)

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

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

Multilevel interpolation of divergence-free vector fields
od: Gillow, K, et al.
Izdano: (2016)

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

An interpolating decision procedure for transitive relations with uninterpreted functions
od: Kroening, D, et al.
Izdano: (2009)

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

Approximation Refinement for Interpolation−Based Model Checking
od: D'Silva, V, et al.
Izdano: (2008)

Approximation Refinement for Interpolation−Based Model Checking
od: D'Silva, V, et al.
Izdano: (2008)

Ranking function synthesis for bit-vector relations
od: Cook, B, et al.
Izdano: (2013)

Computing mutation coverage in interpolation-based model checking
od: Chockler, H, et al.
Izdano: (2012)

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

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

Grid-free computation of probabilistic safety with Malliavin calculus
od: Cosentino, F, et al.
Izdano: (2023)