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 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.