Search

Your search keyword '"Presburger arithmetic"' showing total 589 results
Start Over Descriptor "Presburger arithmetic"
589 results on '"Presburger arithmetic"'

2. On the first order theory of plactic monoids.

Author

Turaev, Daniel

Subjects
*MONOIDS, *ARITHMETIC, *ALGORITHMS
Abstract

We prove that a plactic monoid of any finite rank has decidable first order theory. This resolves other open decidability problems about the finite rank plactic monoids, such as the Diophantine problem and identity checking. This is achieved by interpreting a plactic monoid of arbitrary rank in Presburger arithmetic, which is known to have decidable first order theory. We also prove that the interpretation of the plactic monoids into Presburger Arithmetic is in fact a bi-interpretation, hence any two plactic monoids of finite rank are bi-interpretable with one another. The algorithm generating the interpretations is uniform, which answers positively the decidability of the Diophantine problem for the infinite rank plactic monoid. [ABSTRACT FROM AUTHOR]

Published
2024
Full Text
View/download PDF

3. Porous invariants for linear systems.

Author

Lefaucheux, Engel, Ouaknine, Joël, Purser, David, and Worrell, James

Subjects
LINEAR dynamical systems, POLYNOMIAL time algorithms, LINEAR equations, LINEAR systems, INTEGERS
Abstract

We introduce the notion of porous invariants for multipath affine loops over the integers. These are invariants definable in (fragments of) Presburger arithmetic and, as such, lack certain tame geometrical properties, such a convexity and connectedness. Nevertheless, we show that in many cases such invariants can be automatically synthesised, and moreover can be used to settle reachability questions for various non-trivial classes of affine loops and target sets. For the class of Z -linear invariants (those defined as conjunctions of linear equations with integer coefficients), we show that a strongest such invariant can be computed in polynomial time. For the more general class of N -semi-linear invariants (those defined as Boolean combinations of linear inequalities with integer coefficients), such a strongest invariant need not exist. Here we show that for point targets the existence of a separating invariant is undecidable in general. However we show that such separating invariants can be computed either by restricting the number of program variables or by restricting from multipath to single-path loops. Additionally, we consider porous targets, represented as Z -semi-linear sets (those defined as Boolean combinations of equations with integer coefficients). We show that an invariant can be computed providing the target spans the whole space. We present our tool porous, which computes porous invariants. [ABSTRACT FROM AUTHOR]

Published
2024
Full Text
View/download PDF

4. TWO VARIABLE LOGIC WITH ULTIMATELY PERIODIC COUNTING.

Author

BENEDIKT, MICHAEL, KOSTYLEV, EGOR V., and TAN, TONY

Subjects
*ARITHMETIC, *LOGIC, *INTEGERS, *COUNTING
Abstract

We consider the extension of FO2 with quantifiers that state that the number of elements where a formula holds should belong to a given ultimately periodic set. We show that both satisfiability and finite satisfiability of the logic are decidable. We also show that the spectrum of any sentence, i.e., the set of the sizes of its finite models, is definable in Presburger arithmetic. In the process we present several refinements to the "biregular graph method." In this method, decidability issues concerning two-variable logics are reduced to questions about Presburger definability of integer vectors associated with partitioned graphs, where nodes in a partition satisfy certain constraints on their in- and out-degrees. [ABSTRACT FROM AUTHOR]

Published
2024
Full Text
View/download PDF

6. ON PRESBURGER ARITHMETIC EXTENDED WITH NON-UNARY COUNTING QUANTIFIERS.

Author

HABERMEHL, PETER and KUSKE, DIETRICH

Subjects
FIRST-order logic, POLYNOMIAL time algorithms, SATISFACTION, COUNTING, LOGIC, INTEGERS, ARITHMETIC
Abstract

We consider a first-order logic for the integers with addition. This logic extends classical first-order logic by modulo-counting, threshold-counting and exact-counting quantifiers, all applied to tuples of variables (here, residues are given as terms while moduli and thresholds are given explicitly). Our main result shows that satisfaction for this logic is decidable in two-fold exponential space. If only threshold- and exact-counting quantifiers are allowed, we prove an upper bound of alternating two-fold exponential time with linearly many alternations. This latter result almost matches Berman's exact complexity of first-order logic without counting quantifiers. To obtain these results, we first translate threshold- and exact-counting quantifiers into classical first-order logic in polynomial time (which already proves the second result). To handle the remaining modulo-counting quantifiers for tuples, we first reduce them in doubly exponential time to modulo-counting quantifiers for single elements. For these quantifiers, we provide a quantifier elimination procedure similar to Reddy and Loveland's procedure for first-order logic and analyse the growth of coefficients, constants, and moduli appearing in this process. The bounds obtained this way allow to restrict quantification in the original formula to integers of bounded size which then implies the first result mentioned above. Our logic is incomparable with the logic considered by Chistikov et al. in 2022. They allow more general counting operations in quantifiers, but only unary quantifiers. The move from unary to non-unary quantifiers is non-trivial, since, e.g., the non-unary version of the Härtig quantifier results in an undecidable theory. [ABSTRACT FROM AUTHOR]

