Presburger Arithmetic and its use in verification

Phan Anh Dung

AbstractToday, when every computer has gone multicore, the requirement of taking advantage of these computing powers becomes critical. However, multicore parallelism is complex and error-prone due to extensive use of synchronization techniques. In this thesis, we explore the functional paradigm in the context of F# programming language and parallelism support in .NET framework. This paradigm prefers the declarative way of thinking and no side effect which lead to the ease of parallelizing algorithms. The purpose is to investigate decision algorithms for quantified linear arithmetic of integers (also called Presburger Arithmetic) aiming at efficient parallel implementations. The context of the project is; however, to support model checking for the real-time logic Duration Calculus, and the goal is to decide a subset of Presburger formulas, which is relevant to this model-checking problem and for which efficient tool support can be provided. We present a simplification process for this subset of Presburger formulas which gives some hope for creating small corresponding formulas. Later two parallel decision procedures for Presburger Arithmetic along with their experimental results are discussed.
TypeMaster's thesis [Academic thesis]
Year2011
PublisherTechnical University of Denmark, DTU Informatics, E-mail: reception@imm.dtu.dk
AddressAsmussens Alle, Building 305, DK-2800 Kgs. Lyngby, Denmark
SeriesIMM-M.Sc.-2011-39
NoteSupervised by Associate Professor Michael R. Hansen, mrh@imm.dtu.dk, DTU Informatics
Electronic version(s)[pdf]
Publication linkhttp://www.imm.dtu.dk/English.aspx
BibTeX data [bibtex]
IMM Group(s)Computer Science & Engineering