scientific article; zbMATH DE number 3408928

Cited in

(67)

The complexity of linear problems in fields
Subclasses of Presburger arithmetic and the polynomial-time hierarchy
Complexity of logical theories involving coprimality
A \(2^{2^{2^{pn}}}\) upper bound on the complexity of Presburger arithmetic
Automatic synthesis of logical models for order-sorted first-order theories
Bounding quantification in parametric expansions of Presburger arithmetic
Solving quantified linear arithmetic by counterexample-guided instantiation
Symbolic model checking of timed guarded commands using difference decision diagrams
The first order theory of primal grammars is decidable
The complexity of verifying population protocols
On solving quantified bit-vector constraints using invertibility conditions
Combination of uniform interpolants via Beth definability
A characterization of pseudofinite MV-algebras
Eliminating message counters in synchronous threshold automata
A practical approach to model checking duration calculus using Presburger arithmetic
A complete and terminating approach to linear integer solving
Taming past LTL and flat counter systems
Cutting to the chase.
A layered algorithm for quantifier elimination from linear modular constraints
Hyperfinite MV-algebras
Decision procedures for term algebras with integer constraints
A survey of satisfiability modulo theory
Complexity of Subcases of Presburger Arithmetic
Linear integer arithmetic revisited
Parallélisation sémantique
Upper Bounds on the Automata Size for Integer and Mixed Real and Integer Linear Arithmetic (Extended Abstract)
Effective Quantifier Elimination for Presburger Arithmetic with Infinity
Separation logics and modalities: a survey
Parametric Presburger arithmetic: logic, combinatorics, and quasi-polynomial behavior
An approach to multicore parallelism using functional programming: a case study based on Presburger arithmetic
Rast: a language for resource-aware session types
A plethora of polynomials: a toolbox for counting problems
Short Presburger Arithmetic Is Hard
Session Types with Arithmetic Refinements
Presburger arithmetic with algebraic scalar multiplications
SMT-based model checking for recursive programs
Cutting to the chase. Solving linear integer arithmetic
A tableaux-based decision procedure for multi-parameter propositional schemata
Model-theoretic methods in combined constraint satisfiability
A decidable class of nested iterated schemata
A pattern logic for automata with outputs
Survey on Parameterized Verification with Threshold Automata and the Byzantine Model Checker
On Composing Finite Forests with Modal Logics
A decision procedure for string constraints with string/integer conversion and flat regular constraints
Simulation by Rounds of Letter-to-Letter Transducers
Symbolic Model Construction for Saturated Constrained Horn Clauses
Boolean abstractions for realizability modulo theories
Realizability modulo theories
The two variable per inequality abstract domain
A typed -calculus for proving-by-example and bottom-up generalization procedure
Rast: resource-aware session types with arithmetic refinements (system description)
Infinite state model checking by learning transitive relations
An efficient quantifier elimination procedure for Presburger arithmetic
Integer linear-exponential programming in NP by quantifier elimination
Quantifier elimination and Craig interpolation: the quantitative way
Synchronized CTL over one-counter automata
VIRAS: conflict-driven quantifier elimination for integer-real arithmetic
Linear quantifier elimination
Ehrenfeucht-Fraïssé goes automatic for real addition
An introduction to the theory of linear integer arithmetic (invited paper)
One-parametric Presburger arithmetic has quantifier elimination
Quantifier Elimination for Linear Arithmetic
The complexity of almost linear diophantine problems
Reflections on termination of linear loops
Deciding Boolean algebra with Presburger arithmetic
Weak quantifier elimination for the full linear theory of the integers
Proof synthesis and reflection for linear arithmetic

This page was built for publication:

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5674430)