Published
2023
Full Text
View/download PDF

7. New Bounds for the Flock-of-Birds Problem

Author

Kozachinskiy, Alexander, Goos, Gerhard, Founding Editor, Hartmanis, Juris, Founding Editor, Bertino, Elisa, Editorial Board Member, Gao, Wen, Editorial Board Member, Steffen, Bernhard, Editorial Board Member, Yung, Moti, Editorial Board Member, Kulikov, Alexander S., editor, and Raskhodnikova, Sofya, editor

Published
2022
Full Text
View/download PDF

8. Groups definable in Presburger arithmetic.

Author

Acosta, Juan Pablo

Subjects
*MODULAR arithmetic, *GROUP theory, *MODEL theory, *ARITHMETIC
Abstract

Here we give a complete list of the groups definable in Presburger arithmetic up to a finite index subgroup. [ABSTRACT FROM AUTHOR]

Published
2025
Full Text
View/download PDF

9. Porous Invariants

Author

Lefaucheux, Engel, Ouaknine, Joël, Purser, David, Worrell, James, Goos, Gerhard, Founding Editor, Hartmanis, Juris, Founding Editor, Bertino, Elisa, Editorial Board Member, Gao, Wen, Editorial Board Member, Steffen, Bernhard, Editorial Board Member, Woeginger, Gerhard, Editorial Board Member, Yung, Moti, Editorial Board Member, Silva, Alexandra, editor, and Leino, K. Rustan M., editor

Published
2021
Full Text
View/download PDF

10. Flat Petri Nets (Invited Talk)

Author

Leroux, Jérôme, Goos, Gerhard, Founding Editor, Hartmanis, Juris, Founding Editor, Bertino, Elisa, Editorial Board Member, Gao, Wen, Editorial Board Member, Steffen, Bernhard, Editorial Board Member, Woeginger, Gerhard, Editorial Board Member, Yung, Moti, Editorial Board Member, Buchs, Didier, editor, and Carmona, Josep, editor

Published
2021
Full Text
View/download PDF

11. Discrete Temporal Constraint Satisfaction Problems.

Author

Bodirsky, Manuel, Martin, Barnaby, and Mottet, Antoine

Subjects
ENDOMORPHISMS, GENETIC polymorphisms, INTEGERS, COMPUTATIONAL complexity, ELECTRONIC data processing
Abstract

A discrete temporal constraint satisfaction problem is a constraint satisfaction problem (CSP) over the set of integers whose constraint language consists of relations that are first-order definable over the order of the integers. We prove that every discrete temporal CSP is in P or NP-complete, unless it can be formulated as a finite domain CSP, in which case the computational complexity is not known in general. [ABSTRACT FROM AUTHOR]

Published
2018
Full Text
View/download PDF

12. Seventy Years of Computer Science

Author

Davis, Martin, Goos, Gerhard, Founding Editor, Hartmanis, Juris, Founding Editor, Bertino, Elisa, Editorial Board Member, Gao, Wen, Editorial Board Member, Steffen, Bernhard, Editorial Board Member, Woeginger, Gerhard, Editorial Board Member, Yung, Moti, Editorial Board Member, Blass, Andreas, editor, Cégielski, Patrick, editor, Dershowitz, Nachum, editor, Droste, Manfred, editor, and Finkbeiner, Bernd, editor

Published
2020
Full Text
View/download PDF

13. Approaching Arithmetic Theories with Finite-State Automata

Author

Haase, Christoph, Goos, Gerhard, Founding Editor, Hartmanis, Juris, Founding Editor, Bertino, Elisa, Editorial Board Member, Gao, Wen, Editorial Board Member, Steffen, Bernhard, Editorial Board Member, Woeginger, Gerhard, Editorial Board Member, Yung, Moti, Editorial Board Member, Leporati, Alberto, editor, Martín-Vide, Carlos, editor, Shapira, Dana, editor, and Zandron, Claudio, editor

Published
2020
Full Text
View/download PDF

14. Representation of Peano Arithmetic in Separation Logic

Author

Sohei Ito and Makoto Tatsuta, Ito, Sohei, Tatsuta, Makoto, Sohei Ito and Makoto Tatsuta, Ito, Sohei, and Tatsuta, Makoto

Abstract

Separation logic is successful for software verification of heap-manipulating programs. Numbers are necessary to be added to separation logic for verification of practical software where numbers are important. However, properties of the validity such as decidability and complexity for separation logic with numbers have not been fully studied yet. This paper presents the translation of Pi-0-1 formulas in Peano arithmetic to formulas in a small fragment of separation logic with numbers, which consists only of the intuitionistic points-to predicate, 0 and the successor function. Then this paper proves that a formula in Peano arithmetic is valid in the standard model if and only if its translation in this fragment is valid in the standard interpretation. As a corollary, this paper also gives a perspective proof for the undecidability of the validity in this fragment. Since Pi-0-1 formulas can describe consistency of logical systems and non-termination of computations, this result also shows that these properties discussed in Peano arithmetic can also be discussed in such a small fragment of separation logic with numbers.

