max planck institut
informatik

# 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)
Title: A Quantifier- Elimination Heuristic for Octagonal Constraints Deepak Kapur University of New Mexico 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. SWS Colloquium D1, D2, D3, D4, D5, SWS, RG1, MMCIWe use this to send out email in the morning. Expert Audience English
Date: Friday, 18 September 2015 14:00 -- Not specified -- Kaiserslautern G26 112
 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 0631 93039606 --email address not disclosed on the web
Video Broadcast: To Location: Yes Saarbrücken E1 5 029

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