Hello,
In the first TAVer meeting we will discuss the attached paper. I'll host
the discussion.
The meeting will take place in Room 349 on October 30 at 12:00.
Abstract of the paper:
The first-order theory of the integers with addition and order, commonly
known as Presburger arithmetic,
has been a central topic in mathematical logic and computer science for
almost 90 years. Presburger arithmetic
has been the starting point for numerous lines of research in automata
theory, model theory and discrete geometry.
In formal verification, Presburger arithmetic is the first-choice logic
to represent and reason about systems with
infinitely many states. This article provides a broad yet concise
overview over the history, decision procedures,
extensions and geometric properties of Presburger arithmetic.
Best,
Alessio