Published
2024
Full Text
View/download PDF

15. Extensions of Presburger arithmetic and model checking one-counter automata

Author

Lechner, Antonia and Worrell, James

Subjects
006.3, Automata Theory, Linear Arithmetic, Computational Complexity Theory, reachability problems, Presburger arithmetic, p-adic numbers, one-counter automata
Abstract

This thesis concerns decision procedures for fragments of linear arithmetic and their application to model-checking one-counter automata. The first part of this thesis covers the complexity of decision problems for different types of linear arithmetic, namely the existential subset of the first-order linear theory over the p-adic numbers and the existential subset of Presburger arithmetic with divisibility, with all integer constants and coefficients represented in binary. The most important result of this part is a new upper complexity bound of NEXPTIME for existential Presburger arithmetic with divisibility. The best bound that was known previously was 2NEXPTIME, which followed directly from the original proof of decidability of this theory by Lipshitz in 1976. Lipshitz also gave a proof of NP-hardness of the problem in 1981. Our result is the first improvement of the bound since this original description of a decision procedure. Another new result, which is both an important building block in establishing our new upper complexity bound for existential Presburger arithmetic with divisibility and an interesting result in its own right, is that the decision problem for the existential linear theory of the p-adic numbers is in the Counting Hierarchy CH, and thus within PSPACE. The precise complexity of this problem was stated as open by Weispfenning in 1988, who showed that it is in EXPTIME and NP-hard. The second part of this thesis covers two problems concerning one-counter automata. The first problem is an LTL synthesis problem on one-counter automata with integer-valued and parameterised updates and with equality tests. The decidability of this problem was stated as open by Göller et al. in 2010. We give a reduction of this problem to the decision problem of a subset of Presburger arithmetic with divisibility with one quantifier alternation and a restriction on existentially quantified variables. A proof of decidability of this theory is currently under review. The final result of this thesis concerns a type of one-counter automata that differs from the previous one in that it allows parameters only on tests, not actions, and it includes both equality and disequality tests on counter values. The decidability of the basic reachability problem on such one-counter automata was stated as an open problem by Demri and Sangnier in 2010. We show that this problem is decidable by a reduction to the decision problem for Presburger arithmetic.

Published
2016

16. Logic and Rational Languages of Scattered and Countable Series-Parallel Posets

Author

Amrane, Amazigh, Bedon, Nicolas, Hutchison, David, Series Editor, Kanade, Takeo, Series Editor, Kittler, Josef, Series Editor, Kleinberg, Jon M., Series Editor, Mattern, Friedemann, Series Editor, Mitchell, John C., Series Editor, Naor, Moni, Series Editor, Pandu Rangan, C., Series Editor, Steffen, Bernhard, Series Editor, Terzopoulos, Demetri, Series Editor, Tygar, Doug, Series Editor, Martín-Vide, Carlos, editor, Okhotin, Alexander, editor, and Shapira, Dana, editor

Published
2019
Full Text
View/download PDF

18. Interpretations of Presburger Arithmetic in Itself

Author

Zapryagaev, Alexander, Pakhomov, Fedor, Hutchison, David, Series editor, Kanade, Takeo, Series editor, Kittler, Josef, Series editor, Kleinberg, Jon M., Series editor, Mattern, Friedemann, Series editor, Mitchell, John C., Series editor, Naor, Moni, Series editor, Pandu Rangan, C., Series editor, Steffen, Bernhard, Series editor, Terzopoulos, Demetri, Series editor, Tygar, Doug, Series editor, Weikum, Gerhard, Series editor, Artemov, Sergei, editor, and Nerode, Anil, editor

Published
2018
Full Text
View/download PDF

19. Interpolating bit-vector formulas using uninterpreted predicates and Presburger arithmetic.

Author

Backeman, Peter, Rümmer, Philipp, and Zeljić, Aleksandar

Subjects
PROPOSITION (Logic), NONLINEAR equations, LAZINESS, INTERPOLATION, TRANSLATING & interpreting
Abstract

The 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. [ABSTRACT FROM AUTHOR]

Published
2021
Full Text
View/download PDF

20. Decidable Weighted Expressions with Presburger Combinators

Author

Filiot, Emmanuel, Mazzocchi, Nicolas, Raskin, Jean-François, Hutchison, David, Series editor, Kanade, Takeo, Series editor, Kittler, Josef, Series editor, Kleinberg, Jon M., Series editor, Mattern, Friedemann, Series editor, Mitchell, John C., Series editor, Naor, Moni, Series editor, Pandu Rangan, C., Series editor, Steffen, Bernhard, Series editor, Terzopoulos, Demetri, Series editor, Tygar, Doug, Series editor, Weikum, Gerhard, Series editor, Klasing, Ralf, editor, and Zeitoun, Marc, editor

