scientific article; zbMATH DE number 3408928
From MaRDI portal
Publication:5674430
zbMath0258.68046MaRDI QIDQ5674430
Publication date: 1972
Title: zbMATH Open Web Interface contents unavailable due to conflicting licenses.
Lua error in Module:PublicationMSCList at line 37: attempt to index local 'msc_result' (a nil value).
Related Items (55)
Survey on Parameterized Verification with Threshold Automata and the Byzantine Model Checker ⋮ On Composing Finite Forests with Modal Logics ⋮ A layered algorithm for quantifier elimination from linear modular constraints ⋮ The first order theory of primal grammars is decidable ⋮ Reflections on termination of linear loops ⋮ Hyperfinite MV-algebras ⋮ Complexity of Subcases of Presburger Arithmetic ⋮ Linear Integer Arithmetic Revisited ⋮ The complexity of linear problems in fields ⋮ A characterization of pseudofinite MV-algebras ⋮ A Plethora of Polynomials: A Toolbox for Counting Problems ⋮ Automatic synthesis of logical models for order-sorted first-order theories ⋮ Deciding Boolean algebra with Presburger arithmetic ⋮ Short Presburger Arithmetic Is Hard ⋮ Bounding quantification in parametric expansions of Presburger arithmetic ⋮ Subclasses of Presburger arithmetic and the polynomial-time hierarchy ⋮ Parallélisation sémantique ⋮ Separation logics and modalities: a survey ⋮ Solving quantified linear arithmetic by counterexample-guided instantiation ⋮ A decision procedure for string constraints with string/integer conversion and flat regular constraints ⋮ Simulation by Rounds of Letter-to-Letter Transducers ⋮ Decision procedures for term algebras with integer constraints ⋮ Unnamed Item ⋮ Upper Bounds on the Automata Size for Integer and Mixed Real and Integer Linear Arithmetic (Extended Abstract) ⋮ The two variable per inequality abstract domain ⋮ An approach to multicore parallelism using functional programming: a case study based on Presburger arithmetic ⋮ Eliminating message counters in synchronous threshold automata ⋮ Weak quantifier elimination for the full linear theory of the integers ⋮ Proof synthesis and reflection for linear arithmetic ⋮ A typed \(\lambda\)-calculus for proving-by-example and bottom-up generalization procedure ⋮ Parametric Presburger arithmetic: logic, combinatorics, and quasi-polynomial behavior ⋮ SMT-based model checking for recursive programs ⋮ A practical approach to model checking duration calculus using Presburger arithmetic ⋮ Complexity of logical theories involving coprimality ⋮ Model-theoretic methods in combined constraint satisfiability ⋮ Linear quantifier elimination ⋮ A Decidable Class of Nested Iterated Schemata ⋮ Ehrenfeucht-Fraïssé goes automatic for real addition ⋮ The complexity of verifying population protocols ⋮ Cutting to the Chase Solving Linear Integer Arithmetic ⋮ A \(2^{2^{2^{pn}}}\) upper bound on the complexity of Presburger arithmetic ⋮ On solving quantified bit-vector constraints using invertibility conditions ⋮ The complexity of almost linear diophantine problems ⋮ Towards efficient verification of population protocols ⋮ A complete and terminating approach to linear integer solving ⋮ Session Types with Arithmetic Refinements ⋮ Effective Quantifier Elimination for Presburger Arithmetic with Infinity ⋮ A Survey of Satisfiability Modulo Theory ⋮ A Tableaux-Based Decision Procedure for Multi-parameter Propositional Schemata ⋮ Combination of uniform interpolants via Beth definability ⋮ Unnamed Item ⋮ A Pattern Logic for Automata with Outputs ⋮ Symbolic model checking of timed guarded commands using difference decision diagrams ⋮ Taming past LTL and flat counter systems ⋮ Cutting to the chase.
This page was built for publication:
