Presburger Arithmetic with Divisibility
|
Supervisor |
|
|
Suitable for |
Abstract
Decision procedure for the quantifier-free fragment of Presburger
arithmetic play an important role in software verification.
This
project concerns an extension of this theory: Presburger arithmetic
with divisibility. The first goal
of the project is to produce a
clear exposition of a known (but somewhat obscurely presented)
decision procedure
for the quantifier-free fragment of Presburger
arithmetic with divisibility. The second goal is to produce an
implementation of this decision procedure.
This project would suit a mathematically inclined student, although
there are no specific prerequisites.
Reading:
C. Haase, J. Ouaknine, S. Kreutzer and J. Worrell.
Reachability in
Succinct and Parametric One-Counter Automata. Proceedings of
CONCUR'09. LNCS 5710, Springer
2009.
L. Lipshitz. The diophantine problem for addition and
divisibility. Transaction of the American Mathematical
Society,
235:271--283, 1976.