Published
2017
Full Text
View/download PDF

21. Quantified Formulas

Author

Kroening, Daniel, Strichman, Ofer, Henzinger, Monika, Series editor, Hromkovič, Juraj, Series editor, Nielsen, Mogens, Series editor, Rozenberg, Grzegorz, Series editor, Salomaa, Arto, Series editor, Kroening, Daniel, and Strichman, Ofer

Published
2016
Full Text
View/download PDF

22. Circuit Satisfiability and Constraint Satisfaction Around Skolem Arithmetic

Author

Glaßer, Christian, Jonsson, Peter, Martin, Barnaby, Hutchison, David, Series editor, Kanade, Takeo, Series editor, Kittler, Josef, Series editor, Kleinberg, Jon M., Series editor, Mattern, Friedemann, Series editor, Mitchell, John C., Series editor, Naor, Moni, Series editor, Pandu Rangan, C., Series editor, Steffen, Bernhard, Series editor, Terzopoulos, Demetri, Series editor, Tygar, Doug, Series editor, Weikum, Gerhard, Series editor, Beckmann, Arnold, editor, Bienvenu, Laurent, editor, and Jonoska, Nataša, editor

Published
2016
Full Text
View/download PDF

23. Decision Procedure for Separation Logic with Inductive Definitions and Presburger Arithmetic

Author

Tatsuta, Makoto, Le, Quang Loc, Chin, Wei-Ngan, Hutchison, David, Series editor, Kanade, Takeo, Series editor, Kittler, Josef, Series editor, Kleinberg, Jon M., Series editor, Mattern, Friedemann, Series editor, Mitchell, John C., Series editor, Naor, Moni, Series editor, Pandu Rangan, C., Series editor, Steffen, Bernhard, Series editor, Terzopoulos, Demetri, Series editor, Tygar, Doug, Series editor, Weikum, Gerhard, Series editor, and Igarashi, Atsushi, editor

Published
2016
Full Text
View/download PDF

24. Petri Nets and Semilinear Sets (Extended Abstract)

Author

Yen, Hsu-Chun, Hutchison, David, Series editor, Kanade, Takeo, Series editor, Kittler, Josef, Series editor, Kleinberg, Jon M., Series editor, Mattern, Friedemann, Series editor, Mitchell, John C., Series editor, Naor, Moni, Series editor, Pandu Rangan, C., Series editor, Steffen, Bernhard, Series editor, Terzopoulos, Demetri, Series editor, Tygar, Doug, Series editor, Weikum, Gerhard, Series editor, Sampaio, Augusto, editor, and Wang, Farn, editor

Published
2016
Full Text
View/download PDF

26. Logic and rational languages of scattered and countable series-parallel posets.

Author

Amrane, Amazigh and Bedon, Nicolas

Subjects
*PARTIALLY ordered sets, *LINEAR orderings, *LOGIC, *ARITHMETIC mean, *ARITHMETIC functions
Abstract

Let A be an alphabet and S P ⋄ (A) denote the class of all countable N-free partially ordered sets labeled by A , in which chains are scattered linear orderings and antichains are finite. We characterize the rational languages of S P ⋄ (A) by means of logic. We define an extension of monadic second-order logic by Presburger arithmetic, named P-MSO, such that a language L of S P ⋄ (A) is rational if and only if L is the language of a sentence of P-MSO, with effective constructions from one formalism to the other. As a corollary, the P-MSO theory of S P ⋄ (A) is decidable. [ABSTRACT FROM AUTHOR]

Published
2020
Full Text
View/download PDF

27. Decidable weighted expressions with Presburger combinators.

Author

Filiot, Emmanuel, Mazzocchi, Nicolas, and Raskin, Jean-François

Abstract

In this paper, we investigate the expressive power and the algorithmic properties of weighted expressions, which define functions from finite words to integers. First, we consider a slight extension of an expression formalism, introduced by Chatterjee et al. in the context of infinite words, in order to combine values given by unambiguous sum -automata, using Presburger arithmetic. We show that important decision problems such as emptiness, universality, inclusion and equivalence are PSpace-C for these expressions. We then investigate the extension of these expressions with Kleene star. This allows to iterate an expression over smaller fragments of the input word, and to combine the results by taking their iterated sum. The decision problems turn out to be undecidable, but we introduce a decidable and still expressive class of synchronised expressions. [ABSTRACT FROM AUTHOR]

Published
2019
Full Text
View/download PDF

28. Target counting with Presburger constraints and its application in sensor networks.

Author

Linker, Sven and Sevegnani, Michele

Subjects
*SENSOR networks, *WIRELESS sensor networks
Abstract

