Campus Event Calendar
Event Entry
New for: D2, D3
What and Who
Termination of Imperative Programs via Term Rewriting
Deepak Kapur
University of New Mexico
MPI-INF Distinguished Speaker Series
AG 1, AG 2, AG 3, AG 4, AG 5, SWS, RG1, MMCI
Public Audience
English
Note: We use this to send email in the morning.
Date, Time and Location
Tuesday, 15 June 2010
16:00
60 Minutes
E1 4
024
Saarbrücken
Abstract
Termination techniques and tools from term rewriting literature
are proposed for showing termination of imperative programs
working on numbers. An imperative program is translated to a
constrained rewrite system in which rewrite rules are applicable
only at the top most level. Constraints are simple number
theoretic relations on program variables, expressible in
quantifier-free Presburger arithmetic. A rewriting sequence is
proved to directly mimic computations of an imperative
program. Termination of such rewrite systems is shown by adapting
the dependency pair method and the associated dependency pair
framework to the constrained equational rewrite system modulo
Presburger arithmetic. The proposed approach has been used to
prove termination of a large class of imperative programs.
are proposed for showing termination of imperative programs
working on numbers. An imperative program is translated to a
constrained rewrite system in which rewrite rules are applicable
only at the top most level. Constraints are simple number
theoretic relations on program variables, expressible in
quantifier-free Presburger arithmetic. A rewriting sequence is
proved to directly mimic computations of an imperative
program. Termination of such rewrite systems is shown by adapting
the dependency pair method and the associated dependency pair
framework to the constrained equational rewrite system modulo
Presburger arithmetic. The proposed approach has been used to
prove termination of a large class of imperative programs.
Contact
Jennifer Müller
900
--email hidden
passcode not visible
logged in users only
Jennifer Müller, 06/07/2010 09:44 -- Created document.