scholarly journals Anatomy of Alternating Quantifier Satisfiability (Work in progress)

10.29007/8cf7 ◽  
2018 ◽  
Author(s):  
Anh-Dung Phan ◽  
Nikolaj Bjørner ◽  
David Monniaux
Keyword(s):  
Quantifier Elimination ◽  
Model Checker ◽  
Duration Calculus ◽  
Presburger Arithmetic ◽  
Work In Progress ◽  
Quantifier Alternation

We report on work in progress to generalize an algorithm recently introduced in [10] for checkingsatisfiability of formulas with quantifier alternation. The algorithm uses two auxiliary procedures:a procedure for producing a candidate formula for quantifier elimination and a procedure for eliminatingor partially eliminating quantifiers. We also apply the algorithm for Presburger Arithmeticformulas and evaluate it on formulas from a model checker for Duration Calculus [8]. We report onexperiments on different variants of the auxiliary procedures. So far, there is an edge to applyingSMT-TEST proposed in [10], while we found that a simpler approach which just eliminates quantifiedvariables per round is almost as good. Both approaches offer drastic improvements to applyingdefault quantifier elimination.

scholarly journals Program Verification via Craig Interpolation for Presburger Arithmetic with Arrays

10.29007/zfkw ◽  
2018 ◽  
Author(s):  
Angelo Brillout ◽  
Daniel Kroening ◽  
Philipp Rümmer ◽  
Thomas Wahl
Keyword(s):  
Model Checking ◽  
Program Verification ◽  
Model Checker ◽  
Craig Interpolation ◽  
Presburger Arithmetic ◽  
C Programs ◽  
Full Theory ◽  
Software Model ◽  
Interpolation Procedure ◽  
Versatile Tool

Craig interpolation has become a versatile tool in formal verification, in particular for generating intermediate assertions in safety analysis and model checking. In this paper, we present a novel interpolation procedure for the theory of arrays, extending an interpolating calculus for the full theory of quantifier-free Presburger arithmetic, which will be presented at IJCAR this year. We investigate the use of this procedure in a software model checker for C programs. A distinguishing feature of the model checker is its ability to faithfully model machine arithmetic with an encoding into Presburger arithmetic with uninterpreted predicates. The interpolation procedure allows the synthesis of quantified invariants about arrays. This paper presents work in progress; we include initial experiments to demonstrate the potential of our method.

scholarly journals Parametric Presburger arithmetic: complexity of counting and quantifier elimination

2019 ◽  
Vol 65 (2) ◽  
pp. 237-250
Author(s):  
Tristram Bogart ◽  
John Goodrick ◽  
Danny Nguyen ◽  
Kevin Woods
Keyword(s):  
Quantifier Elimination ◽  
Arithmetic Complexity ◽  
Presburger Arithmetic

scholarly journals Interpolating bit-vector formulas using uninterpreted predicates and Presburger arithmetic

2021 ◽  
Author(s):  
Peter Backeman ◽  
Philipp Rümmer ◽  
Aleksandar Zeljić
Keyword(s):  
Propositional Logic ◽  
Quantifier Elimination ◽  
New Approach ◽  
Presburger Arithmetic ◽  
Proof Rules ◽  
Proof Search ◽  
Linear Polynomial ◽  
Bit Vector ◽  
Verification Techniques ◽  
Polynomial Constraints

AbstractThe inference of program invariants over machine arithmetic, commonly called bit-vector arithmetic, is an important problem in verification. Techniques that have been successful for unbounded arithmetic, in particular Craig interpolation, have turned out to be difficult to generalise to machine arithmetic: existing bit-vector interpolation approaches are based either on eager translation from bit-vectors to unbounded arithmetic, resulting in complicated constraints that are hard to solve and interpolate, or on bit-blasting to propositional logic, in the process losing all arithmetic structure. We present a new approach to bit-vector interpolation, as well as bit-vector quantifier elimination (QE), that works by lazy translation of bit-vector constraints to unbounded arithmetic. Laziness enables us to fully utilise the information available during proof search (implied by decisions and propagation) in the encoding, and this way produce constraints that can be handled relatively easily by existing interpolation and QE procedures for Presburger arithmetic. The lazy encoding is complemented with a set of native proof rules for bit-vector equations and non-linear (polynomial) constraints, this way minimising the number of cases a solver has to consider. We also incorporate a method for handling concatenations and extractions of bit-vector efficiently.

On decidable extensions of Presburger arithmetic: from A. Bertrand numeration sytems to Pisot numbers

2000 ◽  
Vol 65 (3) ◽  
pp. 1347-1374 ◽  
Author(s):  
Françoise Point
Keyword(s):  
Quantifier Elimination ◽  
Unary Predicate ◽  
Presburger Arithmetic ◽  
Pisot Numbers

AbstractWe study extensions of Presburger arithmetic with a unary predicate R and we show that under certain conditions on R, R is sparse (a notion introduced by A. L. Semënov) and the theory of 〈ℕ, +, R〉 is decidable. We axiomatize this theory and we show that in a reasonable language, it admits quantifier elimination. We obtain similar results for the structure 〈ℚ, +, R〉.

Sign in / Sign up

Export Citation Format

Share Document