One of the applications popularized by the emergence of wireless sensor networks is target counting: the computational task of determining the total number of targets located in an area by aggregating the individual counts of each sensor. The complexity of this task lies in the fact that sensing ranges may overlap, and therefore, targets may be overcounted as, in this setting, they are assumed to be indistinguishable from each other. In the literature, this problem has been proven to be unsolvable, hence the existence of several estimation algorithms. However, the main limitation currently affecting these algorithms is that no assurance regarding the precision of a solution can be given. We present a novel algorithm for target counting based on exhaustive enumeration of target distributions using linear Presburger constraints. We improve on current approaches since the estimated counts obtained by our algorithm are by construction guaranteed to be consistent with the counts of each sensor. We further extend our algorithm to allow for weighted topologies and sensing errors for applicability in real-world deployments. We evaluate our approach through an extensive collection of synthetic and real-life configurations. [ABSTRACT FROM AUTHOR]

Published
2019
Full Text
View/download PDF

29. A NEW DP-MINIMAL EXPANSION OF THE INTEGERS.

Author

ALOUF, ERAN and D'ELBÉE, CHRISTIAN

Subjects
INTEGERS, ABELIAN groups, NATURAL languages
Abstract

We consider the structure $({\Bbb Z}, + ,0,|_{p_1 } , \ldots ,|_{p_n })$ , where $x|_p y$ means $v_p \left(x \right) \leqslant v_p \left(y \right)$ and v p is the p -adic valuation. We prove that this structure has quantifier elimination in a natural expansion of the language of abelian groups, and that it has dp-rank n. In addition, we prove that a first order structure with universe ${\Bbb Z}$ which is an expansion of $({\Bbb Z}, + ,0)$ and a reduct of $({\Bbb Z}, + ,0,|_p)$ must be interdefinable with one of them. We also give an alternative proof for Conant's analogous result about $({\Bbb Z}, + ,0,. [ABSTRACT FROM AUTHOR]

Published
2019
Full Text
View/download PDF

30. LENGTH OF LOCAL COHOMOLOGY OF POWERS OF IDEALS.

Author

HAILONG DAO and MONTAÑO, JONATHAN

Subjects
*COHOMOLOGY theory, *POLYNOMIAL rings, *COMMUTATIVE algebra, *MATHEMATICAL singularities, *COMBINATORICS
Abstract

