Max-Planck-Institut für Informatik
max planck institut
mpii logo Minerva of the Max Planck Society

MPI-INF or MPI-SWS or Local Campus Event Calendar

<< Previous Entry Next Entry >> New Event Entry Edit this Entry Login to DB (to update, delete)
What and Who
Title:A Quantifier- Elimination Heuristic for Octagonal Constraints
Speaker:Deepak Kapur
coming from:University of New Mexico
Speakers Bio:PhD (1980), Massachusetts Institute of Technology (MIT), Cambridge, MA;
M. Tech. (1973) and B. Tech. (1971), Indian Institute of Technology (IIT), Kanpur, India.

Chair, Department of Computer Science, University of New Mexico, Jan. 1999--June 2006.

Adjunct Professor,
School of Technology and Computer Science, Tata Institute of Fundamental Research, Mumbai, India, 2003 onwards.

Professor, Department of Computer Science, Jan. 1988-- Dec. 1998, University at Albany.
Founder and former Director,
Institute for Programming and Logics, University at Albany.

Member, Research Staff, Computer Science Branch, General Electric Corporate Research and Development, Schenectady, NY, 1980-87.
Event Type:SWS Colloquium
Visibility:D1, D2, D3, D4, D5, SWS, RG1, MMCI
We use this to send out email in the morning.
Level:Expert Audience
Date, Time and Location
Date:Friday, 18 September 2015
Duration:-- Not specified --
Octagonal constraints expressing weakly relational numerical

properties of the form ($l \le \pm x \pm y \leq h$) have been
found useful and effective in static analysis of numerical
programs. Their analysis serves as a key component of the tool
ASTREE based on abstract interpretation framework proposed by
Patrick Cousot and his group, which has been successfully used to
analyze commercial software consisting of hundreds of thousand of
lines of code. This talk will discuss a heuristic based on the
quantifier-elimination (QE) approach presented by Kapur (2005)
that can be used to automatically derive loop invariants
expressed as a conjunction of octagonal constraints in $O(n^2)$,
where $n$ is the number of program variables over which these
constraints are expressed. This is in contrast to the algorithms
developed in Mine's thesis which have the complexity at least
$O(n^3)$. The restricted QE heuristic usually generates
invariants stronger than those obtained by the freely available
Interproc tool. Extensions of the proposed approach to generating disjunctive
invariants will be presented.

Name(s):Roslyn Stricker
Phone:0631 93039606
EMail:--email address not disclosed on the web
Video Broadcast
Video Broadcast:YesTo Location:Saarbr├╝cken
To Building:E1 5To Room:029
Tags, Category, Keywords and additional notes
Attachments, File(s):

Created by:Roslyn Stricker/MPI-SWS, 09/17/2015 09:17 AMLast modified by:Uwe Brahm/MPII/DE, 11/24/2016 04:13 PM
  • Roslyn Stricker, 09/17/2015 09:34 AM -- Created document.