Let R be a polynomial ring over a field k with irrelevant ideal m and dimension d. Let I be a homogeneous ideal in R. We study the asymptotic behavior of the length of the modules Hmi(R/In) for n >> 0. We show that for a fixed number α ∈ ℤ, lim supn→∞ λ(Hmi(R/In)≥−αn) / nd < ∞. It follows that lim supn→∞ λ(Hmi(R/In)) / nd < ∞ when X = Proj R/I is locally a complete intersection (lci) and i ≤ dimX. We also establish that the actual limit exists and is rational for certain classes of monomial ideals I such that the lengths of local cohomology of In are eventually finite. Our proofs use Gr¨obner deformation and Presburger arithmetic. Finally, we utilize more traditional commutative algebra techniques to show that lim infn→∞ λ(Hmi(R/In) / nd > 0 under certain conditions when R/I is either F-pure or lci. [ABSTRACT FROM AUTHOR]

Published
2019
Full Text
View/download PDF

31. The Context-Freeness Problem Is coNP-Complete for Flat Counter Systems

Author

Leroux, Jérôme, Penelle, Vincent, Sutre, Grégoire, Hutchison, David, Series editor, Kanade, Takeo, Series editor, Kittler, Josef, Series editor, Kleinberg, Jon M., Series editor, Kobsa, Alfred, Series editor, Mattern, Friedemann, Series editor, Mitchell, John C., Series editor, Naor, Moni, Series editor, Nierstrasz, Oscar, Series editor, Pandu Rangan, C., Series editor, Steffen, Bernhard, Series editor, Terzopoulos, Demetri, Series editor, Tygar, Doug, Series editor, Weikum, Gerhard, Series editor, Cassez, Franck, editor, and Raskin, Jean-François, editor

Published
2014
Full Text
View/download PDF

32. Integer Vector Addition Systems with States

Author

Haase, Christoph, Halfon, Simon, Hutchison, David, Series editor, Kanade, Takeo, Series editor, Kittler, Josef, Series editor, Kleinberg, Jon M., Series editor, Kobsa, Alfred, Series editor, Mattern, Friedemann, Series editor, Mitchell, John C., Series editor, Naor, Moni, Series editor, Nierstrasz, Oscar, Series editor, Pandu Rangan, C., Series editor, Steffen, Bernhard, Series editor, Terzopoulos, Demetri, Series editor, Tygar, Doug, Series editor, Weikum, Gerhard, Series editor, Ouaknine, Joël, editor, Potapov, Igor, editor, and Worrell, James, editor

Published
2014
Full Text
View/download PDF

33. Monadic Decomposition

Author

Veanes, Margus, Bjørner, Nikolaj, Nachmanson, Lev, Bereg, Sergey, Hutchison, David, editor, Kanade, Takeo, editor, Kittler, Josef, editor, Kleinberg, Jon M., editor, Kobsa, Alfred, editor, Mattern, Friedemann, editor, Mitchell, John C., editor, Naor, Moni, editor, Nierstrasz, Oscar, editor, Pandu Rangan, C., editor, Steffen, Bernhard, editor, Terzopoulos, Demetri, editor, Tygar, Doug, editor, Weikum, Gerhard, editor, Biere, Armin, editor, and Bloem, Roderick, editor

Published
2014
Full Text
View/download PDF

34. Presburger Arithmetic in Memory Access Optimization for Data-Parallel Languages

Author

Karrenberg, Ralf, Košta, Marek, Sturm, Thomas, Hutchison, David, editor, Kanade, Takeo, editor, Kittler, Josef, editor, Kleinberg, Jon M., editor, Mattern, Friedemann, editor, Mitchell, John C., editor, Naor, Moni, editor, Nierstrasz, Oscar, editor, Pandu Rangan, C., editor, Steffen, Bernhard, editor, Sudan, Madhu, editor, Terzopoulos, Demetri, editor, Tygar, Doug, editor, Vardi, Moshe Y., editor, Weikum, Gerhard, editor, Goebel, Randy, editor, Siekmann, Jörg, editor, Wahlster, Wolfgang, editor, Fontaine, Pascal, editor, Ringeissen, Christophe, editor, and Schmidt, Renate A., editor

Published
2013
Full Text
View/download PDF

35. Which Finitely Ambiguous Automata Recognize Finitely Sequential Functions? : (Extended Abstract)

Author

Bala, Sebastian, Hutchison, David, editor, Kanade, Takeo, editor, Kittler, Josef, editor, Kleinberg, Jon M., editor, Mattern, Friedemann, editor, Mitchell, John C., editor, Naor, Moni, editor, Nierstrasz, Oscar, editor, Pandu Rangan, C., editor, Steffen, Bernhard, editor, Sudan, Madhu, editor, Terzopoulos, Demetri, editor, Tygar, Doug, editor, Vardi, Moshe Y., editor, Weikum, Gerhard, editor, Chatterjee, Krishnendu, editor, and Sgall, Jirí, editor

Published
2013
Full Text
View/download PDF

36. Non-deterministic Population Protocols

Author

Beauquier, Joffroy, Burman, Janna, Rosaz, Laurent, Rozoy, Brigitte, Hutchison, David, editor, Kanade, Takeo, editor, Kittler, Josef, editor, Kleinberg, Jon M., editor, Mattern, Friedemann, editor, Mitchell, John C., editor, Naor, Moni, editor, Nierstrasz, Oscar, editor, Pandu Rangan, C., editor, Steffen, Bernhard, editor, Sudan, Madhu, editor, Terzopoulos, Demetri, editor, Tygar, Doug, editor, Vardi, Moshe Y., editor, Weikum, Gerhard, editor, Baldoni, Roberto, editor, Flocchini, Paola, editor, and Binoy, Ravindran, editor

Published
2012
Full Text
View/download PDF

37. A Verification Toolkit for Numerical Transition Systems : Tool Paper

Author

Hojjat, Hossein, Konečný, Filip, Garnier, Florent, Iosif, Radu, Kuncak, Viktor, Rümmer, Philipp, Hutchison, David, editor, Kanade, Takeo, editor, Kittler, Josef, editor, Kleinberg, Jon M., editor, Mattern, Friedemann, editor, Mitchell, John C., editor, Naor, Moni, editor, Nierstrasz, Oscar, editor, Pandu Rangan, C., editor, Steffen, Bernhard, editor, Sudan, Madhu, editor, Terzopoulos, Demetri, editor, Tygar, Doug, editor, Vardi, Moshe Y., editor, Weikum, Gerhard, editor, Giannakopoulou, Dimitra, editor, and Méry, Dominique, editor

Published
2012
Full Text
View/download PDF

38. Lynx: A Programmatic SAT Solver for the RNA-Folding Problem

Author

Ganesh, Vijay, O’Donnell, Charles W., Soos, Mate, Devadas, Srinivas, Rinard, Martin C., Solar-Lezama, Armando, Hutchison, David, editor, Kanade, Takeo, editor, Kittler, Josef, editor, Kleinberg, Jon M., editor, Mattern, Friedemann, editor, Mitchell, John C., editor, Naor, Moni, editor, Nierstrasz, Oscar, editor, Pandu Rangan, C., editor, Steffen, Bernhard, editor, Sudan, Madhu, editor, Terzopoulos, Demetri, editor, Tygar, Doug, editor, Vardi, Moshe Y., editor, Weikum, Gerhard, editor, Cimatti, Alessandro, editor, and Sebastiani, Roberto, editor

Published
2012
Full Text
View/download PDF

39. Automatically Proving Thousands of Verification Conditions Using an SMT Solver: An Empirical Study

Author

Tagore, Aditi, Zaccai, Diego, Weide, Bruce W., Hutchison, David, editor, Kanade, Takeo, editor, Kittler, Josef, editor, Kleinberg, Jon M., editor, Mattern, Friedemann, editor, Mitchell, John C., editor, Naor, Moni, editor, Nierstrasz, Oscar, editor, Pandu Rangan, C., editor, Steffen, Bernhard, editor, Sudan, Madhu, editor, Terzopoulos, Demetri, editor, Tygar, Doug, editor, Vardi, Moshe Y., editor, Weikum, Gerhard, editor, Goodloe, Alwyn E., editor, and Person, Suzette, editor

Published
2012
Full Text
View/download PDF

40. Decision Procedures for Region Logic

Author

Rosenberg, Stan, Banerjee, Anindya, Naumann, David A., Hutchison, David, Series editor, Kanade, Takeo, Series editor, Kittler, Josef, Series editor, Kleinberg, Jon M., Series editor, Mattern, Friedemann, Series editor, Mitchell, John C., Series editor, Naor, Moni, Series editor, Nierstrasz, Oscar, Series editor, Pandu Rangan, C., Series editor, Steffen, Bernhard, Series editor, Sudan, Madhu, Series editor, Terzopoulos, Demetri, Series editor, Tygar, Doug, Series editor, Vardi, Moshe Y., Series editor, Weikum, Gerhard, Series editor, Kuncak, Viktor, editor, and Rybalchenko, Andrey, editor

Published
2012
Full Text
View/download PDF

41. Verifying Two Lines of C with Why3: An Exercise in Program Verification

Author

Filliâtre, Jean-Christophe, Hutchison, David, Series editor, Kanade, Takeo, Series editor, Kittler, Josef, Series editor, Kleinberg, Jon M., Series editor, Mattern, Friedemann, Series editor, Mitchell, John C., Series editor, Naor, Moni, Series editor, Nierstrasz, Oscar, Series editor, Pandu Rangan, C., Series editor, Steffen, Bernhard, Series editor, Sudan, Madhu, Series editor, Terzopoulos, Demetri, Series editor, Tygar, Doug, Series editor, Vardi, Moshe Y., Series editor, Weikum, Gerhard, Series editor, Joshi, Rajeev, editor, Müller, Peter, editor, and Podelski, Andreas, editor

Published
2012
Full Text
View/download PDF

42. Scala to the Power of Z3: Integrating SMT and Programming

Author

Köksal, Ali Sinan, Kuncak, Viktor, Suter, Philippe, Hutchison, David, Series editor, Kanade, Takeo, Series editor, Kittler, Josef, Series editor, Kleinberg, Jon M., Series editor, Mattern, Friedemann, Series editor, Mitchell, John C., Series editor, Naor, Moni, Series editor, Nierstrasz, Oscar, Series editor, Pandu Rangan, C., Series editor, Steffen, Bernhard, Series editor, Sudan, Madhu, Series editor, Terzopoulos, Demetri, Series editor, Tygar, Doug, Series editor, Vardi, Moshe Y., Series editor, Weikum, Gerhard, Series editor, Goebel, Randy, editor, Siekmann, Jörg, editor, Wahlster, Wolfgang, editor, Bjørner, Nikolaj, editor, and Sofronie-Stokkermans, Viorica, editor

Published
2011
Full Text
View/download PDF

43. Forward Analysis and Model Checking for Trace Bounded WSTS

Author

Chambart, Pierre, Finkel, Alain, Schmitz, Sylvain, Hutchison, David, Series editor, Kanade, Takeo, Series editor, Kittler, Josef, Series editor, Kleinberg, Jon M., Series editor, Mattern, Friedemann, Series editor, Mitchell, John C., Series editor, Naor, Moni, Series editor, Nierstrasz, Oscar, Series editor, Pandu Rangan, C., Series editor, Steffen, Bernhard, Series editor, Sudan, Madhu, Series editor, Terzopoulos, Demetri, Series editor, Tygar, Doug, Series editor, Vardi, Moshe Y., Series editor, Weikum, Gerhard, Series editor, Kristensen, Lars M., editor, and Petrucci, Laure, editor

Published
2011
Full Text
View/download PDF

44. Infinite Families of Finite String Rewriting Systems and Their Confluence

Author

Jouannaud, Jean-Pierre, Monate, Benjamin, Hutchison, David, Series editor, Kanade, Takeo, Series editor, Kittler, Josef, Series editor, Kleinberg, Jon M., Series editor, Mattern, Friedemann, Series editor, Mitchell, John C., Series editor, Naor, Moni, Series editor, Nierstrasz, Oscar, Series editor, Pandu Rangan, C., Series editor, Steffen, Bernhard, Series editor, Sudan, Madhu, Series editor, Terzopoulos, Demetri, Series editor, Tygar, Doug, Series editor, Vardi, Moshe Y., Series editor, Weikum, Gerhard, Series editor, Fermüller, Christian G., editor, and Voronkov, Andrei, editor

Published
2010
Full Text
View/download PDF

45. Ranking Function Synthesis for Bit-Vector Relations

Author

Cook, Byron, Kroening, Daniel, Rümmer, Philipp, Wintersteiger, Christoph M., Hutchison, David, editor, Kanade, Takeo, editor, Kittler, Josef, editor, Kleinberg, Jon M., editor, Mattern, Friedemann, editor, Mitchell, John C., editor, Naor, Moni, editor, Nierstrasz, Oscar, editor, Pandu Rangan, C., editor, Steffen, Bernhard, editor, Sudan, Madhu, editor, Terzopoulos, Demetri, editor, Tygar, Doug, editor, Vardi, Moshe Y., editor, Weikum, Gerhard, editor, Esparza, Javier, editor, and Majumdar, Rupak, editor

Published
2010
Full Text
View/download PDF

46. On Gossip and Populations

Author

Bertier, Marin, Busnel, Yann, Kermarrec, Anne-Marie, Hutchison, David, Series editor, Kanade, Takeo, Series editor, Kittler, Josef, Series editor, Kleinberg, Jon M., Series editor, Mattern, Friedemann, Series editor, Mitchell, John C., Series editor, Naor, Moni, Series editor, Nierstrasz, Oscar, Series editor, Pandu Rangan, C., Series editor, Steffen, Bernhard, Series editor, Sudan, Madhu, Series editor, Terzopoulos, Demetri, Series editor, Tygar, Doug, Series editor, Vardi, Moshe Y., Series editor, Weikum, Gerhard, Series editor, Kutten, Shay, editor, and Žerovnik, Janez, editor

Published
2010
Full Text
View/download PDF

47. Decidable models of integer-manipulating programs with recursive parallelism.

Author

Hague, Matthew and Lin, Anthony W.

Subjects
*INTEGERS, *RECURSIVE functions, *MATHEMATICAL variables, *CONTROL theory (Engineering), *MATHEMATICAL invariants
Abstract

Abstract We study safety verification for multithreaded programs with recursive parallelism (i.e. unbounded thread creation and recursion) as well as unbounded integer variables. Since the threads in each program configuration are structured in a hierarchical fashion, our model is state-extended ground-tree rewrite systems equipped with shared unbounded integer counters that can be incremented, decremented, and compared against an integer constant. Since the model is Turing-complete, we propose a decidable underapproximation. First, using a restriction similar to context-bounding, we underapproximate the global control by a weak global control (i.e. DAGs possibly with self-loops), thereby limiting the number of synchronisations between different threads. Second, we bound the number of reversals between non-decrementing and non-incrementing modes of the counters. Under this restriction, we show that reachability becomes NP-complete. In fact, it is poly-time reducible to satisfaction over existential Presburger formulas, which allows one to tap into highly optimised SMT solvers. Our decidable approximation strictly generalises known decidable models including (i) weakly-synchronised ground-tree rewrite systems, and (ii) synchronisation/reversal-bounded concurrent pushdown systems with counters. Finally, we show that, when equipped with reversal-bounded counters, relaxing the weak control restriction by the notion of senescence results in undecidability. [ABSTRACT FROM AUTHOR]

Published
2018
Full Text
View/download PDF

48. Bounding quantification in parametric expansions of Presburger arithmetic.

Author

Goodrick, John

Subjects
*MATHEMATICAL bounds, *ARITHMETIC, *ELIMINATION (Mathematics), *POLYNOMIALS, *MULTIPLICATION
Abstract

Generalizing Cooper’s method of quantifier elimination for Presburger arithmetic, we give a new proof that all parametric Presburger families {St:t∈N} [as defined by Woods (Electron J Comb 21:P21, 2014)] are definable by formulas with polynomially bounded quantifiers in an expanded language with predicates for divisibility by f(t) for every polynomial f∈Z[t]. In fact, this quantifier bounding method works more generally in expansions of Presburger arithmetic by multiplication by scalars {α(t):α∈R,t∈X} where R is any ring of functions from X into Z. [ABSTRACT FROM AUTHOR]

Published
2018
Full Text
View/download PDF

49. Equivalence between model-checking flat counter systems and Presburger arithmetic.

Author

Demri, Stéphane, Dhar, Amit Kumar, and Sangnier, Arnaud

Subjects
*COUNTERS (Computer science), *DIGITAL counters, *CONSTRAINT satisfaction, *ARITHMETIC, *INFORMATION technology
Abstract

We show that model-checking flat counter systems with the branching-time temporal logic CTL* extended with arithmetical constraints on counter values has the same worst-case complexity as the satisfiability problem for Presburger arithmetic. The lower bound already holds with strong restrictions: the logical language uses only the temporal operator EF and no arithmetical constraints, and the guards on the transitions are made of linear constraints. This work complements our understanding of model-checking flat counter systems with linear-time temporal logics, such as LTL, for which the problem is already known to be (only) NP-complete with guards restricted to the linear fragment. [ABSTRACT FROM AUTHOR]

Published
2018
Full Text
View/download PDF

Catalog

Books, media, physical & digital resources
See catalog results