ÿþ<html xmlns:v="urn:schemas-microsoft-com:vml" xmlns:o="urn:schemas-microsoft-com:office:office" xmlns:w="urn:schemas-microsoft-com:office:word" xmlns:m="http://schemas.microsoft.com/office/2004/12/omml" xmlns="http://www.w3.org/TR/REC-html40"> <head> <meta http-equiv=Content-Type content="text/html; charset=unicode"> <meta name=ProgId content=Word.Document> <meta name=Generator content="Microsoft Word 15"> <meta name=Originator content="Microsoft Word 15"> <link rel=File-List href="pubs_files/filelist.xml"> <link rel=Edit-Time-Data href="pubs_files/editdata.mso"> <!--[if !mso]> <style> v\:* {behavior:url(#default#VML);} o\:* {behavior:url(#default#VML);} w\:* {behavior:url(#default#VML);} .shape {behavior:url(#default#VML);} </style> <![endif]--><!--[if gte mso 9]><xml> <o:DocumentProperties> <o:Author>Aarti</o:Author> <o:Template>Normal</o:Template> <o:LastAuthor>Aarti</o:LastAuthor> <o:Revision>11</o:Revision> <o:TotalTime>33</o:TotalTime> <o:Created>2015-01-27T03:44:00Z</o:Created> <o:LastSaved>2015-01-27T13:46:00Z</o:LastSaved> <o:Pages>8</o:Pages> <o:Words>4307</o:Words> <o:Characters>24554</o:Characters> <o:Lines>204</o:Lines> <o:Paragraphs>57</o:Paragraphs> <o:CharactersWithSpaces>28804</o:CharactersWithSpaces> <o:Version>15.00</o:Version> </o:DocumentProperties> <o:OfficeDocumentSettings> <o:AllowPNG/> </o:OfficeDocumentSettings> </xml><![endif]--> <link rel=themeData href="pubs_files/themedata.thmx"> <link rel=colorSchemeMapping href="pubs_files/colorschememapping.xml"> <!--[if gte mso 9]><xml> <w:WordDocument> <w:View>Print</w:View> <w:SpellingState>Clean</w:SpellingState> <w:GrammarState>Clean</w:GrammarState> <w:TrackMoves>false</w:TrackMoves> <w:TrackFormatting/> <w:ValidateAgainstSchemas/> <w:SaveIfXMLInvalid>false</w:SaveIfXMLInvalid> <w:IgnoreMixedContent>false</w:IgnoreMixedContent> <w:AlwaysShowPlaceholderText>false</w:AlwaysShowPlaceholderText> <w:DoNotPromoteQF/> <w:LidThemeOther>EN-US</w:LidThemeOther> <w:LidThemeAsian>X-NONE</w:LidThemeAsian> <w:LidThemeComplexScript>X-NONE</w:LidThemeComplexScript> <w:Compatibility> <w:BreakWrappedTables/> <w:SplitPgBreakAndParaMark/> </w:Compatibility> <w:BrowserLevel>MicrosoftInternetExplorer4</w:BrowserLevel> <m:mathPr> <m:mathFont m:val="Cambria Math"/> <m:brkBin m:val="before"/> <m:brkBinSub m:val="&#45;-"/> <m:smallFrac m:val="off"/> <m:dispDef/> <m:lMargin m:val="0"/> <m:rMargin m:val="0"/> <m:defJc m:val="centerGroup"/> <m:wrapIndent m:val="1440"/> <m:intLim m:val="subSup"/> <m:naryLim m:val="undOvr"/> </m:mathPr></w:WordDocument> </xml><![endif]--><!--[if gte mso 9]><xml> <w:LatentStyles DefLockedState="false" DefUnhideWhenUsed="false" DefSemiHidden="false" DefQFormat="false" DefPriority="99" LatentStyleCount="371"> <w:LsdException Locked="false" Priority="0" QFormat="true" Name="Normal"/> <w:LsdException Locked="false" Priority="9" QFormat="true" Name="heading 1"/> <w:LsdException Locked="false" Priority="9" QFormat="true" Name="heading 2"/> <w:LsdException Locked="false" Priority="9" SemiHidden="true" UnhideWhenUsed="true" QFormat="true" Name="heading 3"/> <w:LsdException Locked="false" Priority="9" SemiHidden="true" UnhideWhenUsed="true" QFormat="true" Name="heading 4"/> <w:LsdException Locked="false" Priority="9" SemiHidden="true" UnhideWhenUsed="true" QFormat="true" Name="heading 5"/> <w:LsdException Locked="false" Priority="9" SemiHidden="true" UnhideWhenUsed="true" QFormat="true" Name="heading 6"/> <w:LsdException Locked="false" Priority="9" SemiHidden="true" UnhideWhenUsed="true" QFormat="true" Name="heading 7"/> <w:LsdException Locked="false" Priority="9" SemiHidden="true" UnhideWhenUsed="true" QFormat="true" Name="heading 8"/> <w:LsdException Locked="false" Priority="9" SemiHidden="true" UnhideWhenUsed="true" QFormat="true" Name="heading 9"/> <w:LsdException Locked="false" SemiHidden="true" UnhideWhenUsed="true" Name="index 1"/> <w:LsdException Locked="false" SemiHidden="true" UnhideWhenUsed="true" Name="index 2"/> <w:LsdException Locked="false" SemiHidden="true" UnhideWhenUsed="true" Name="index 3"/> <w:LsdException Locked="false" SemiHidden="true" UnhideWhenUsed="true" Name="index 4"/> <w:LsdException Locked="false" SemiHidden="true" UnhideWhenUsed="true" Name="index 5"/> <w:LsdException Locked="false" SemiHidden="true" UnhideWhenUsed="true" Name="index 6"/> <w:LsdException Locked="false" SemiHidden="true" UnhideWhenUsed="true" Name="index 7"/> <w:LsdException Locked="false" SemiHidden="true" UnhideWhenUsed="true" Name="index 8"/> <w:LsdException Locked="false" SemiHidden="true" UnhideWhenUsed="true" Name="index 9"/> <w:LsdException Locked="false" Priority="39" SemiHidden="true" UnhideWhenUsed="true" Name="toc 1"/> <w:LsdException Locked="false" Priority="39" SemiHidden="true" UnhideWhenUsed="true" Name="toc 2"/> <w:LsdException Locked="false" Priority="39" SemiHidden="true" UnhideWhenUsed="true" Name="toc 3"/> <w:LsdException Locked="false" Priority="39" SemiHidden="true" UnhideWhenUsed="true" Name="toc 4"/> <w:LsdException Locked="false" Priority="39" SemiHidden="true" UnhideWhenUsed="true" Name="toc 5"/> <w:LsdException Locked="false" Priority="39" SemiHidden="true" UnhideWhenUsed="true" Name="toc 6"/> <w:LsdException Locked="false" Priority="39" SemiHidden="true" UnhideWhenUsed="true" Name="toc 7"/> <w:LsdException Locked="false" Priority="39" SemiHidden="true" UnhideWhenUsed="true" Name="toc 8"/> <w:LsdException Locked="false" Priority="39" SemiHidden="true" UnhideWhenUsed="true" Name="toc 9"/> <w:LsdException Locked="false" SemiHidden="true" UnhideWhenUsed="true" Name="Normal Indent"/> <w:LsdException Locked="false" SemiHidden="true" UnhideWhenUsed="true" Name="footnote text"/> <w:LsdException Locked="false" SemiHidden="true" UnhideWhenUsed="true" Name="annotation text"/> <w:LsdException Locked="false" SemiHidden="true" UnhideWhenUsed="true" Name="header"/> <w:LsdException Locked="false" SemiHidden="true" UnhideWhenUsed="true" Name="footer"/> <w:LsdException Locked="false" SemiHidden="true" UnhideWhenUsed="true" Name="index heading"/> <w:LsdException Locked="false" Priority="35" SemiHidden="true" UnhideWhenUsed="true" QFormat="true" Name="caption"/> <w:LsdException Locked="false" SemiHidden="true" UnhideWhenUsed="true" Name="table of figures"/> <w:LsdException Locked="false" SemiHidden="true" UnhideWhenUsed="true" Name="envelope address"/> <w:LsdException Locked="false" SemiHidden="true" UnhideWhenUsed="true" Name="envelope return"/> <w:LsdException Locked="false" SemiHidden="true" UnhideWhenUsed="true" Name="footnote reference"/> <w:LsdException Locked="false" SemiHidden="true" UnhideWhenUsed="true" Name="annotation reference"/> <w:LsdException Locked="false" SemiHidden="true" UnhideWhenUsed="true" Name="line number"/> <w:LsdException Locked="false" SemiHidden="true" UnhideWhenUsed="true" Name="page number"/> <w:LsdException Locked="false" SemiHidden="true" UnhideWhenUsed="true" Name="endnote reference"/> <w:LsdException Locked="false" SemiHidden="true" UnhideWhenUsed="true" Name="endnote text"/> <w:LsdException Locked="false" SemiHidden="true" UnhideWhenUsed="true" Name="table of authorities"/> <w:LsdException Locked="false" SemiHidden="true" UnhideWhenUsed="true" Name="macro"/> <w:LsdException Locked="false" SemiHidden="true" UnhideWhenUsed="true" Name="toa heading"/> <w:LsdException Locked="false" SemiHidden="true" UnhideWhenUsed="true" Name="List"/> <w:LsdException Locked="false" SemiHidden="true" UnhideWhenUsed="true" Name="List Bullet"/> <w:LsdException Locked="false" SemiHidden="true" UnhideWhenUsed="true" Name="List Number"/> <w:LsdException Locked="false" SemiHidden="true" UnhideWhenUsed="true" Name="List 2"/> <w:LsdException Locked="false" SemiHidden="true" UnhideWhenUsed="true" Name="List 3"/> <w:LsdException Locked="false" SemiHidden="true" UnhideWhenUsed="true" Name="List 4"/> <w:LsdException Locked="false" SemiHidden="true" UnhideWhenUsed="true" Name="List 5"/> <w:LsdException Locked="false" SemiHidden="true" UnhideWhenUsed="true" Name="List Bullet 2"/> <w:LsdException Locked="false" SemiHidden="true" UnhideWhenUsed="true" Name="List Bullet 3"/> <w:LsdException Locked="false" SemiHidden="true" UnhideWhenUsed="true" Name="List Bullet 4"/> <w:LsdException Locked="false" SemiHidden="true" UnhideWhenUsed="true" Name="List Bullet 5"/> <w:LsdException Locked="false" SemiHidden="true" UnhideWhenUsed="true" Name="List Number 2"/> <w:LsdException Locked="false" SemiHidden="true" UnhideWhenUsed="true" Name="List Number 3"/> <w:LsdException Locked="false" SemiHidden="true" UnhideWhenUsed="true" Name="List Number 4"/> <w:LsdException Locked="false" SemiHidden="true" UnhideWhenUsed="true" Name="List Number 5"/> <w:LsdException Locked="false" Priority="10" QFormat="true" Name="Title"/> <w:LsdException Locked="false" SemiHidden="true" UnhideWhenUsed="true" Name="Closing"/> <w:LsdException Locked="false" SemiHidden="true" UnhideWhenUsed="true" Name="Signature"/> <w:LsdException Locked="false" Priority="1" SemiHidden="true" UnhideWhenUsed="true" Name="Default Paragraph Font"/> <w:LsdException Locked="false" SemiHidden="true" UnhideWhenUsed="true" Name="Body Text"/> <w:LsdException Locked="false" SemiHidden="true" UnhideWhenUsed="true" Name="Body Text Indent"/> <w:LsdException Locked="false" SemiHidden="true" UnhideWhenUsed="true" Name="List Continue"/> <w:LsdException Locked="false" SemiHidden="true" UnhideWhenUsed="true" Name="List Continue 2"/> <w:LsdException Locked="false" SemiHidden="true" UnhideWhenUsed="true" Name="List Continue 3"/> <w:LsdException Locked="false" SemiHidden="true" UnhideWhenUsed="true" Name="List Continue 4"/> <w:LsdException Locked="false" SemiHidden="true" UnhideWhenUsed="true" Name="List Continue 5"/> <w:LsdException Locked="false" SemiHidden="true" UnhideWhenUsed="true" Name="Message Header"/> <w:LsdException Locked="false" Priority="11" QFormat="true" Name="Subtitle"/> <w:LsdException Locked="false" SemiHidden="true" UnhideWhenUsed="true" Name="Salutation"/> <w:LsdException Locked="false" SemiHidden="true" UnhideWhenUsed="true" Name="Date"/> <w:LsdException Locked="false" SemiHidden="true" UnhideWhenUsed="true" Name="Body Text First Indent"/> <w:LsdException Locked="false" SemiHidden="true" UnhideWhenUsed="true" Name="Body Text First Indent 2"/> <w:LsdException Locked="false" SemiHidden="true" UnhideWhenUsed="true" Name="Note Heading"/> <w:LsdException Locked="false" SemiHidden="true" UnhideWhenUsed="true" Name="Body Text 2"/> <w:LsdException Locked="false" SemiHidden="true" UnhideWhenUsed="true" Name="Body Text 3"/> <w:LsdException Locked="false" SemiHidden="true" UnhideWhenUsed="true" Name="Body Text Indent 2"/> <w:LsdException Locked="false" SemiHidden="true" UnhideWhenUsed="true" Name="Body Text Indent 3"/> <w:LsdException Locked="false" SemiHidden="true" UnhideWhenUsed="true" Name="Block Text"/> <w:LsdException Locked="false" SemiHidden="true" UnhideWhenUsed="true" Name="Hyperlink"/> <w:LsdException Locked="false" SemiHidden="true" UnhideWhenUsed="true" Name="FollowedHyperlink"/> <w:LsdException Locked="false" Priority="22" QFormat="true" Name="Strong"/> <w:LsdException Locked="false" Priority="20" QFormat="true" Name="Emphasis"/> <w:LsdException Locked="false" SemiHidden="true" UnhideWhenUsed="true" Name="Document Map"/> <w:LsdException Locked="false" SemiHidden="true" UnhideWhenUsed="true" Name="Plain Text"/> <w:LsdException Locked="false" SemiHidden="true" UnhideWhenUsed="true" Name="E-mail Signature"/> <w:LsdException Locked="false" SemiHidden="true" UnhideWhenUsed="true" Name="HTML Top of Form"/> <w:LsdException Locked="false" SemiHidden="true" UnhideWhenUsed="true" Name="HTML Bottom of Form"/> <w:LsdException Locked="false" SemiHidden="true" UnhideWhenUsed="true" Name="Normal (Web)"/> <w:LsdException Locked="false" SemiHidden="true" UnhideWhenUsed="true" Name="HTML Acronym"/> <w:LsdException Locked="false" SemiHidden="true" UnhideWhenUsed="true" Name="HTML Address"/> <w:LsdException Locked="false" SemiHidden="true" UnhideWhenUsed="true" Name="HTML Cite"/> <w:LsdException Locked="false" SemiHidden="true" UnhideWhenUsed="true" Name="HTML Code"/> <w:LsdException Locked="false" SemiHidden="true" UnhideWhenUsed="true" Name="HTML Definition"/> <w:LsdException Locked="false" SemiHidden="true" UnhideWhenUsed="true" Name="HTML Keyboard"/> <w:LsdException Locked="false" SemiHidden="true" UnhideWhenUsed="true" Name="HTML Preformatted"/> <w:LsdException Locked="false" SemiHidden="true" UnhideWhenUsed="true" Name="HTML Sample"/> <w:LsdException Locked="false" SemiHidden="true" UnhideWhenUsed="true" Name="HTML Typewriter"/> <w:LsdException Locked="false" SemiHidden="true" UnhideWhenUsed="true" Name="HTML Variable"/> <w:LsdException Locked="false" SemiHidden="true" UnhideWhenUsed="true" Name="Normal Table"/> <w:LsdException Locked="false" SemiHidden="true" UnhideWhenUsed="true" Name="annotation subject"/> <w:LsdException Locked="false" SemiHidden="true" UnhideWhenUsed="true" Name="No List"/> <w:LsdException Locked="false" SemiHidden="true" UnhideWhenUsed="true" Name="Outline List 1"/> <w:LsdException Locked="false" SemiHidden="true" UnhideWhenUsed="true" Name="Outline List 2"/> <w:LsdException Locked="false" SemiHidden="true" UnhideWhenUsed="true" Name="Outline List 3"/> <w:LsdException Locked="false" SemiHidden="true" UnhideWhenUsed="true" Name="Table Simple 1"/> <w:LsdException Locked="false" SemiHidden="true" UnhideWhenUsed="true" Name="Table Simple 2"/> <w:LsdException Locked="false" SemiHidden="true" UnhideWhenUsed="true" Name="Table Simple 3"/> <w:LsdException Locked="false" SemiHidden="true" UnhideWhenUsed="true" Name="Table Classic 1"/> <w:LsdException Locked="false" SemiHidden="true" UnhideWhenUsed="true" Name="Table Classic 2"/> <w:LsdException Locked="false" SemiHidden="true" UnhideWhenUsed="true" Name="Table Classic 3"/> <w:LsdException Locked="false" SemiHidden="true" UnhideWhenUsed="true" Name="Table Classic 4"/> <w:LsdException Locked="false" SemiHidden="true" UnhideWhenUsed="true" Name="Table Colorful 1"/> <w:LsdException Locked="false" SemiHidden="true" UnhideWhenUsed="true" Name="Table Colorful 2"/> <w:LsdException Locked="false" SemiHidden="true" UnhideWhenUsed="true" Name="Table Colorful 3"/> <w:LsdException Locked="false" SemiHidden="true" UnhideWhenUsed="true" Name="Table Columns 1"/> <w:LsdException Locked="false" SemiHidden="true" UnhideWhenUsed="true" Name="Table Columns 2"/> <w:LsdException Locked="false" SemiHidden="true" UnhideWhenUsed="true" Name="Table Columns 3"/> <w:LsdException Locked="false" SemiHidden="true" UnhideWhenUsed="true" Name="Table Columns 4"/> <w:LsdException Locked="false" SemiHidden="true" UnhideWhenUsed="true" Name="Table Columns 5"/> <w:LsdException Locked="false" SemiHidden="true" UnhideWhenUsed="true" Name="Table Grid 1"/> <w:LsdException Locked="false" SemiHidden="true" UnhideWhenUsed="true" Name="Table Grid 2"/> <w:LsdException Locked="false" SemiHidden="true" UnhideWhenUsed="true" Name="Table Grid 3"/> <w:LsdException Locked="false" SemiHidden="true" UnhideWhenUsed="true" Name="Table Grid 4"/> <w:LsdException Locked="false" SemiHidden="true" UnhideWhenUsed="true" Name="Table Grid 5"/> <w:LsdException Locked="false" SemiHidden="true" UnhideWhenUsed="true" Name="Table Grid 6"/> <w:LsdException Locked="false" SemiHidden="true" UnhideWhenUsed="true" Name="Table Grid 7"/> <w:LsdException Locked="false" SemiHidden="true" UnhideWhenUsed="true" Name="Table Grid 8"/> <w:LsdException Locked="false" SemiHidden="true" UnhideWhenUsed="true" Name="Table List 1"/> <w:LsdException Locked="false" SemiHidden="true" UnhideWhenUsed="true" Name="Table List 2"/> <w:LsdException Locked="false" SemiHidden="true" UnhideWhenUsed="true" Name="Table List 3"/> <w:LsdException Locked="false" SemiHidden="true" UnhideWhenUsed="true" Name="Table List 4"/> <w:LsdException Locked="false" SemiHidden="true" UnhideWhenUsed="true" Name="Table List 5"/> <w:LsdException Locked="false" SemiHidden="true" UnhideWhenUsed="true" Name="Table List 6"/> <w:LsdException Locked="false" SemiHidden="true" UnhideWhenUsed="true" Name="Table List 7"/> <w:LsdException Locked="false" SemiHidden="true" UnhideWhenUsed="true" Name="Table List 8"/> <w:LsdException Locked="false" SemiHidden="true" UnhideWhenUsed="true" Name="Table 3D effects 1"/> <w:LsdException Locked="false" SemiHidden="true" UnhideWhenUsed="true" Name="Table 3D effects 2"/> <w:LsdException Locked="false" SemiHidden="true" UnhideWhenUsed="true" Name="Table 3D effects 3"/> <w:LsdException Locked="false" SemiHidden="true" UnhideWhenUsed="true" Name="Table Contemporary"/> <w:LsdException Locked="false" SemiHidden="true" UnhideWhenUsed="true" Name="Table Elegant"/> <w:LsdException Locked="false" SemiHidden="true" UnhideWhenUsed="true" Name="Table Professional"/> <w:LsdException Locked="false" SemiHidden="true" UnhideWhenUsed="true" Name="Table Subtle 1"/> <w:LsdException Locked="false" SemiHidden="true" UnhideWhenUsed="true" Name="Table Subtle 2"/> <w:LsdException Locked="false" SemiHidden="true" UnhideWhenUsed="true" Name="Table Web 1"/> <w:LsdException Locked="false" SemiHidden="true" UnhideWhenUsed="true" Name="Table Web 2"/> <w:LsdException Locked="false" SemiHidden="true" UnhideWhenUsed="true" Name="Table Web 3"/> <w:LsdException Locked="false" SemiHidden="true" UnhideWhenUsed="true" Name="Balloon Text"/> <w:LsdException Locked="false" Priority="39" Name="Table Grid"/> <w:LsdException Locked="false" SemiHidden="true" UnhideWhenUsed="true" Name="Table Theme"/> <w:LsdException Locked="false" SemiHidden="true" Name="Placeholder Text"/> <w:LsdException Locked="false" Priority="1" QFormat="true" Name="No Spacing"/> <w:LsdException Locked="false" Priority="60" Name="Light Shading"/> <w:LsdException Locked="false" Priority="61" Name="Light List"/> <w:LsdException Locked="false" Priority="62" Name="Light Grid"/> <w:LsdException Locked="false" Priority="63" Name="Medium Shading 1"/> <w:LsdException Locked="false" Priority="64" Name="Medium Shading 2"/> <w:LsdException Locked="false" Priority="65" Name="Medium List 1"/> <w:LsdException Locked="false" Priority="66" Name="Medium List 2"/> <w:LsdException Locked="false" Priority="67" Name="Medium Grid 1"/> <w:LsdException Locked="false" Priority="68" Name="Medium Grid 2"/> <w:LsdException Locked="false" Priority="69" Name="Medium Grid 3"/> <w:LsdException Locked="false" Priority="70" Name="Dark List"/> <w:LsdException Locked="false" Priority="71" Name="Colorful Shading"/> <w:LsdException Locked="false" Priority="72" Name="Colorful List"/> <w:LsdException Locked="false" Priority="73" Name="Colorful Grid"/> <w:LsdException Locked="false" Priority="60" Name="Light Shading Accent 1"/> <w:LsdException Locked="false" Priority="61" Name="Light List Accent 1"/> <w:LsdException Locked="false" Priority="62" Name="Light Grid Accent 1"/> <w:LsdException Locked="false" Priority="63" Name="Medium Shading 1 Accent 1"/> <w:LsdException Locked="false" Priority="64" Name="Medium Shading 2 Accent 1"/> <w:LsdException Locked="false" Priority="65" Name="Medium List 1 Accent 1"/> <w:LsdException Locked="false" SemiHidden="true" Name="Revision"/> <w:LsdException Locked="false" Priority="34" QFormat="true" Name="List Paragraph"/> <w:LsdException Locked="false" Priority="29" QFormat="true" Name="Quote"/> <w:LsdException Locked="false" Priority="30" QFormat="true" Name="Intense Quote"/> <w:LsdException Locked="false" Priority="66" Name="Medium List 2 Accent 1"/> <w:LsdException Locked="false" Priority="67" Name="Medium Grid 1 Accent 1"/> <w:LsdException Locked="false" Priority="68" Name="Medium Grid 2 Accent 1"/> <w:LsdException Locked="false" Priority="69" Name="Medium Grid 3 Accent 1"/> <w:LsdException Locked="false" Priority="70" Name="Dark List Accent 1"/> <w:LsdException Locked="false" Priority="71" Name="Colorful Shading Accent 1"/> <w:LsdException Locked="false" Priority="72" Name="Colorful List Accent 1"/> <w:LsdException Locked="false" Priority="73" Name="Colorful Grid Accent 1"/> <w:LsdException Locked="false" Priority="60" Name="Light Shading Accent 2"/> <w:LsdException Locked="false" Priority="61" Name="Light List Accent 2"/> <w:LsdException Locked="false" Priority="62" Name="Light Grid Accent 2"/> <w:LsdException Locked="false" Priority="63" Name="Medium Shading 1 Accent 2"/> <w:LsdException Locked="false" Priority="64" Name="Medium Shading 2 Accent 2"/> <w:LsdException Locked="false" Priority="65" Name="Medium List 1 Accent 2"/> <w:LsdException Locked="false" Priority="66" Name="Medium List 2 Accent 2"/> <w:LsdException Locked="false" Priority="67" Name="Medium Grid 1 Accent 2"/> <w:LsdException Locked="false" Priority="68" Name="Medium Grid 2 Accent 2"/> <w:LsdException Locked="false" Priority="69" Name="Medium Grid 3 Accent 2"/> <w:LsdException Locked="false" Priority="70" Name="Dark List Accent 2"/> <w:LsdException Locked="false" Priority="71" Name="Colorful Shading Accent 2"/> <w:LsdException Locked="false" Priority="72" Name="Colorful List Accent 2"/> <w:LsdException Locked="false" Priority="73" Name="Colorful Grid Accent 2"/> <w:LsdException Locked="false" Priority="60" Name="Light Shading Accent 3"/> <w:LsdException Locked="false" Priority="61" Name="Light List Accent 3"/> <w:LsdException Locked="false" Priority="62" Name="Light Grid Accent 3"/> <w:LsdException Locked="false" Priority="63" Name="Medium Shading 1 Accent 3"/> <w:LsdException Locked="false" Priority="64" Name="Medium Shading 2 Accent 3"/> <w:LsdException Locked="false" Priority="65" Name="Medium List 1 Accent 3"/> <w:LsdException Locked="false" Priority="66" Name="Medium List 2 Accent 3"/> <w:LsdException Locked="false" Priority="67" Name="Medium Grid 1 Accent 3"/> <w:LsdException Locked="false" Priority="68" Name="Medium Grid 2 Accent 3"/> <w:LsdException Locked="false" Priority="69" Name="Medium Grid 3 Accent 3"/> <w:LsdException Locked="false" Priority="70" Name="Dark List Accent 3"/> <w:LsdException Locked="false" Priority="71" Name="Colorful Shading Accent 3"/> <w:LsdException Locked="false" Priority="72" Name="Colorful List Accent 3"/> <w:LsdException Locked="false" Priority="73" Name="Colorful Grid Accent 3"/> <w:LsdException Locked="false" Priority="60" Name="Light Shading Accent 4"/> <w:LsdException Locked="false" Priority="61" Name="Light List Accent 4"/> <w:LsdException Locked="false" Priority="62" Name="Light Grid Accent 4"/> <w:LsdException Locked="false" Priority="63" Name="Medium Shading 1 Accent 4"/> <w:LsdException Locked="false" Priority="64" Name="Medium Shading 2 Accent 4"/> <w:LsdException Locked="false" Priority="65" Name="Medium List 1 Accent 4"/> <w:LsdException Locked="false" Priority="66" Name="Medium List 2 Accent 4"/> <w:LsdException Locked="false" Priority="67" Name="Medium Grid 1 Accent 4"/> <w:LsdException Locked="false" Priority="68" Name="Medium Grid 2 Accent 4"/> <w:LsdException Locked="false" Priority="69" Name="Medium Grid 3 Accent 4"/> <w:LsdException Locked="false" Priority="70" Name="Dark List Accent 4"/> <w:LsdException Locked="false" Priority="71" Name="Colorful Shading Accent 4"/> <w:LsdException Locked="false" Priority="72" Name="Colorful List Accent 4"/> <w:LsdException Locked="false" Priority="73" Name="Colorful Grid Accent 4"/> <w:LsdException Locked="false" Priority="60" Name="Light Shading Accent 5"/> <w:LsdException Locked="false" Priority="61" Name="Light List Accent 5"/> <w:LsdException Locked="false" Priority="62" Name="Light Grid Accent 5"/> <w:LsdException Locked="false" Priority="63" Name="Medium Shading 1 Accent 5"/> <w:LsdException Locked="false" Priority="64" Name="Medium Shading 2 Accent 5"/> <w:LsdException Locked="false" Priority="65" Name="Medium List 1 Accent 5"/> <w:LsdException Locked="false" Priority="66" Name="Medium List 2 Accent 5"/> <w:LsdException Locked="false" Priority="67" Name="Medium Grid 1 Accent 5"/> <w:LsdException Locked="false" Priority="68" Name="Medium Grid 2 Accent 5"/> <w:LsdException Locked="false" Priority="69" Name="Medium Grid 3 Accent 5"/> <w:LsdException Locked="false" Priority="70" Name="Dark List Accent 5"/> <w:LsdException Locked="false" Priority="71" Name="Colorful Shading Accent 5"/> <w:LsdException Locked="false" Priority="72" Name="Colorful List Accent 5"/> <w:LsdException Locked="false" Priority="73" Name="Colorful Grid Accent 5"/> <w:LsdException Locked="false" Priority="60" Name="Light Shading Accent 6"/> <w:LsdException Locked="false" Priority="61" Name="Light List Accent 6"/> <w:LsdException Locked="false" Priority="62" Name="Light Grid Accent 6"/> <w:LsdException Locked="false" Priority="63" Name="Medium Shading 1 Accent 6"/> <w:LsdException Locked="false" Priority="64" Name="Medium Shading 2 Accent 6"/> <w:LsdException Locked="false" Priority="65" Name="Medium List 1 Accent 6"/> <w:LsdException Locked="false" Priority="66" Name="Medium List 2 Accent 6"/> <w:LsdException Locked="false" Priority="67" Name="Medium Grid 1 Accent 6"/> <w:LsdException Locked="false" Priority="68" Name="Medium Grid 2 Accent 6"/> <w:LsdException Locked="false" Priority="69" Name="Medium Grid 3 Accent 6"/> <w:LsdException Locked="false" Priority="70" Name="Dark List Accent 6"/> <w:LsdException Locked="false" Priority="71" Name="Colorful Shading Accent 6"/> <w:LsdException Locked="false" Priority="72" Name="Colorful List Accent 6"/> <w:LsdException Locked="false" Priority="73" Name="Colorful Grid Accent 6"/> <w:LsdException Locked="false" Priority="19" QFormat="true" Name="Subtle Emphasis"/> <w:LsdException Locked="false" Priority="21" QFormat="true" Name="Intense Emphasis"/> <w:LsdException Locked="false" Priority="31" QFormat="true" Name="Subtle Reference"/> <w:LsdException Locked="false" Priority="32" QFormat="true" Name="Intense Reference"/> <w:LsdException Locked="false" Priority="33" QFormat="true" Name="Book Title"/> <w:LsdException Locked="false" Priority="37" SemiHidden="true" UnhideWhenUsed="true" Name="Bibliography"/> <w:LsdException Locked="false" Priority="39" SemiHidden="true" UnhideWhenUsed="true" QFormat="true" Name="TOC Heading"/> <w:LsdException Locked="false" Priority="41" Name="Plain Table 1"/> <w:LsdException Locked="false" Priority="42" Name="Plain Table 2"/> <w:LsdException Locked="false" Priority="43" Name="Plain Table 3"/> <w:LsdException Locked="false" Priority="44" Name="Plain Table 4"/> <w:LsdException Locked="false" Priority="45" Name="Plain Table 5"/> <w:LsdException Locked="false" Priority="40" Name="Grid Table Light"/> <w:LsdException Locked="false" Priority="46" Name="Grid Table 1 Light"/> <w:LsdException Locked="false" Priority="47" Name="Grid Table 2"/> <w:LsdException Locked="false" Priority="48" Name="Grid Table 3"/> <w:LsdException Locked="false" Priority="49" Name="Grid Table 4"/> <w:LsdException Locked="false" Priority="50" Name="Grid Table 5 Dark"/> <w:LsdException Locked="false" Priority="51" Name="Grid Table 6 Colorful"/> <w:LsdException Locked="false" Priority="52" Name="Grid Table 7 Colorful"/> <w:LsdException Locked="false" Priority="46" Name="Grid Table 1 Light Accent 1"/> <w:LsdException Locked="false" Priority="47" Name="Grid Table 2 Accent 1"/> <w:LsdException Locked="false" Priority="48" Name="Grid Table 3 Accent 1"/> <w:LsdException Locked="false" Priority="49" Name="Grid Table 4 Accent 1"/> <w:LsdException Locked="false" Priority="50" Name="Grid Table 5 Dark Accent 1"/> <w:LsdException Locked="false" Priority="51" Name="Grid Table 6 Colorful Accent 1"/> <w:LsdException Locked="false" Priority="52" Name="Grid Table 7 Colorful Accent 1"/> <w:LsdException Locked="false" Priority="46" Name="Grid Table 1 Light Accent 2"/> <w:LsdException Locked="false" Priority="47" Name="Grid Table 2 Accent 2"/> <w:LsdException Locked="false" Priority="48" Name="Grid Table 3 Accent 2"/> <w:LsdException Locked="false" Priority="49" Name="Grid Table 4 Accent 2"/> <w:LsdException Locked="false" Priority="50" Name="Grid Table 5 Dark Accent 2"/> <w:LsdException Locked="false" Priority="51" Name="Grid Table 6 Colorful Accent 2"/> <w:LsdException Locked="false" Priority="52" Name="Grid Table 7 Colorful Accent 2"/> <w:LsdException Locked="false" Priority="46" Name="Grid Table 1 Light Accent 3"/> <w:LsdException Locked="false" Priority="47" Name="Grid Table 2 Accent 3"/> <w:LsdException Locked="false" Priority="48" Name="Grid Table 3 Accent 3"/> <w:LsdException Locked="false" Priority="49" Name="Grid Table 4 Accent 3"/> <w:LsdException Locked="false" Priority="50" Name="Grid Table 5 Dark Accent 3"/> <w:LsdException Locked="false" Priority="51" Name="Grid Table 6 Colorful Accent 3"/> <w:LsdException Locked="false" Priority="52" Name="Grid Table 7 Colorful Accent 3"/> <w:LsdException Locked="false" Priority="46" Name="Grid Table 1 Light Accent 4"/> <w:LsdException Locked="false" Priority="47" Name="Grid Table 2 Accent 4"/> <w:LsdException Locked="false" Priority="48" Name="Grid Table 3 Accent 4"/> <w:LsdException Locked="false" Priority="49" Name="Grid Table 4 Accent 4"/> <w:LsdException Locked="false" Priority="50" Name="Grid Table 5 Dark Accent 4"/> <w:LsdException Locked="false" Priority="51" Name="Grid Table 6 Colorful Accent 4"/> <w:LsdException Locked="false" Priority="52" Name="Grid Table 7 Colorful Accent 4"/> <w:LsdException Locked="false" Priority="46" Name="Grid Table 1 Light Accent 5"/> <w:LsdException Locked="false" Priority="47" Name="Grid Table 2 Accent 5"/> <w:LsdException Locked="false" Priority="48" Name="Grid Table 3 Accent 5"/> <w:LsdException Locked="false" Priority="49" Name="Grid Table 4 Accent 5"/> <w:LsdException Locked="false" Priority="50" Name="Grid Table 5 Dark Accent 5"/> <w:LsdException Locked="false" Priority="51" Name="Grid Table 6 Colorful Accent 5"/> <w:LsdException Locked="false" Priority="52" Name="Grid Table 7 Colorful Accent 5"/> <w:LsdException Locked="false" Priority="46" Name="Grid Table 1 Light Accent 6"/> <w:LsdException Locked="false" Priority="47" Name="Grid Table 2 Accent 6"/> <w:LsdException Locked="false" Priority="48" Name="Grid Table 3 Accent 6"/> <w:LsdException Locked="false" Priority="49" Name="Grid Table 4 Accent 6"/> <w:LsdException Locked="false" Priority="50" Name="Grid Table 5 Dark Accent 6"/> <w:LsdException Locked="false" Priority="51" Name="Grid Table 6 Colorful Accent 6"/> <w:LsdException Locked="false" Priority="52" Name="Grid Table 7 Colorful Accent 6"/> <w:LsdException Locked="false" Priority="46" Name="List Table 1 Light"/> <w:LsdException Locked="false" Priority="47" Name="List Table 2"/> <w:LsdException Locked="false" Priority="48" Name="List Table 3"/> <w:LsdException Locked="false" Priority="49" Name="List Table 4"/> <w:LsdException Locked="false" Priority="50" Name="List Table 5 Dark"/> <w:LsdException Locked="false" Priority="51" Name="List Table 6 Colorful"/> <w:LsdException Locked="false" Priority="52" Name="List Table 7 Colorful"/> <w:LsdException Locked="false" Priority="46" Name="List Table 1 Light Accent 1"/> <w:LsdException Locked="false" Priority="47" Name="List Table 2 Accent 1"/> <w:LsdException Locked="false" Priority="48" Name="List Table 3 Accent 1"/> <w:LsdException Locked="false" Priority="49" Name="List Table 4 Accent 1"/> <w:LsdException Locked="false" Priority="50" Name="List Table 5 Dark Accent 1"/> <w:LsdException Locked="false" Priority="51" Name="List Table 6 Colorful Accent 1"/> <w:LsdException Locked="false" Priority="52" Name="List Table 7 Colorful Accent 1"/> <w:LsdException Locked="false" Priority="46" Name="List Table 1 Light Accent 2"/> <w:LsdException Locked="false" Priority="47" Name="List Table 2 Accent 2"/> <w:LsdException Locked="false" Priority="48" Name="List Table 3 Accent 2"/> <w:LsdException Locked="false" Priority="49" Name="List Table 4 Accent 2"/> <w:LsdException Locked="false" Priority="50" Name="List Table 5 Dark Accent 2"/> <w:LsdException Locked="false" Priority="51" Name="List Table 6 Colorful Accent 2"/> <w:LsdException Locked="false" Priority="52" Name="List Table 7 Colorful Accent 2"/> <w:LsdException Locked="false" Priority="46" Name="List Table 1 Light Accent 3"/> <w:LsdException Locked="false" Priority="47" Name="List Table 2 Accent 3"/> <w:LsdException Locked="false" Priority="48" Name="List Table 3 Accent 3"/> <w:LsdException Locked="false" Priority="49" Name="List Table 4 Accent 3"/> <w:LsdException Locked="false" Priority="50" Name="List Table 5 Dark Accent 3"/> <w:LsdException Locked="false" Priority="51" Name="List Table 6 Colorful Accent 3"/> <w:LsdException Locked="false" Priority="52" Name="List Table 7 Colorful Accent 3"/> <w:LsdException Locked="false" Priority="46" Name="List Table 1 Light Accent 4"/> <w:LsdException Locked="false" Priority="47" Name="List Table 2 Accent 4"/> <w:LsdException Locked="false" Priority="48" Name="List Table 3 Accent 4"/> <w:LsdException Locked="false" Priority="49" Name="List Table 4 Accent 4"/> <w:LsdException Locked="false" Priority="50" Name="List Table 5 Dark Accent 4"/> <w:LsdException Locked="false" Priority="51" Name="List Table 6 Colorful Accent 4"/> <w:LsdException Locked="false" Priority="52" Name="List Table 7 Colorful Accent 4"/> <w:LsdException Locked="false" Priority="46" Name="List Table 1 Light Accent 5"/> <w:LsdException Locked="false" Priority="47" Name="List Table 2 Accent 5"/> <w:LsdException Locked="false" Priority="48" Name="List Table 3 Accent 5"/> <w:LsdException Locked="false" Priority="49" Name="List Table 4 Accent 5"/> <w:LsdException Locked="false" Priority="50" Name="List Table 5 Dark Accent 5"/> <w:LsdException Locked="false" Priority="51" Name="List Table 6 Colorful Accent 5"/> <w:LsdException Locked="false" Priority="52" Name="List Table 7 Colorful Accent 5"/> <w:LsdException Locked="false" Priority="46" Name="List Table 1 Light Accent 6"/> <w:LsdException Locked="false" Priority="47" Name="List Table 2 Accent 6"/> <w:LsdException Locked="false" Priority="48" Name="List Table 3 Accent 6"/> <w:LsdException Locked="false" Priority="49" Name="List Table 4 Accent 6"/> <w:LsdException Locked="false" Priority="50" Name="List Table 5 Dark Accent 6"/> <w:LsdException Locked="false" Priority="51" Name="List Table 6 Colorful Accent 6"/> <w:LsdException Locked="false" Priority="52" Name="List Table 7 Colorful Accent 6"/> </w:LatentStyles> </xml><![endif]--> <style> <!-- /* Font Definitions */ @font-face {font-family:Wingdings; panose-1:5 0 0 0 0 0 0 0 0 0; mso-font-charset:2; mso-generic-font-family:auto; mso-font-pitch:variable; mso-font-signature:0 268435456 0 0 -2147483648 0;} @font-face {font-family:"MS Mincho"; panose-1:2 2 6 9 4 2 5 8 3 4; mso-font-alt:"-ÿ3ÿ fg"; mso-font-charset:128; mso-generic-font-family:modern; mso-font-pitch:fixed; mso-font-signature:-536870145 1791491579 18 0 131231 0;} @font-face {font-family:"Cambria Math"; panose-1:2 4 5 3 5 4 6 3 2 4; mso-font-charset:1; mso-generic-font-family:roman; mso-font-format:other; mso-font-pitch:variable; mso-font-signature:0 0 0 0 0 0;} @font-face {font-family:Calibri; panose-1:2 15 5 2 2 2 4 3 2 4; mso-font-charset:0; mso-generic-font-family:swiss; mso-font-pitch:variable; mso-font-signature:-536870145 1073786111 1 0 415 0;} @font-face {font-family:"\@MS Mincho"; panose-1:2 2 6 9 4 2 5 8 3 4; mso-font-charset:128; mso-generic-font-family:modern; mso-font-pitch:fixed; mso-font-signature:-536870145 1791491579 18 0 131231 0;} /* Style Definitions */ p.MsoNormal, li.MsoNormal, div.MsoNormal {mso-style-unhide:no; mso-style-qformat:yes; mso-style-parent:""; margin:0in; margin-bottom:.0001pt; mso-pagination:widow-orphan; font-size:12.0pt; font-family:"Times New Roman",serif; mso-fareast-font-family:"Times New Roman"; mso-fareast-theme-font:minor-fareast;} h2 {mso-style-priority:9; mso-style-unhide:no; mso-style-qformat:yes; mso-style-link:"Heading 2 Char"; mso-margin-top-alt:auto; margin-right:0in; mso-margin-bottom-alt:auto; margin-left:0in; mso-pagination:widow-orphan; mso-outline-level:2; font-size:18.0pt; font-family:"Times New Roman",serif; mso-fareast-font-family:"Times New Roman"; mso-fareast-theme-font:minor-fareast; font-weight:bold;} a:link, span.MsoHyperlink {mso-style-noshow:yes; mso-style-priority:99; color:blue; text-decoration:underline; text-underline:single;} a:visited, span.MsoHyperlinkFollowed {mso-style-noshow:yes; mso-style-priority:99; color:purple; text-decoration:underline; text-underline:single;} p {mso-style-noshow:yes; mso-style-priority:99; mso-margin-top-alt:auto; margin-right:0in; mso-margin-bottom-alt:auto; margin-left:0in; mso-pagination:widow-orphan; font-size:12.0pt; font-family:"Times New Roman",serif; mso-fareast-font-family:"Times New Roman"; mso-fareast-theme-font:minor-fareast;} p.MsoListParagraph, li.MsoListParagraph, div.MsoListParagraph {mso-style-noshow:yes; mso-style-priority:34; mso-style-unhide:no; mso-style-qformat:yes; margin-top:0in; margin-right:0in; margin-bottom:0in; margin-left:.5in; margin-bottom:.0001pt; mso-add-space:auto; mso-pagination:widow-orphan; font-size:12.0pt; mso-bidi-font-size:10.0pt; font-family:"Times New Roman",serif; mso-fareast-font-family:"Times New Roman";} p.MsoListParagraphCxSpFirst, li.MsoListParagraphCxSpFirst, div.MsoListParagraphCxSpFirst {mso-style-noshow:yes; mso-style-priority:34; mso-style-unhide:no; mso-style-qformat:yes; mso-style-type:export-only; margin-top:0in; margin-right:0in; margin-bottom:0in; margin-left:.5in; margin-bottom:.0001pt; mso-add-space:auto; mso-pagination:widow-orphan; font-size:12.0pt; mso-bidi-font-size:10.0pt; font-family:"Times New Roman",serif; mso-fareast-font-family:"Times New Roman";} p.MsoListParagraphCxSpMiddle, li.MsoListParagraphCxSpMiddle, div.MsoListParagraphCxSpMiddle {mso-style-noshow:yes; mso-style-priority:34; mso-style-unhide:no; mso-style-qformat:yes; mso-style-type:export-only; margin-top:0in; margin-right:0in; margin-bottom:0in; margin-left:.5in; margin-bottom:.0001pt; mso-add-space:auto; mso-pagination:widow-orphan; font-size:12.0pt; mso-bidi-font-size:10.0pt; font-family:"Times New Roman",serif; mso-fareast-font-family:"Times New Roman";} p.MsoListParagraphCxSpLast, li.MsoListParagraphCxSpLast, div.MsoListParagraphCxSpLast {mso-style-noshow:yes; mso-style-priority:34; mso-style-unhide:no; mso-style-qformat:yes; mso-style-type:export-only; margin-top:0in; margin-right:0in; margin-bottom:0in; margin-left:.5in; margin-bottom:.0001pt; mso-add-space:auto; mso-pagination:widow-orphan; font-size:12.0pt; mso-bidi-font-size:10.0pt; font-family:"Times New Roman",serif; mso-fareast-font-family:"Times New Roman";} span.Heading2Char {mso-style-name:"Heading 2 Char"; mso-style-noshow:yes; mso-style-priority:9; mso-style-unhide:no; mso-style-locked:yes; mso-style-link:"Heading 2"; mso-ansi-font-size:13.0pt; mso-bidi-font-size:13.0pt; font-family:"Calibri Light",sans-serif; mso-ascii-font-family:"Calibri Light"; mso-ascii-theme-font:major-latin; mso-fareast-font-family:"Times New Roman"; mso-fareast-theme-font:major-fareast; mso-hansi-font-family:"Calibri Light"; mso-hansi-theme-font:major-latin; mso-bidi-font-family:"Times New Roman"; mso-bidi-theme-font:major-bidi; color:#2E74B5; mso-themecolor:accent1; mso-themeshade:191;} span.smalltitle {mso-style-name:smalltitle; mso-style-unhide:no;} span.main {mso-style-name:main; mso-style-unhide:no;} span.Title1 {mso-style-name:Title1; mso-style-unhide:no;} span.this-person {mso-style-name:this-person; mso-style-unhide:no;} span.apple-converted-space {mso-style-name:apple-converted-space; mso-style-unhide:no;} span.Title2 {mso-style-name:Title2; mso-style-unhide:no;} span.SpellE {mso-style-name:""; mso-spl-e:yes;} span.GramE {mso-style-name:""; mso-gram-e:yes;} .MsoChpDefault {mso-style-type:export-only; mso-default-props:yes; font-size:10.0pt; mso-ansi-font-size:10.0pt; mso-bidi-font-size:10.0pt;} @page WordSection1 {size:8.5in 11.0in; margin:1.0in 1.0in 1.0in 1.0in; mso-header-margin:.5in; mso-footer-margin:.5in; mso-paper-source:0;} div.WordSection1 {page:WordSection1;} /* List Definitions */ @list l0 {mso-list-id:181675969; mso-list-type:hybrid; mso-list-template-ids:-1442137050 67698689 67698691 67698693 67698689 67698691 67698693 67698689 67698691 67698693;} @list l0:level1 {mso-level-number-format:bullet; mso-level-text:·ð; mso-level-tab-stop:none; mso-level-number-position:left; text-indent:-.25in; font-family:Symbol;} @list l0:level2 {mso-level-number-format:bullet; mso-level-text:o; mso-level-tab-stop:none; mso-level-number-position:left; text-indent:-.25in; font-family:"Courier New";} @list l0:level3 {mso-level-number-format:bullet; mso-level-text:§ð; mso-level-tab-stop:none; mso-level-number-position:left; text-indent:-.25in; font-family:Wingdings;} @list l0:level4 {mso-level-number-format:bullet; mso-level-text:·ð; mso-level-tab-stop:none; mso-level-number-position:left; text-indent:-.25in; font-family:Symbol;} @list l0:level5 {mso-level-number-format:bullet; mso-level-text:o; mso-level-tab-stop:none; mso-level-number-position:left; text-indent:-.25in; font-family:"Courier New";} @list l0:level6 {mso-level-number-format:bullet; mso-level-text:§ð; mso-level-tab-stop:none; mso-level-number-position:left; text-indent:-.25in; font-family:Wingdings;} @list l0:level7 {mso-level-number-format:bullet; mso-level-text:·ð; mso-level-tab-stop:none; mso-level-number-position:left; text-indent:-.25in; font-family:Symbol;} @list l0:level8 {mso-level-number-format:bullet; mso-level-text:o; mso-level-tab-stop:none; mso-level-number-position:left; text-indent:-.25in; font-family:"Courier New";} @list l0:level9 {mso-level-number-format:bullet; mso-level-text:§ð; mso-level-tab-stop:none; mso-level-number-position:left; text-indent:-.25in; font-family:Wingdings;} @list l1 {mso-list-id:1119186531; mso-list-type:hybrid; mso-list-template-ids:1103012222 67698689 67698691 67698693 67698689 67698691 67698693 67698689 67698691 67698693;} @list l1:level1 {mso-level-number-format:bullet; mso-level-text:·ð; mso-level-tab-stop:none; mso-level-number-position:left; text-indent:-.25in; font-family:Symbol;} @list l1:level2 {mso-level-number-format:bullet; mso-level-text:o; mso-level-tab-stop:none; mso-level-number-position:left; text-indent:-.25in; font-family:"Courier New";} @list l1:level3 {mso-level-number-format:bullet; mso-level-text:§ð; mso-level-tab-stop:none; mso-level-number-position:left; text-indent:-.25in; font-family:Wingdings;} @list l1:level4 {mso-level-number-format:bullet; mso-level-text:·ð; mso-level-tab-stop:none; mso-level-number-position:left; text-indent:-.25in; font-family:Symbol;} @list l1:level5 {mso-level-number-format:bullet; mso-level-text:o; mso-level-tab-stop:none; mso-level-number-position:left; text-indent:-.25in; font-family:"Courier New";} @list l1:level6 {mso-level-number-format:bullet; mso-level-text:§ð; mso-level-tab-stop:none; mso-level-number-position:left; text-indent:-.25in; font-family:Wingdings;} @list l1:level7 {mso-level-number-format:bullet; mso-level-text:·ð; mso-level-tab-stop:none; mso-level-number-position:left; text-indent:-.25in; font-family:Symbol;} @list l1:level8 {mso-level-number-format:bullet; mso-level-text:o; mso-level-tab-stop:none; mso-level-number-position:left; text-indent:-.25in; font-family:"Courier New";} @list l1:level9 {mso-level-number-format:bullet; mso-level-text:§ð; mso-level-tab-stop:none; mso-level-number-position:left; text-indent:-.25in; font-family:Wingdings;} ol {margin-bottom:0in;} ul {margin-bottom:0in;} --> </style> <!--[if gte mso 10]> <style> /* Style Definitions */ table.MsoNormalTable {mso-style-name:"Table Normal"; mso-tstyle-rowband-size:0; mso-tstyle-colband-size:0; mso-style-noshow:yes; mso-style-priority:99; mso-style-parent:""; mso-padding-alt:0in 5.4pt 0in 5.4pt; mso-para-margin:0in; mso-para-margin-bottom:.0001pt; mso-pagination:widow-orphan; font-size:10.0pt; font-family:"Times New Roman",serif;} </style> <![endif]--><!--[if gte mso 9]><xml> <o:shapedefaults v:ext="edit" spidmax="1026"/> </xml><![endif]--><!--[if gte mso 9]><xml> <o:shapelayout v:ext="edit"> <o:idmap v:ext="edit" data="1"/> </o:shapelayout></xml><![endif]--> </head> <body lang=EN-US link=blue vlink=purple style='tab-interval:.5in'> <div class=WordSection1> <h2 align=center style='text-align:center'><span style='font-size:16.0pt; font-family:"Arial",sans-serif;mso-fareast-font-family:"Times New Roman"; color:#1F4E79;mso-themecolor:accent1;mso-themeshade:128;mso-style-textfill-fill-color: #1F4E79;mso-style-textfill-fill-themecolor:accent1;mso-style-textfill-fill-alpha: 100.0%;mso-style-textfill-fill-colortransforms:lumm=50000'>Aarti Gupta: Publications</span><span style='font-size:16.0pt;mso-fareast-font-family:"Times New Roman"; color:#1F4E79;mso-themecolor:accent1;mso-themeshade:128;mso-style-textfill-fill-color: #1F4E79;mso-style-textfill-fill-themecolor:accent1;mso-style-textfill-fill-alpha: 100.0%;mso-style-textfill-fill-colortransforms:lumm=50000'><o:p></o:p></span></h2> <div class=MsoNormal align=center style='text-align:center'><span style='font-family:"Arial",sans-serif;mso-fareast-font-family:"Times New Roman"'> <hr size=2 width="100%" align=center> </span></div> <p class=MsoNormal><a name=books><b style='mso-bidi-font-weight:normal'><span style='font-family:"Calibri",sans-serif;mso-ascii-theme-font:minor-latin; mso-hansi-theme-font:minor-latin'><o:p>&nbsp;</o:p></span></b></a></p> <p class=MsoNormal><span style='mso-bookmark:books'><b style='mso-bidi-font-weight: normal'><span style='font-family:"Calibri",sans-serif;mso-ascii-theme-font: minor-latin;mso-hansi-theme-font:minor-latin'>Books and Edited Volumes<o:p></o:p></span></b></span></p> <span style='mso-bookmark:books'></span> <p class=MsoListParagraphCxSpFirst style='text-indent:-.25in;mso-list:l0 level1 lfo2'><![if !supportLists]><span style='font-size:11.0pt;font-family:Symbol;mso-fareast-font-family:Symbol; mso-bidi-font-family:Symbol'><span style='mso-list:Ignore'>·<span style='font:7.0pt "Times New Roman"'>&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp; </span></span></span><![endif]><b style='mso-bidi-font-weight:normal'><span style='font-size:11.0pt;font-family:"Calibri",sans-serif;mso-ascii-theme-font: minor-latin;mso-hansi-theme-font:minor-latin;mso-bidi-font-family:Arial'>Book:</span></b><span style='font-size:11.0pt;font-family:"Calibri",sans-serif;mso-ascii-theme-font: minor-latin;mso-hansi-theme-font:minor-latin;mso-bidi-font-family:Arial'> M. K. </span><span class=SpellE><span style='font-size:11.0pt;font-family:"Calibri",sans-serif; mso-ascii-theme-font:minor-latin;mso-hansi-theme-font:minor-latin'>Ganai</span></span><span style='font-size:11.0pt;font-family:"Calibri",sans-serif;mso-ascii-theme-font: minor-latin;mso-hansi-theme-font:minor-latin;mso-bidi-font-family:Arial'> and A. Gupta: SAT-based Scalable Formal Verification Solutions. Springer, August 2007.</span><span style='font-size:11.0pt;font-family:"Calibri",sans-serif; mso-ascii-theme-font:minor-latin;mso-hansi-theme-font:minor-latin'><o:p></o:p></span></p> <p class=MsoListParagraphCxSpMiddle style='text-indent:-.25in;mso-list:l0 level1 lfo2'><![if !supportLists]><span style='font-size:11.0pt;font-family:Symbol;mso-fareast-font-family:Symbol; mso-bidi-font-family:Symbol'><span style='mso-list:Ignore'>·<span style='font:7.0pt "Times New Roman"'>&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp; </span></span></span><![endif]><span style='font-size:11.0pt;font-family:"Calibri",sans-serif; mso-ascii-theme-font:minor-latin;mso-hansi-theme-font:minor-latin;mso-bidi-font-family: Arial'>A. Gupta and D. </span><span class=SpellE><span style='font-size:11.0pt; font-family:"Calibri",sans-serif;mso-ascii-theme-font:minor-latin;mso-hansi-theme-font: minor-latin'>Kroening</span></span><span style='font-size:11.0pt;font-family: "Calibri",sans-serif;mso-ascii-theme-font:minor-latin;mso-hansi-theme-font: minor-latin;mso-bidi-font-family:Arial'>, editors: Proceedings of the 8th International Workshop on </span><span class=SpellE><span style='font-size: 11.0pt;font-family:"Calibri",sans-serif;mso-ascii-theme-font:minor-latin; mso-hansi-theme-font:minor-latin'>Satisfiability</span></span><span style='font-size:11.0pt;font-family:"Calibri",sans-serif;mso-ascii-theme-font: minor-latin;mso-hansi-theme-font:minor-latin;mso-bidi-font-family:Arial'> Modulo Theories (SMT '10), July 2010. Edinburgh, Scotland, United Kingdom.</span><span style='font-size:11.0pt;font-family:"Calibri",sans-serif;mso-ascii-theme-font: minor-latin;mso-hansi-theme-font:minor-latin'><o:p></o:p></span></p> <p class=MsoListParagraphCxSpMiddle style='text-indent:-.25in;mso-list:l0 level1 lfo2'><![if !supportLists]><span style='font-size:11.0pt;font-family:Symbol;mso-fareast-font-family:Symbol; mso-bidi-font-family:Symbol'><span style='mso-list:Ignore'>·<span style='font:7.0pt "Times New Roman"'>&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp; </span></span></span><![endif]><span style='font-size:11.0pt;font-family:"Calibri",sans-serif; mso-ascii-theme-font:minor-latin;mso-hansi-theme-font:minor-latin;mso-bidi-font-family: Arial'>A. Gupta and S. Malik, editors: Computer Aided Verification, 20th International Conference, CAV 2008, Princeton, NJ, USA. Lecture Notes in Computer Science 5123, Springer, 2008.</span><span style='font-size:11.0pt; font-family:"Calibri",sans-serif;mso-ascii-theme-font:minor-latin;mso-hansi-theme-font: minor-latin'><o:p></o:p></span></p> <p class=MsoListParagraphCxSpLast style='text-indent:-.25in;mso-list:l0 level1 lfo2'><![if !supportLists]><span style='font-size:11.0pt;font-family:Symbol;mso-fareast-font-family:Symbol; mso-bidi-font-family:Symbol'><span style='mso-list:Ignore'>·<span style='font:7.0pt "Times New Roman"'>&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp; </span></span></span><![endif]><span style='font-size:11.0pt;font-family:"Calibri",sans-serif; mso-ascii-theme-font:minor-latin;mso-hansi-theme-font:minor-latin'>A. Gupta and P. <span class=SpellE>Manolios</span>, editors: Proceedings of the ACM/IEEE Formal Methods in Computer-Aided Design Conference. IEEE, November 2006.<o:p></o:p></span></p> <h2><span style='font-size:14.0pt;font-family:"Calibri",sans-serif;mso-ascii-theme-font: minor-latin;mso-fareast-font-family:"Times New Roman";mso-hansi-theme-font: minor-latin;mso-bidi-font-family:Arial'>Publications by Topic<a name="_Books_and_Edited"></a><a name="_Distributed_System_Testing"></a><o:p></o:p></span></h2> <p class=MsoListParagraphCxSpFirst style='text-indent:-.25in;mso-list:l1 level1 lfo1'><![if !supportLists]><span style='font-size:14.0pt;font-family:Symbol;mso-fareast-font-family:Symbol; mso-bidi-font-family:Symbol;color:#1F4E79;mso-themecolor:accent1;mso-themeshade: 128;mso-style-textfill-fill-color:#1F4E79;mso-style-textfill-fill-themecolor: accent1;mso-style-textfill-fill-alpha:100.0%;mso-style-textfill-fill-colortransforms: lumm=50000'><span style='mso-list:Ignore'>·<span style='font:7.0pt "Times New Roman"'>&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp; </span></span></span><![endif]><span style='font-family:"Calibri",sans-serif; mso-ascii-theme-font:minor-latin;mso-hansi-theme-font:minor-latin;color:#1F4E79; mso-themecolor:accent1;mso-themeshade:128;mso-style-textfill-fill-color:#1F4E79; mso-style-textfill-fill-themecolor:accent1;mso-style-textfill-fill-alpha:100.0%; mso-style-textfill-fill-colortransforms:lumm=50000'><a href="#distributed"><span style='mso-bidi-font-size:12.0pt;color:#1F4E79;mso-themecolor:accent1; mso-themeshade:128;mso-style-textfill-fill-color:#1F4E79;mso-style-textfill-fill-themecolor: accent1;mso-style-textfill-fill-alpha:100.0%;mso-style-textfill-fill-colortransforms: lumm=50000'>Distributed System Testing and Verification</span></a></span><span style='font-size:14.0pt;font-family:"Calibri",sans-serif;mso-ascii-theme-font: minor-latin;mso-hansi-theme-font:minor-latin;mso-bidi-font-family:Arial; color:#1F4E79;mso-themecolor:accent1;mso-themeshade:128;mso-style-textfill-fill-color: #1F4E79;mso-style-textfill-fill-themecolor:accent1;mso-style-textfill-fill-alpha: 100.0%;mso-style-textfill-fill-colortransforms:lumm=50000'><o:p></o:p></span></p> <p class=MsoListParagraphCxSpMiddle style='text-indent:-.25in;mso-list:l1 level1 lfo1'><![if !supportLists]><span style='font-family:Symbol;mso-fareast-font-family:Symbol;mso-bidi-font-family: Symbol;color:#1F4E79;mso-themecolor:accent1;mso-themeshade:128;mso-style-textfill-fill-color: #1F4E79;mso-style-textfill-fill-themecolor:accent1;mso-style-textfill-fill-alpha: 100.0%;mso-style-textfill-fill-colortransforms:lumm=50000'><span style='mso-list:Ignore'>·<span style='font:7.0pt "Times New Roman"'>&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp; </span></span></span><![endif]><span style='font-family:"Calibri",sans-serif; mso-ascii-theme-font:minor-latin;mso-hansi-theme-font:minor-latin;color:#1F4E79; mso-themecolor:accent1;mso-themeshade:128;mso-style-textfill-fill-color:#1F4E79; mso-style-textfill-fill-themecolor:accent1;mso-style-textfill-fill-alpha:100.0%; mso-style-textfill-fill-colortransforms:lumm=50000'><a href="#concurrency"><span style='mso-bidi-font-size:12.0pt;color:#1F4E79;mso-themecolor:accent1; mso-themeshade:128;mso-style-textfill-fill-color:#1F4E79;mso-style-textfill-fill-themecolor: accent1;mso-style-textfill-fill-alpha:100.0%;mso-style-textfill-fill-colortransforms: lumm=50000'>Concurrency Verification</span></a><u><o:p></o:p></u></span></p> <p class=MsoListParagraphCxSpMiddle style='text-indent:-.25in;mso-list:l1 level1 lfo1'><![if !supportLists]><span style='font-family:Symbol;mso-fareast-font-family:Symbol;mso-bidi-font-family: Symbol;color:#1F4E79;mso-themecolor:accent1;mso-themeshade:128;mso-style-textfill-fill-color: #1F4E79;mso-style-textfill-fill-themecolor:accent1;mso-style-textfill-fill-alpha: 100.0%;mso-style-textfill-fill-colortransforms:lumm=50000'><span style='mso-list:Ignore'>·<span style='font:7.0pt "Times New Roman"'>&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp; </span></span></span><![endif]><span style='font-family:"Calibri",sans-serif; mso-ascii-theme-font:minor-latin;mso-hansi-theme-font:minor-latin;color:#1F4E79; mso-themecolor:accent1;mso-themeshade:128;mso-style-textfill-fill-color:#1F4E79; mso-style-textfill-fill-themecolor:accent1;mso-style-textfill-fill-alpha:100.0%; mso-style-textfill-fill-colortransforms:lumm=50000'><a href="#program"><span style='mso-bidi-font-size:12.0pt;color:#1F4E79;mso-themecolor:accent1; mso-themeshade:128;mso-style-textfill-fill-color:#1F4E79;mso-style-textfill-fill-themecolor: accent1;mso-style-textfill-fill-alpha:100.0%;mso-style-textfill-fill-colortransforms: lumm=50000'>Program Analysis and Verification</span></a><o:p></o:p></span></p> <p class=MsoListParagraphCxSpMiddle style='text-indent:-.25in;mso-list:l1 level1 lfo1'><![if !supportLists]><span style='font-family:Symbol;mso-fareast-font-family:Symbol;mso-bidi-font-family: Symbol;color:#1F4E79;mso-themecolor:accent1;mso-themeshade:128;mso-style-textfill-fill-color: #1F4E79;mso-style-textfill-fill-themecolor:accent1;mso-style-textfill-fill-alpha: 100.0%;mso-style-textfill-fill-colortransforms:lumm=50000'><span style='mso-list:Ignore'>·<span style='font:7.0pt "Times New Roman"'>&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp; </span></span></span><![endif]><span style='font-family:"Calibri",sans-serif; mso-ascii-theme-font:minor-latin;mso-hansi-theme-font:minor-latin;color:#1F4E79; mso-themecolor:accent1;mso-themeshade:128;mso-style-textfill-fill-color:#1F4E79; mso-style-textfill-fill-themecolor:accent1;mso-style-textfill-fill-alpha:100.0%; mso-style-textfill-fill-colortransforms:lumm=50000'><a href="#decisionproc"><span style='mso-bidi-font-size:12.0pt;color:#1F4E79;mso-themecolor:accent1; mso-themeshade:128;mso-style-textfill-fill-color:#1F4E79;mso-style-textfill-fill-themecolor: accent1;mso-style-textfill-fill-alpha:100.0%;mso-style-textfill-fill-colortransforms: lumm=50000'>Automatic Decision Procedures</span></a><o:p></o:p></span></p> <p class=MsoListParagraphCxSpMiddle style='text-indent:-.25in;mso-list:l1 level1 lfo1'><![if !supportLists]><span style='font-family:Symbol;mso-fareast-font-family:Symbol;mso-bidi-font-family: Symbol;color:#1F4E79;mso-themecolor:accent1;mso-themeshade:128;mso-style-textfill-fill-color: #1F4E79;mso-style-textfill-fill-themecolor:accent1;mso-style-textfill-fill-alpha: 100.0%;mso-style-textfill-fill-colortransforms:lumm=50000'><span style='mso-list:Ignore'>·<span style='font:7.0pt "Times New Roman"'>&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp; </span></span></span><![endif]><span style='font-family:"Calibri",sans-serif; mso-ascii-theme-font:minor-latin;mso-hansi-theme-font:minor-latin;color:#1F4E79; mso-themecolor:accent1;mso-themeshade:128;mso-style-textfill-fill-color:#1F4E79; mso-style-textfill-fill-themecolor:accent1;mso-style-textfill-fill-alpha:100.0%; mso-style-textfill-fill-colortransforms:lumm=50000'><a href="#eda"><span style='mso-bidi-font-size:12.0pt;color:#1F4E79;mso-themecolor:accent1; mso-themeshade:128;mso-style-textfill-fill-color:#1F4E79;mso-style-textfill-fill-themecolor: accent1;mso-style-textfill-fill-alpha:100.0%;mso-style-textfill-fill-colortransforms: lumm=50000'>Verification in Electronic Design Automation</span></a><o:p></o:p></span></p> <p class=MsoListParagraphCxSpMiddle style='text-indent:-.25in;mso-list:l1 level1 lfo1'><![if !supportLists]><span style='font-family:Symbol;mso-fareast-font-family:Symbol;mso-bidi-font-family: Symbol;color:#1F4E79;mso-themecolor:accent1;mso-themeshade:128;mso-style-textfill-fill-color: #1F4E79;mso-style-textfill-fill-themecolor:accent1;mso-style-textfill-fill-alpha: 100.0%;mso-style-textfill-fill-colortransforms:lumm=50000'><span style='mso-list:Ignore'>·<span style='font:7.0pt "Times New Roman"'>&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp; </span></span></span><![endif]><span style='font-family:"Calibri",sans-serif; mso-ascii-theme-font:minor-latin;mso-hansi-theme-font:minor-latin;color:#1F4E79; mso-themecolor:accent1;mso-themeshade:128;mso-style-textfill-fill-color:#1F4E79; mso-style-textfill-fill-themecolor:accent1;mso-style-textfill-fill-alpha:100.0%; mso-style-textfill-fill-colortransforms:lumm=50000'><a href="#phd"><span style='mso-bidi-font-size:12.0pt;color:#1F4E79;mso-themecolor:accent1; mso-themeshade:128;mso-style-textfill-fill-color:#1F4E79;mso-style-textfill-fill-themecolor: accent1;mso-style-textfill-fill-alpha:100.0%;mso-style-textfill-fill-colortransforms: lumm=50000'>BDD-based Verification (Ph.D. Thesis research)</span></a><o:p></o:p></span></p> <p class=MsoListParagraphCxSpLast style='text-indent:-.25in;mso-list:l1 level1 lfo1'><![if !supportLists]><span style='font-family:Symbol;mso-fareast-font-family:Symbol;mso-bidi-font-family: Symbol;color:#1F4E79;mso-themecolor:accent1;mso-themeshade:128;mso-style-textfill-fill-color: #1F4E79;mso-style-textfill-fill-themecolor:accent1;mso-style-textfill-fill-alpha: 100.0%;mso-style-textfill-fill-colortransforms:lumm=50000'><span style='mso-list:Ignore'>·<span style='font:7.0pt "Times New Roman"'>&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp; </span></span></span><![endif]><span style='font-family:"Calibri",sans-serif; mso-ascii-theme-font:minor-latin;mso-hansi-theme-font:minor-latin;color:#1F4E79; mso-themecolor:accent1;mso-themeshade:128;mso-style-textfill-fill-color:#1F4E79; mso-style-textfill-fill-themecolor:accent1;mso-style-textfill-fill-alpha:100.0%; mso-style-textfill-fill-colortransforms:lumm=50000'><a href="#masters"><span style='mso-bidi-font-size:12.0pt;color:#1F4E79;mso-themecolor:accent1; mso-themeshade:128;mso-style-textfill-fill-color:#1F4E79;mso-style-textfill-fill-themecolor: accent1;mso-style-textfill-fill-alpha:100.0%;mso-style-textfill-fill-colortransforms: lumm=50000'>Computer Systems (M.S. Thesis research)</span></a></span><span style='color:#0000CC'>&nbsp;<span style='mso-tab-count:1'>    </span></span><span style='color:#1F4E79;mso-themecolor:accent1;mso-themeshade:128;mso-style-textfill-fill-color: #1F4E79;mso-style-textfill-fill-themecolor:accent1;mso-style-textfill-fill-alpha: 100.0%;mso-style-textfill-fill-colortransforms:lumm=50000'><o:p></o:p></span></p> <p class=MsoNormal><b style='mso-bidi-font-weight:normal'><span style='font-size:11.0pt;font-family:"Calibri",sans-serif;mso-ascii-theme-font: minor-latin;mso-hansi-theme-font:minor-latin'><o:p>&nbsp;</o:p></span></b></p> <p class=MsoNormal><a name=distributed><b style='mso-bidi-font-weight:normal'><span style='font-family:"Calibri",sans-serif;mso-ascii-theme-font:minor-latin; mso-hansi-theme-font:minor-latin'>Distributed System Testing and Verification</span></b></a><b style='mso-bidi-font-weight:normal'><span style='font-family:"Calibri",sans-serif; mso-ascii-theme-font:minor-latin;mso-hansi-theme-font:minor-latin'> <o:p></o:p></span></b></p> <p class=MsoListParagraphCxSpFirst style='text-indent:-.25in;mso-list:l0 level1 lfo2'><![if !supportLists]><span style='font-size:11.0pt;font-family:Symbol;mso-fareast-font-family:Symbol; mso-bidi-font-family:Symbol;color:#090000'><span style='mso-list:Ignore'>·<span style='font:7.0pt "Times New Roman"'>&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp; </span></span></span><![endif]><span style='font-size:11.0pt;font-family:"Calibri",sans-serif; mso-ascii-theme-font:minor-latin;mso-hansi-theme-font:minor-latin;color:#090000; background:white'>K. Li, P. Joshi, A. Gupta, and M. K. <span class=SpellE>Ganai</span>: <span class=SpellE>ReproLite</span>: A Lightweight Tool to Quickly Reproduce Hard System Bugs. In Proceedings of the ACM Symposium on Cloud Computing (<span class=SpellE>SoCC</span>), November 2014.<o:p></o:p></span></p> <p class=MsoListParagraphCxSpMiddle style='text-indent:-.25in;mso-list:l0 level1 lfo2'><![if !supportLists]><span style='font-size:11.0pt;font-family:Symbol;mso-fareast-font-family:Symbol; mso-bidi-font-family:Symbol;color:#090000'><span style='mso-list:Ignore'>·<span style='font:7.0pt "Times New Roman"'>&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp; </span></span></span><![endif]><span style='font-size:11.0pt;font-family:"Calibri",sans-serif; mso-ascii-theme-font:minor-latin;mso-hansi-theme-font:minor-latin;color:#090000; background:white'>S. Park, M. K. <span class=SpellE>Ganai</span>, and A. Gupta: PATRIOT: Runtime Checks for Permission Exploits in the Android System (<i style='mso-bidi-font-style:normal'>in submission</i>).<o:p></o:p></span></p> <p class=MsoListParagraphCxSpMiddle style='text-indent:-.25in;mso-list:l0 level1 lfo2'><![if !supportLists]><span style='font-size:11.0pt;font-family:Symbol;mso-fareast-font-family:Symbol; mso-bidi-font-family:Symbol;color:#090000'><span style='mso-list:Ignore'>·<span style='font:7.0pt "Times New Roman"'>&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp; </span></span></span><![endif]><span style='font-size:11.0pt;font-family:"Calibri",sans-serif; mso-ascii-theme-font:minor-latin;mso-hansi-theme-font:minor-latin;color:#090000; background:white'>Y. Lin, F. <span class=SpellE>Ivan i</span>, P. Joshi, G. <span class=SpellE>Balakrishnan</span>, M. K. <span class=SpellE>Ganai</span>, and A. Gupta: Environment-Sensitive Performance Tuning for Distributed Service Orchestration. In the Ninth International Workshop on Automatic Performance Tuning (<span class=SpellE>iWAPT</span>), June 2014.<o:p></o:p></span></p> <p class=MsoListParagraphCxSpMiddle style='text-indent:-.25in;mso-list:l0 level1 lfo2; tab-stops:.75in'><![if !supportLists]><span class=Title1><span style='font-family:Symbol;mso-fareast-font-family:Symbol;mso-bidi-font-family: Symbol;mso-fareast-language:JA'><span style='mso-list:Ignore'>·<span style='font:7.0pt "Times New Roman"'>&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp; </span></span></span></span><![endif]><span class=Title1><span style='font-size:11.0pt;font-family:"Calibri",sans-serif;mso-ascii-theme-font: minor-latin;mso-hansi-theme-font:minor-latin'>Y. Yuan, F. <span class=SpellE>Ivan i</span>, C. <span class=SpellE>Lumezanu</span>, S. Zhang, and A. Gupta: Generating Consistent Updates for Software-Defined Network Configurations. In Proceedings of the ACM SIGCOMM Workshop on Hot Topics in Software Defined Networking (<span class=SpellE>HotSDN</span>), June 2014 (poster paper).</span></span><span class=Title1><span style='mso-fareast-font-family:"MS Mincho";mso-fareast-language: JA'><o:p></o:p></span></span></p> <p class=MsoListParagraphCxSpMiddle style='text-indent:-.25in;mso-list:l0 level1 lfo2'><![if !supportLists]><span style='font-family:Symbol;mso-fareast-font-family:Symbol;mso-bidi-font-family: Symbol'><span style='mso-list:Ignore'>·<span style='font:7.0pt "Times New Roman"'>&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp; </span></span></span><![endif]><span style='font-size:11.0pt;font-family:"Calibri",sans-serif; mso-ascii-theme-font:minor-latin;mso-hansi-theme-font:minor-latin'>S. Zhang, <span class=Title1>F. <span class=SpellE>Ivan i</span>, C. <span class=SpellE>Lumezanu</span>, Y. Yuan, A. Gupta, and S. Malik: An Adaptable Rule Placement for Software-Defined Networks. In Proceedings of the IEEE/IFIP International Conference on Dependable Systems and Networks (DSN), June 2014.</span></span></p> <p class=MsoListParagraphCxSpMiddle style='text-indent:-.25in;mso-list:l0 level1 lfo2'><![if !supportLists]><span style='font-size:11.0pt;font-family:Symbol;mso-fareast-font-family:Symbol; mso-bidi-font-family:Symbol'><span style='mso-list:Ignore'>·<span style='font:7.0pt "Times New Roman"'>&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp; </span></span></span><![endif]><span style='font-size:11.0pt;font-family:"Calibri",sans-serif; mso-ascii-theme-font:minor-latin;mso-hansi-theme-font:minor-latin;color:#090000; background:white'>P. Joshi, M. K. <span class=SpellE>Ganai</span>, G. <span class=SpellE>Balakrishnan</span>, A. Gupta, and N. <span class=SpellE>Papakonstantinou</span>: <span class=SpellE>Setsudo</span>: Perturbation-based Testing Framework for Scalable Distributed Systems. In Proceedings of the Conference on Timely Results in Operating Systems (TRIOS), November 2013.</span><span style='font-size:11.0pt;font-family:"Calibri",sans-serif;mso-ascii-theme-font: minor-latin;mso-hansi-theme-font:minor-latin'><o:p></o:p></span></p> <p class=MsoListParagraphCxSpLast><span style='font-size:10.0pt;font-family: "Calibri",sans-serif;mso-ascii-theme-font:minor-latin;mso-hansi-theme-font: minor-latin'><o:p>&nbsp;</o:p></span></p> <p class=MsoNormal><a name=concurrency><b style='mso-bidi-font-weight:normal'><span style='font-family:"Calibri",sans-serif;mso-ascii-theme-font:minor-latin; mso-hansi-theme-font:minor-latin'>Concurren</span></b></a><a name="F_Soft_Project"></a><span style='mso-bookmark:concurrency'><b style='mso-bidi-font-weight:normal'><span style='font-family:"Calibri",sans-serif; mso-ascii-theme-font:minor-latin;mso-hansi-theme-font:minor-latin'>cy Verification<o:p></o:p></span></b></span></p> <span style='mso-bookmark:concurrency'></span> <p class=MsoListParagraph style='text-indent:-.25in;mso-list:l0 level1 lfo2; tab-stops:.75in'><![if !supportLists]><span class=Title1><span style='font-size:11.0pt;font-family:Symbol;mso-fareast-font-family:Symbol; mso-bidi-font-family:Symbol;mso-fareast-language:JA'><span style='mso-list: Ignore'>·<span style='font:7.0pt "Times New Roman"'>&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp; </span></span></span></span><![endif]><span class=Title1><span style='font-size:11.0pt;font-family:"Calibri",sans-serif;mso-ascii-theme-font: minor-latin;mso-hansi-theme-font:minor-latin'>A. Gupta, V. <span class=SpellE>Kahlon</span>, S. <span class=SpellE>Qadeer</span>, and T. <span class=SpellE>Touili</span>: Model Checking Concurrent Software. In Handbook of Model Checking, Springer (<i style='mso-bidi-font-style:normal'>invited paper</i>, <i style='mso-bidi-font-style: normal'>in final review</i>).</span></span><span class=Title1><span style='font-size:11.0pt;mso-fareast-font-family:"MS Mincho";mso-fareast-language: JA'><o:p></o:p></span></span></p> <p class=MsoNormal style='margin-left:.5in;text-indent:-.25in;mso-list:l0 level1 lfo2; tab-stops:.75in'><![if !supportLists]><span style='font-family:Symbol; mso-fareast-font-family:Symbol;mso-bidi-font-family:Symbol'><span style='mso-list:Ignore'>·<span style='font:7.0pt "Times New Roman"'>&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp; </span></span></span><![endif]><span class=Title1><span style='font-size:11.0pt; font-family:"Calibri",sans-serif;mso-ascii-theme-font:minor-latin;mso-hansi-theme-font: minor-latin'>V. <span class=SpellE>Kahlon</span>, S. <span class=SpellE>Sankaranarayanan</span>, and A. Gupta: Static Analysis for Concurrent Programs with Applications to Data Race Detection. Software Tools for Technology Transfer (STTT) 15(4): 321-336, 2013.</span></span><span style='font-size:11.0pt;font-family:"Calibri",sans-serif; mso-ascii-theme-font:minor-latin;mso-hansi-theme-font:minor-latin'> </span></p> <p class=MsoNormal style='margin-left:.5in;text-indent:-.25in;mso-list:l0 level1 lfo2; tab-stops:.75in'><![if !supportLists]><span style='font-size:11.0pt;font-family: Symbol;mso-fareast-font-family:Symbol;mso-bidi-font-family:Symbol;mso-fareast-language: JA'><span style='mso-list:Ignore'>·<span style='font:7.0pt "Times New Roman"'>&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp; </span></span></span><![endif]><span style='font-size:11.0pt;font-family:"Calibri",sans-serif; mso-ascii-theme-font:minor-latin;mso-hansi-theme-font:minor-latin'>N. <span class=SpellE>Razavi</span>, F. <span class=SpellE>Ivan i</span>, V. <span class=SpellE>Kahlon</span>, and A. Gupta: Concurrent Test Generation using <span class=SpellE>Concolic</span> Multi-Trace Analysis, In Proceedings of the Asian Symposium on Programming Languages and Systems (APLAS), December 2012.</span><span style='font-size:11.0pt;font-family:"Calibri",sans-serif;mso-ascii-theme-font: minor-latin;mso-fareast-font-family:"MS Mincho";mso-hansi-theme-font:minor-latin; mso-fareast-language:JA'><o:p></o:p></span></p> <p class=MsoNormal style='margin-left:.5in;text-indent:-.25in;mso-list:l0 level1 lfo2; tab-stops:.75in'><![if !supportLists]><span style='font-size:11.0pt;font-family: Symbol;mso-fareast-font-family:Symbol;mso-bidi-font-family:Symbol;mso-fareast-language: JA'><span style='mso-list:Ignore'>·<span style='font:7.0pt "Times New Roman"'>&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp; </span></span></span><![endif]><span style='font-size:11.0pt;font-family:"Calibri",sans-serif; mso-ascii-theme-font:minor-latin;mso-hansi-theme-font:minor-latin'><a href="http://www.informatik.uni-trier.de/%7Eley/pers/hd/g/Ganai:Malay_K=.html"><span style='mso-fareast-font-family:"Times New Roman";mso-fareast-theme-font:major-fareast; color:windowtext;text-decoration:none;text-underline:none'>M. K. <span class=SpellE>Ganai</span></span></a>, <a href="http://www.informatik.uni-trier.de/%7Eley/pers/hd/l/Lee:Dongyoon.html"><span style='mso-fareast-font-family:"Times New Roman";mso-fareast-theme-font:major-fareast; color:windowtext;text-decoration:none;text-underline:none'>D. Lee</span></a></span><span class=MsoHyperlink><span style='font-size:11.0pt;font-family:"Calibri",sans-serif; mso-ascii-theme-font:minor-latin;mso-fareast-font-family:"Times New Roman"; mso-fareast-theme-font:major-fareast;mso-hansi-theme-font:minor-latin; color:windowtext;text-decoration:none;text-underline:none'>, and A. Gupta: </span></span><span class=Title1><span style='font-size:11.0pt;font-family:"Calibri",sans-serif; mso-ascii-theme-font:minor-latin;mso-fareast-font-family:"Times New Roman"; mso-fareast-theme-font:major-fareast;mso-hansi-theme-font:minor-latin'>DTAM: Dynamic Taint Analysis of Multi-threaded Programs for Relevancy</span></span><span style='font-size:11.0pt;font-family:"Calibri",sans-serif;mso-ascii-theme-font: minor-latin;mso-hansi-theme-font:minor-latin'>. In ACM SIGSOFT Symposium on the Foundations of Software Engineering (FSE), November 2012.</span><span style='font-size:11.0pt;font-family:"Calibri",sans-serif;mso-ascii-theme-font: minor-latin;mso-fareast-font-family:"MS Mincho";mso-hansi-theme-font:minor-latin; mso-fareast-language:JA'><o:p></o:p></span></p> <p class=MsoNormal style='margin-left:.5in;text-indent:-.25in;mso-list:l0 level1 lfo2; tab-stops:.75in'><![if !supportLists]><span style='font-size:11.0pt;font-family: Symbol;mso-fareast-font-family:Symbol;mso-bidi-font-family:Symbol;mso-fareast-language: JA'><span style='mso-list:Ignore'>·<span style='font:7.0pt "Times New Roman"'>&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp; </span></span></span><![endif]><span class=main><span style='font-size:11.0pt; font-family:"Calibri",sans-serif;mso-ascii-theme-font:minor-latin;mso-fareast-font-family: "Times New Roman";mso-fareast-theme-font:major-fareast;mso-hansi-theme-font: minor-latin'>A. Sinha, S. Malik, and A. Gupta: Efficient Predictive Analysis for Detecting <span class=SpellE>Nondeterminism</span> in Multi-threaded Programs. In Proceedings of the International Conference on Computer-Aided Design (FMCAD), October 2012.</span></span><span style='font-size:11.0pt;font-family: "Calibri",sans-serif;mso-ascii-theme-font:minor-latin;mso-fareast-font-family: "MS Mincho";mso-hansi-theme-font:minor-latin;mso-fareast-language:JA'><o:p></o:p></span></p> <p class=MsoNormal style='margin-left:.5in;text-indent:-.25in;mso-list:l0 level1 lfo2; tab-stops:.75in'><![if !supportLists]><span style='font-size:11.0pt;font-family: Symbol;mso-fareast-font-family:Symbol;mso-bidi-font-family:Symbol;mso-fareast-language: JA'><span style='mso-list:Ignore'>·<span style='font:7.0pt "Times New Roman"'>&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp; </span></span></span><![endif]><span style='font-size:11.0pt;font-family:"Calibri",sans-serif; mso-ascii-theme-font:minor-latin;mso-hansi-theme-font:minor-latin'><a href="http://www.informatik.uni-trier.de/~ley/pers/hd/r/Ray:Sandip.html"><span style='mso-fareast-font-family:"Times New Roman";mso-fareast-theme-font:major-fareast; mso-bidi-font-family:Arial;color:windowtext;background:white;text-decoration: none;text-underline:none'>S. Ray</span></a></span><span style='font-size:11.0pt; font-family:"Calibri",sans-serif;mso-ascii-theme-font:minor-latin;mso-hansi-theme-font: minor-latin;mso-bidi-font-family:Arial;background:white'>,</span><span class=apple-converted-space><span style='font-size:11.0pt;font-family:"Calibri",sans-serif; mso-ascii-theme-font:minor-latin;mso-fareast-font-family:"Times New Roman"; mso-fareast-theme-font:major-fareast;mso-hansi-theme-font:minor-latin; mso-bidi-font-family:Arial;background:white'>&nbsp;</span></span><span style='font-size:11.0pt;font-family:"Calibri",sans-serif;mso-ascii-theme-font: minor-latin;mso-hansi-theme-font:minor-latin'><a href="http://www.informatik.uni-trier.de/~ley/pers/hd/b/Bhadra:Jayanta.html"><span style='mso-fareast-font-family:"Times New Roman";mso-fareast-theme-font:major-fareast; mso-bidi-font-family:Arial;color:windowtext;background:white;text-decoration: none;text-underline:none'>J. </span><span class=SpellE><span style='mso-fareast-font-family: "Times New Roman";mso-fareast-theme-font:major-fareast;color:windowtext; background:white;text-decoration:none;text-underline:none'>Bhadra</span></span></a></span><span style='font-size:11.0pt;font-family:"Calibri",sans-serif;mso-ascii-theme-font: minor-latin;mso-hansi-theme-font:minor-latin;mso-bidi-font-family:Arial; background:white'>,</span><span class=apple-converted-space><span style='font-size:11.0pt;font-family:"Calibri",sans-serif;mso-ascii-theme-font: minor-latin;mso-fareast-font-family:"Times New Roman";mso-fareast-theme-font: major-fareast;mso-hansi-theme-font:minor-latin;mso-bidi-font-family:Arial; background:white'>&nbsp;</span></span><span style='font-size:11.0pt;font-family: "Calibri",sans-serif;mso-ascii-theme-font:minor-latin;mso-hansi-theme-font: minor-latin'><a href="http://www.informatik.uni-trier.de/~ley/pers/hd/a/Abadir:Magdy_S=.html"><span style='mso-fareast-font-family:"Times New Roman";mso-fareast-theme-font:major-fareast; mso-bidi-font-family:Arial;color:windowtext;background:white;text-decoration: none;text-underline:none'>M. S. </span><span class=SpellE><span style='mso-fareast-font-family:"Times New Roman";mso-fareast-theme-font:major-fareast; color:windowtext;background:white;text-decoration:none;text-underline:none'>Abadir</span></span></a></span><span style='font-size:11.0pt;font-family:"Calibri",sans-serif;mso-ascii-theme-font: minor-latin;mso-hansi-theme-font:minor-latin;mso-bidi-font-family:Arial; background:white'>,</span><span class=apple-converted-space><span style='font-size:11.0pt;font-family:"Calibri",sans-serif;mso-ascii-theme-font: minor-latin;mso-fareast-font-family:"Times New Roman";mso-fareast-theme-font: major-fareast;mso-hansi-theme-font:minor-latin;mso-bidi-font-family:Arial; background:white'>&nbsp;</span></span><span style='font-size:11.0pt;font-family: "Calibri",sans-serif;mso-ascii-theme-font:minor-latin;mso-hansi-theme-font: minor-latin'><a href="http://www.informatik.uni-trier.de/~ley/pers/hd/w/Wang:Li=C=.html"><span style='mso-fareast-font-family:"Times New Roman";mso-fareast-theme-font:major-fareast; mso-bidi-font-family:Arial;color:windowtext;background:white;text-decoration: none;text-underline:none'>L-C. Wang</span></a></span><span style='font-size: 11.0pt;font-family:"Calibri",sans-serif;mso-ascii-theme-font:minor-latin; mso-hansi-theme-font:minor-latin;mso-bidi-font-family:Arial;background:white'>,</span><span class=apple-converted-space><span style='font-size:11.0pt;font-family:"Calibri",sans-serif; mso-ascii-theme-font:minor-latin;mso-fareast-font-family:"Times New Roman"; mso-fareast-theme-font:major-fareast;mso-hansi-theme-font:minor-latin; mso-bidi-font-family:Arial;background:white'>&nbsp;and </span></span><span class=this-person><span style='font-size:11.0pt;font-family:"Calibri",sans-serif; mso-ascii-theme-font:minor-latin;mso-hansi-theme-font:minor-latin;mso-bidi-font-family: Arial;background:white'>A. Gupta</span></span><span style='font-size:11.0pt; font-family:"Calibri",sans-serif;mso-ascii-theme-font:minor-latin;mso-hansi-theme-font: minor-latin;mso-bidi-font-family:Arial;background:white'>:</span><span class=apple-converted-space><span style='font-size:11.0pt;font-family:"Calibri",sans-serif; mso-ascii-theme-font:minor-latin;mso-fareast-font-family:"Times New Roman"; mso-fareast-theme-font:major-fareast;mso-hansi-theme-font:minor-latin; mso-bidi-font-family:Arial;background:white'>&nbsp;</span></span><span class=Title2><span style='font-size:11.0pt;font-family:"Calibri",sans-serif; mso-ascii-theme-font:minor-latin;mso-hansi-theme-font:minor-latin;mso-bidi-font-family: Arial;background:white;mso-bidi-font-weight:bold'>Introduction to Special Section on Verification Challenges in the Concurrent World.</span></span><span class=apple-converted-space><span style='font-size:11.0pt;font-family:"Calibri",sans-serif; mso-ascii-theme-font:minor-latin;mso-fareast-font-family:"Times New Roman"; mso-fareast-theme-font:major-fareast;mso-hansi-theme-font:minor-latin; mso-bidi-font-family:Arial;background:white'>&nbsp;</span></span><span style='font-size:11.0pt;font-family:"Calibri",sans-serif;mso-ascii-theme-font: minor-latin;mso-hansi-theme-font:minor-latin'><a href="http://www.informatik.uni-trier.de/~ley/db/journals/todaes/todaes17.html#RayBAWG12"><span style='mso-fareast-font-family:"Times New Roman";mso-fareast-theme-font:major-fareast; mso-bidi-font-family:Arial;color:windowtext;background:white;text-decoration: none;text-underline:none'>ACM Transactions on Design Automation of Electronic Systems 17</span></a></span><span style='font-size:11.0pt;font-family:"Calibri",sans-serif; mso-ascii-theme-font:minor-latin;mso-hansi-theme-font:minor-latin;mso-bidi-font-family: Arial;background:white'>(3): 19 (2012).</span><span style='font-size:11.0pt; font-family:"Calibri",sans-serif;mso-ascii-theme-font:minor-latin;mso-fareast-font-family: "MS Mincho";mso-hansi-theme-font:minor-latin;mso-fareast-language:JA'><o:p></o:p></span></p> <p class=MsoNormal style='margin-left:.5in;text-indent:-.25in;mso-list:l0 level1 lfo2; tab-stops:.75in'><![if !supportLists]><span style='font-size:11.0pt;font-family: Symbol;mso-fareast-font-family:Symbol;mso-bidi-font-family:Symbol;mso-fareast-language: JA'><span style='mso-list:Ignore'>·<span style='font:7.0pt "Times New Roman"'>&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp; </span></span></span><![endif]><span style='font-size:11.0pt;font-family:"Calibri",sans-serif; mso-ascii-theme-font:minor-latin;mso-hansi-theme-font:minor-latin'><a href="http://www.informatik.uni-trier.de/%7Eley/pers/hd/w/Wang:Chao.html"><span style='mso-fareast-font-family:"Times New Roman";mso-fareast-theme-font:major-fareast; color:windowtext;text-decoration:none;text-underline:none'>C. Wang</span></a>, <a href="http://www.informatik.uni-trier.de/%7Eley/pers/hd/k/Kundu:Sudipta.html"><span style='mso-fareast-font-family:"Times New Roman";mso-fareast-theme-font:major-fareast; color:windowtext;text-decoration:none;text-underline:none'>S. <span class=SpellE>Kundu</span></span></a>, <a href="http://www.informatik.uni-trier.de/%7Eley/pers/hd/l/Limaye:Rhishikesh.html"><span style='mso-fareast-font-family:"Times New Roman";mso-fareast-theme-font:major-fareast; color:windowtext;text-decoration:none;text-underline:none'>R. <span class=SpellE>Limaye</span></span></a>, <a href="http://www.informatik.uni-trier.de/%7Eley/pers/hd/g/Ganai:Malay_K=.html"><span style='mso-fareast-font-family:"Times New Roman";mso-fareast-theme-font:major-fareast; color:windowtext;text-decoration:none;text-underline:none'>M. K. <span class=SpellE>Ganai</span></span></a></span><span class=MsoHyperlink><span style='font-size:11.0pt;font-family:"Calibri",sans-serif;mso-ascii-theme-font: minor-latin;mso-fareast-font-family:"Times New Roman";mso-fareast-theme-font: major-fareast;mso-hansi-theme-font:minor-latin;color:windowtext;text-decoration: none;text-underline:none'>, and A. Gupta: </span></span><span class=Title1><span style='font-size:11.0pt;font-family:"Calibri",sans-serif;mso-ascii-theme-font: minor-latin;mso-fareast-font-family:"Times New Roman";mso-fareast-theme-font: major-fareast;mso-hansi-theme-font:minor-latin'>Symbolic Predictive Analysis for Concurrent Programs.</span></span><span style='font-size:11.0pt;font-family: "Calibri",sans-serif;mso-ascii-theme-font:minor-latin;mso-hansi-theme-font: minor-latin'> <a href="http://www.informatik.uni-trier.de/%7Eley/db/journals/fac/fac23.html#WangKLGG11"><span style='mso-fareast-font-family:"Times New Roman";mso-fareast-theme-font:major-fareast; color:windowtext;text-decoration:none;text-underline:none'>Formal Aspects of Computing 23</span></a>(6): 781-805 (2011).</span><span style='font-size:11.0pt; font-family:"Calibri",sans-serif;mso-ascii-theme-font:minor-latin;mso-fareast-font-family: "MS Mincho";mso-hansi-theme-font:minor-latin;mso-fareast-language:JA'><o:p></o:p></span></p> <p class=MsoNormal style='margin-left:.5in;text-indent:-.25in;mso-list:l0 level1 lfo2; tab-stops:.75in'><![if !supportLists]><span style='font-size:11.0pt;font-family: Symbol;mso-fareast-font-family:Symbol;mso-bidi-font-family:Symbol;mso-fareast-language: JA'><span style='mso-list:Ignore'>·<span style='font:7.0pt "Times New Roman"'>&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp; </span></span></span><![endif]><span style='font-size:11.0pt;font-family:"Calibri",sans-serif; mso-ascii-theme-font:minor-latin;mso-hansi-theme-font:minor-latin'>M. K. <span class=SpellE>Ganai</span>, N. Arora, C. Wang, A. Gupta, and G. <span class=SpellE>Balakrishnan</span>: BEST: A Symbolic Testing Tool for Predicting Multi-threaded Program Failures. In Proceedings of the <span style='mso-bidi-font-style: italic'>IEEE/ACM International Conference on Automated Software Engineering (ASE)</span>, November 2011. </span><span style='font-size:11.0pt;font-family: "Calibri",sans-serif;mso-ascii-theme-font:minor-latin;mso-fareast-font-family: "MS Mincho";mso-hansi-theme-font:minor-latin;mso-fareast-language:JA'><o:p></o:p></span></p> <p class=MsoNormal style='margin-left:.5in;text-indent:-.25in;mso-list:l0 level1 lfo2; tab-stops:.75in'><![if !supportLists]><span style='font-size:11.0pt;font-family: Symbol;mso-fareast-font-family:Symbol;mso-bidi-font-family:Symbol;mso-fareast-language: JA'><span style='mso-list:Ignore'>·<span style='font:7.0pt "Times New Roman"'>&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp; </span></span></span><![endif]><span style='font-size:11.0pt;font-family:"Calibri",sans-serif; mso-ascii-theme-font:minor-latin;mso-fareast-font-family:"MS Mincho"; mso-hansi-theme-font:minor-latin;mso-fareast-language:JA'>A. Sinha, S. Malik, C. Wang, and A. Gupta: Predicting <span class=SpellE>Serializability</span> Violations: SMT-based Search vs. DPOR-based Search, Haifa Verification Conference (HVC), <span class=GramE>December</span> 2011.<o:p></o:p></span></p> <p class=MsoNormal style='margin-left:.5in;text-indent:-.25in;mso-list:l0 level1 lfo2; tab-stops:.75in'><![if !supportLists]><span style='font-size:11.0pt;font-family: Symbol;mso-fareast-font-family:Symbol;mso-bidi-font-family:Symbol;mso-fareast-language: JA'><span style='mso-list:Ignore'>·<span style='font:7.0pt "Times New Roman"'>&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp; </span></span></span><![endif]><span class=Title1><span style='font-size:11.0pt; font-family:"Calibri",sans-serif;mso-ascii-theme-font:minor-latin;mso-fareast-font-family: "Times New Roman";mso-fareast-theme-font:major-fareast;mso-hansi-theme-font: minor-latin'>A. Gupta: Verifying Concurrent Programs: <span style='mso-bidi-font-style: italic'>Tutorial Talk</span>.</span></span><span style='font-size:11.0pt; font-family:"Calibri",sans-serif;mso-ascii-theme-font:minor-latin;mso-hansi-theme-font: minor-latin'> In Proceedings of the International Conference on Formal Methods in Computer-Aided Design (<a href="http://www.informatik.uni-trier.de/%7Eley/db/conf/fmcad/fmcad2011.html#Gupta11"><span style='mso-fareast-font-family:"Times New Roman";mso-fareast-theme-font:major-fareast; color:windowtext;text-decoration:none;text-underline:none'>FMCAD), October 2011</span></a>.</span><span style='font-size:11.0pt;font-family:"Calibri",sans-serif;mso-ascii-theme-font: minor-latin;mso-fareast-font-family:"MS Mincho";mso-hansi-theme-font:minor-latin; mso-fareast-language:JA'><o:p></o:p></span></p> <p class=MsoNormal style='margin-left:.5in;text-indent:-.25in;mso-list:l0 level1 lfo2; tab-stops:.75in'><![if !supportLists]><span style='font-size:11.0pt;font-family: Symbol;mso-fareast-font-family:Symbol;mso-bidi-font-family:Symbol;mso-fareast-language: JA'><span style='mso-list:Ignore'>·<span style='font:7.0pt "Times New Roman"'>&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp; </span></span></span><![endif]><span style='font-size:11.0pt;font-family:"Calibri",sans-serif; mso-ascii-theme-font:minor-latin;mso-hansi-theme-font:minor-latin'>A. Sinha, S. Malik, C. Wang, and A. Gupta: Predictive Analysis for Detecting <span class=SpellE>Serializability</span> Violations through Trace Segmentation. In Proceedings of the </span><em><span style='font-size:11.0pt;font-family:"Calibri",sans-serif; mso-ascii-theme-font:minor-latin;mso-fareast-font-family:"Times New Roman"; mso-fareast-theme-font:major-fareast;mso-hansi-theme-font:minor-latin'>ACM/IEEE International Conference on Formal Methods and Models for <span class=SpellE>Codesign</span> (MEMOCODE)</span></em><i style='mso-bidi-font-style:normal'><span style='font-size:11.0pt;font-family:"Calibri",sans-serif;mso-ascii-theme-font: minor-latin;mso-hansi-theme-font:minor-latin'>,</span></i><span style='font-size:11.0pt;font-family:"Calibri",sans-serif;mso-ascii-theme-font: minor-latin;mso-hansi-theme-font:minor-latin'> July 2011.</span><span style='font-size:11.0pt;font-family:"Calibri",sans-serif;mso-ascii-theme-font: minor-latin;mso-fareast-font-family:"MS Mincho";mso-hansi-theme-font:minor-latin; mso-fareast-language:JA'><o:p></o:p></span></p> <p class=MsoNormal style='margin-left:.5in;text-indent:-.25in;mso-list:l0 level1 lfo2; tab-stops:.75in'><![if !supportLists]><span style='font-size:11.0pt;font-family: Symbol;mso-fareast-font-family:Symbol;mso-bidi-font-family:Symbol;mso-fareast-language: JA'><span style='mso-list:Ignore'>·<span style='font:7.0pt "Times New Roman"'>&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp; </span></span></span><![endif]><span style='font-size:11.0pt;font-family:"Calibri",sans-serif; mso-ascii-theme-font:minor-latin;mso-hansi-theme-font:minor-latin'>C. Wang, M. Said, and A. Gupta: Coverage Guided Systematic Concurrency Testing. In Proceedings of the International Conference on Software Engineering (ICSE), May 2011.</span><span style='font-size:11.0pt;font-family:"Calibri",sans-serif; mso-ascii-theme-font:minor-latin;mso-fareast-font-family:"MS Mincho"; mso-hansi-theme-font:minor-latin;mso-fareast-language:JA'><o:p></o:p></span></p> <p class=MsoNormal style='margin-left:.5in;text-indent:-.25in;mso-list:l0 level1 lfo2; tab-stops:.75in'><![if !supportLists]><span style='font-size:11.0pt;font-family: Symbol;mso-fareast-font-family:Symbol;mso-bidi-font-family:Symbol;mso-fareast-language: JA'><span style='mso-list:Ignore'>·<span style='font:7.0pt "Times New Roman"'>&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp; </span></span></span><![endif]><span style='font-size:11.0pt;font-family:"Calibri",sans-serif; mso-ascii-theme-font:minor-latin;mso-hansi-theme-font:minor-latin'><a href="http://www.informatik.uni-trier.de/%7Eley/db/indices/a-tree/w/Wang:Chao.html"><span style='mso-fareast-font-family:"Times New Roman";mso-fareast-theme-font:major-fareast; color:windowtext;text-decoration:none;text-underline:none'>C. Wang</span></a>, <a href="http://www.informatik.uni-trier.de/%7Eley/db/indices/a-tree/l/Limaye:Rhishikesh.html"><span style='mso-fareast-font-family:"Times New Roman";mso-fareast-theme-font:major-fareast; color:windowtext;text-decoration:none;text-underline:none'>R.<span style='mso-spacerun:yes'>  </span><span class=SpellE>Limaye</span></span></a>, <a href="http://www.informatik.uni-trier.de/%7Eley/db/indices/a-tree/g/Ganai:Malay_K=.html"><span style='mso-fareast-font-family:"Times New Roman";mso-fareast-theme-font:major-fareast; color:windowtext;text-decoration:none;text-underline:none'>M. K. <span class=SpellE>Ganai</span></span></a></span><span class=MsoHyperlink><span style='font-size:11.0pt;font-family:"Calibri",sans-serif;mso-ascii-theme-font: minor-latin;mso-fareast-font-family:"Times New Roman";mso-fareast-theme-font: major-fareast;mso-hansi-theme-font:minor-latin;color:windowtext;text-decoration: none;text-underline:none'>, and A. Gupta: </span></span><span style='font-size: 11.0pt;font-family:"Calibri",sans-serif;mso-ascii-theme-font:minor-latin; mso-hansi-theme-font:minor-latin'>Trace-Based Symbolic Analysis for Atomicity Violations. In Proceedings of the International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), March 2010.</span><span style='font-size:11.0pt;font-family:"Calibri",sans-serif;mso-ascii-theme-font: minor-latin;mso-fareast-font-family:"MS Mincho";mso-hansi-theme-font:minor-latin; mso-fareast-language:JA'><o:p></o:p></span></p> <p class=MsoNormal style='margin-left:.5in;text-indent:-.25in;mso-list:l0 level1 lfo2; tab-stops:.75in'><![if !supportLists]><span style='font-size:11.0pt;font-family: Symbol;mso-fareast-font-family:Symbol;mso-bidi-font-family:Symbol;mso-fareast-language: JA'><span style='mso-list:Ignore'>·<span style='font:7.0pt "Times New Roman"'>&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp; </span></span></span><![endif]><span style='font-size:11.0pt;font-family:"Calibri",sans-serif; mso-ascii-theme-font:minor-latin;mso-hansi-theme-font:minor-latin'>C. Wang, S. <span class=SpellE>Kundu</span>, M. <span class=SpellE>Ganai</span>, and A. Gupta: Symbolic Predictive Analysis of Concurrent Programs. In Proceedings of the International Symposium on Formal Methods (FM), November 2009.</span><span style='font-size:11.0pt;font-family:"Calibri",sans-serif;mso-ascii-theme-font: minor-latin;mso-fareast-font-family:"MS Mincho";mso-hansi-theme-font:minor-latin; mso-fareast-language:JA'><o:p></o:p></span></p> <p class=MsoNormal style='margin-left:.5in;text-indent:-.25in;mso-list:l0 level1 lfo2; tab-stops:.75in'><![if !supportLists]><span style='font-size:11.0pt;font-family: Symbol;mso-fareast-font-family:Symbol;mso-bidi-font-family:Symbol;mso-fareast-language: JA'><span style='mso-list:Ignore'>·<span style='font:7.0pt "Times New Roman"'>&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp; </span></span></span><![endif]><span style='font-size:11.0pt;font-family:"Calibri",sans-serif; mso-ascii-theme-font:minor-latin;mso-hansi-theme-font:minor-latin'>C. Wang, S. Chaudhuri, A. Gupta, and Y. Yang: Symbolic Pruning of Concurrent Program Executions. In ACM SIGSOFT Symposium on the Foundations of Software Engineering (FSE), August 2009.</span><span style='font-size:11.0pt;font-family:"Calibri",sans-serif; mso-ascii-theme-font:minor-latin;mso-fareast-font-family:"MS Mincho"; mso-hansi-theme-font:minor-latin;mso-fareast-language:JA'><o:p></o:p></span></p> <p class=MsoNormal style='margin-left:.5in;text-indent:-.25in;mso-list:l0 level1 lfo2; tab-stops:.75in'><![if !supportLists]><span style='font-size:11.0pt;font-family: Symbol;mso-fareast-font-family:Symbol;mso-bidi-font-family:Symbol;mso-fareast-language: JA'><span style='mso-list:Ignore'>·<span style='font:7.0pt "Times New Roman"'>&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp; </span></span></span><![endif]><span style='font-size:11.0pt;font-family:"Calibri",sans-serif; mso-ascii-theme-font:minor-latin;mso-hansi-theme-font:minor-latin'>V. <span class=SpellE>Kahlon</span>, C. Wang, and A. Gupta: Monotonic Partial Order Reduction. In Proceedings of the International Conference on Computer Aided Verification (CAV), June 2009.</span><span style='font-size:11.0pt;font-family: "Calibri",sans-serif;mso-ascii-theme-font:minor-latin;mso-fareast-font-family: "MS Mincho";mso-hansi-theme-font:minor-latin;mso-fareast-language:JA'><o:p></o:p></span></p> <p class=MsoNormal style='margin-left:.5in;text-indent:-.25in;mso-list:l0 level1 lfo2; tab-stops:.75in'><![if !supportLists]><span style='font-size:11.0pt;font-family: Symbol;mso-fareast-font-family:Symbol;mso-bidi-font-family:Symbol;mso-fareast-language: JA'><span style='mso-list:Ignore'>·<span style='font:7.0pt "Times New Roman"'>&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp; </span></span></span><![endif]><span style='font-size:11.0pt;font-family:"Calibri",sans-serif; mso-ascii-theme-font:minor-latin;mso-hansi-theme-font:minor-latin'>V. <span class=SpellE>Kahlon</span>, S. <span class=SpellE>Sankaranarayanan</span>, and A. Gupta: Semantic Reduction of Thread <span class=SpellE>Interleavings</span> in Concurrent Programs. In Proceedings of the International Conference on </span><span style='font-size:11.0pt;font-family:"Calibri",sans-serif;mso-ascii-theme-font: minor-latin;mso-fareast-font-family:"Times New Roman";mso-fareast-theme-font: major-fareast;mso-hansi-theme-font:minor-latin;mso-bidi-font-family:Arial'>Tools and Algorithms for Construction and Analysis of Systems (</span><span style='font-size:11.0pt;font-family:"Calibri",sans-serif;mso-ascii-theme-font: minor-latin;mso-hansi-theme-font:minor-latin'>TACAS), March 2009.</span><span style='font-size:11.0pt;font-family:"Calibri",sans-serif;mso-ascii-theme-font: minor-latin;mso-fareast-font-family:"MS Mincho";mso-hansi-theme-font:minor-latin; mso-fareast-language:JA'><o:p></o:p></span></p> <p class=MsoNormal style='margin-left:.5in;text-indent:-.25in;mso-list:l0 level1 lfo2; tab-stops:.75in'><![if !supportLists]><span style='font-size:11.0pt;font-family: Symbol;mso-fareast-font-family:Symbol;mso-bidi-font-family:Symbol;mso-fareast-language: JA'><span style='mso-list:Ignore'>·<span style='font:7.0pt "Times New Roman"'>&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp; </span></span></span><![endif]><span style='font-size:11.0pt;font-family:"Calibri",sans-serif; mso-ascii-theme-font:minor-latin;mso-hansi-theme-font:minor-latin'>C. Wang, Y. Yang, A. Gupta, and G. <span class=SpellE>Gopalakrishnan</span>: Dynamic Model Checking with Property Driven Pruning to Detect Race Conditions. In Proceedings of the 6th International Symposium on Automated Technology for Verification and Analysis (ATVA), October 2008.</span><span style='font-size:11.0pt;font-family: "Calibri",sans-serif;mso-ascii-theme-font:minor-latin;mso-fareast-font-family: "MS Mincho";mso-hansi-theme-font:minor-latin;mso-fareast-language:JA'><o:p></o:p></span></p> <p class=MsoNormal style='margin-left:.5in;text-indent:-.25in;mso-list:l0 level1 lfo2; tab-stops:.75in'><![if !supportLists]><span style='font-size:11.0pt;font-family: Symbol;mso-fareast-font-family:Symbol;mso-bidi-font-family:Symbol;mso-fareast-language: JA'><span style='mso-list:Ignore'>·<span style='font:7.0pt "Times New Roman"'>&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp; </span></span></span><![endif]><span style='font-size:11.0pt;font-family:"Calibri",sans-serif; mso-ascii-theme-font:minor-latin;mso-fareast-font-family:"Times New Roman"; mso-fareast-theme-font:major-fareast;mso-hansi-theme-font:minor-latin; mso-bidi-font-family:Arial'>M. K. </span><span class=SpellE><span style='font-size:11.0pt;font-family:"Calibri",sans-serif;mso-ascii-theme-font: minor-latin;mso-fareast-font-family:"Times New Roman";mso-fareast-theme-font: major-fareast;mso-hansi-theme-font:minor-latin'>Ganai</span></span><span style='font-size:11.0pt;font-family:"Calibri",sans-serif;mso-ascii-theme-font: minor-latin;mso-fareast-font-family:"Times New Roman";mso-fareast-theme-font: major-fareast;mso-hansi-theme-font:minor-latin;mso-bidi-font-family:Arial'> and A. Gupta: Efficient Modeling of Concurrent Systems.</span><span style='font-size:11.0pt;font-family:"Calibri",sans-serif;mso-ascii-theme-font: minor-latin;mso-hansi-theme-font:minor-latin;mso-bidi-font-family:Arial'> In Proceedings of the International SPIN Workshop on Model Checking of Software (SPIN) August 2008.</span><span style='font-size:11.0pt;font-family:"Calibri",sans-serif; mso-ascii-theme-font:minor-latin;mso-fareast-font-family:"MS Mincho"; mso-hansi-theme-font:minor-latin;mso-fareast-language:JA'><o:p></o:p></span></p> <p class=MsoNormal style='margin-left:.5in;text-indent:-.25in;mso-list:l0 level1 lfo2; tab-stops:.75in'><![if !supportLists]><span style='font-size:11.0pt;font-family: Symbol;mso-fareast-font-family:Symbol;mso-bidi-font-family:Symbol;mso-fareast-language: JA'><span style='mso-list:Ignore'>·<span style='font:7.0pt "Times New Roman"'>&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp; </span></span></span><![endif]><span lang=DE style='font-size:11.0pt; font-family:"Calibri",sans-serif;mso-ascii-theme-font:minor-latin;mso-hansi-theme-font: minor-latin;mso-bidi-font-family:Arial;mso-ansi-language:DE'>C. Wang, Z. Yang, V. Kahlon</span><span style='font-size:11.0pt;font-family:"Calibri",sans-serif; mso-ascii-theme-font:minor-latin;mso-fareast-font-family:"Times New Roman"; mso-fareast-theme-font:major-fareast;mso-hansi-theme-font:minor-latin; mso-bidi-font-family:Arial'>, and A. Gupta: Peephole Partial Order Reduction.</span><span style='font-size:11.0pt;font-family:"Calibri",sans-serif;mso-ascii-theme-font: minor-latin;mso-hansi-theme-font:minor-latin;mso-bidi-font-family:Arial'> </span><span style='font-size:11.0pt;font-family:"Calibri",sans-serif;mso-ascii-theme-font: minor-latin;mso-fareast-font-family:"Times New Roman";mso-fareast-theme-font: major-fareast;mso-hansi-theme-font:minor-latin;mso-bidi-font-family:Arial'>In Proceedings of the International Conference on Tools and Algorithms for Construction and Analysis of Systems (TACAS), March 2008.</span><span style='font-size:11.0pt;font-family:"Calibri",sans-serif;mso-ascii-theme-font: minor-latin;mso-fareast-font-family:"MS Mincho";mso-hansi-theme-font:minor-latin; mso-fareast-language:JA'><o:p></o:p></span></p> <p class=MsoNormal style='margin-left:.5in;text-indent:-.25in;mso-list:l0 level1 lfo2; tab-stops:.75in'><![if !supportLists]><span style='font-size:11.0pt;font-family: Symbol;mso-fareast-font-family:Symbol;mso-bidi-font-family:Symbol;mso-fareast-language: JA'><span style='mso-list:Ignore'>·<span style='font:7.0pt "Times New Roman"'>&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp; </span></span></span><![endif]><span style='font-size:11.0pt;font-family:"Calibri",sans-serif; mso-ascii-theme-font:minor-latin;mso-hansi-theme-font:minor-latin'>V. <span class=SpellE>Kahlon</span>, Y. Yang, S. <span class=SpellE>Sankaranarayanan</span>, and A. Gupta: Fast and Accurate Static Race Detection for Concurrent Programs. In Proceedings of the International Conference on Computer Aided Verification (CAV), July 2007.</span><span style='font-size:11.0pt;font-family:"Calibri",sans-serif; mso-ascii-theme-font:minor-latin;mso-fareast-font-family:"MS Mincho"; mso-hansi-theme-font:minor-latin;mso-fareast-language:JA'><o:p></o:p></span></p> <p class=MsoNormal style='margin-left:.5in;text-indent:-.25in;mso-list:l0 level1 lfo2; tab-stops:.75in'><![if !supportLists]><span style='font-size:11.0pt;font-family: Symbol;mso-fareast-font-family:Symbol;mso-bidi-font-family:Symbol'><span style='mso-list:Ignore'>·<span style='font:7.0pt "Times New Roman"'>&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp; </span></span></span><![endif]><span style='font-size:11.0pt;font-family:"Calibri",sans-serif; mso-ascii-theme-font:minor-latin;mso-hansi-theme-font:minor-latin'>V. <span class=SpellE>Kahlon</span> and A. Gupta: On the Analysis of Interacting Pushdown Systems. In Proceedings of the Conference on Principles of Programming Languages (POPL), January 2007.<o:p></o:p></span></p> <p class=MsoNormal style='margin-left:.5in;text-indent:-.25in;mso-list:l0 level1 lfo2; tab-stops:.75in'><![if !supportLists]><span style='font-size:11.0pt;font-family: Symbol;mso-fareast-font-family:Symbol;mso-bidi-font-family:Symbol;mso-fareast-language: JA'><span style='mso-list:Ignore'>·<span style='font:7.0pt "Times New Roman"'>&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp; </span></span></span><![endif]><span style='font-size:11.0pt;font-family:"Calibri",sans-serif; mso-ascii-theme-font:minor-latin;mso-fareast-font-family:"MS Mincho"; mso-hansi-theme-font:minor-latin;mso-fareast-language:JA'>V. <span class=SpellE>Kahlon</span>, N. Sinha, and A. Gupta: Symbolic Model Checking of Concurrent Programs using Partial Orders and On-the-fly Transactions. In Proceedings of the International Conference on Computer Aided Verification (CAV), August 2006. <o:p></o:p></span></p> <p class=MsoNormal style='margin-left:.5in;text-indent:-.25in;mso-list:l0 level1 lfo2; tab-stops:.75in'><![if !supportLists]><span style='font-size:11.0pt;font-family: Symbol;mso-fareast-font-family:Symbol;mso-bidi-font-family:Symbol;mso-fareast-language: JA'><span style='mso-list:Ignore'>·<span style='font:7.0pt "Times New Roman"'>&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp; </span></span></span><![endif]><span style='font-size:11.0pt;font-family:"Calibri",sans-serif; mso-ascii-theme-font:minor-latin;mso-fareast-font-family:"MS Mincho"; mso-hansi-theme-font:minor-latin;mso-fareast-language:JA'>V. <span class=SpellE>Kahlon</span> and A. Gupta: An Automata-theoretic&nbsp;Approach for Model Checking Threads for LTL Properties. In Proceedings of the Conference on Logic in&nbsp;Computer Science (LICS), August 2006.&nbsp;<o:p></o:p></span></p> <p class=MsoNormal style='margin-left:.5in;text-indent:-.25in;mso-list:l0 level1 lfo2; tab-stops:list 58.5pt'><![if !supportLists]><span style='font-size:11.0pt; font-family:Symbol;mso-fareast-font-family:Symbol;mso-bidi-font-family:Symbol'><span style='mso-list:Ignore'>·<span style='font:7.0pt "Times New Roman"'>&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp; </span></span></span><![endif]><span style='font-size:11.0pt;font-family:"Calibri",sans-serif; mso-ascii-theme-font:minor-latin;mso-hansi-theme-font:minor-latin'>V. <span class=SpellE>Kahlon</span>, A. Gupta, and F. <span class=SpellE>Ivan i</span>: Reasoning about Threads Communicating via Locks. In Proceedings of the International Conference on Computer Aided Verification (CAV), July 2005.<o:p></o:p></span></p> <p class=MsoNormal style='margin-left:.25in'><span style='font-size:10.0pt; mso-bidi-font-size:12.0pt;font-family:"Calibri",sans-serif;mso-ascii-theme-font: minor-latin;mso-hansi-theme-font:minor-latin'><o:p>&nbsp;</o:p></span></p> <p class=MsoNormal><a name=program><b style='mso-bidi-font-weight:normal'><span style='font-family:"Calibri",sans-serif;mso-ascii-theme-font:minor-latin; mso-hansi-theme-font:minor-latin'>Program Analysis and Verification</span></b></a><b style='mso-bidi-font-weight:normal'><span style='font-family:"Calibri",sans-serif; mso-ascii-theme-font:minor-latin;mso-hansi-theme-font:minor-latin'> </span><span class=Title1><o:p></o:p></span></b></p> <p class=MsoNormal style='margin-left:.5in;text-indent:-.25in;mso-list:l0 level1 lfo2; tab-stops:.75in'><![if !supportLists]><span class=Title1><span style='font-size:11.0pt;font-family:Symbol;mso-fareast-font-family:Symbol; mso-bidi-font-family:Symbol;mso-fareast-language:JA'><span style='mso-list: Ignore'>·<span style='font:7.0pt "Times New Roman"'>&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp; </span></span></span></span><![endif]><span class=Title1><span style='font-size:11.0pt;font-family:"Calibri",sans-serif;mso-ascii-theme-font: minor-latin;mso-hansi-theme-font:minor-latin'>F. <span class=SpellE>Ivan i</span>, G. <span class=SpellE>Balakrishnan</span>, A. Gupta, S. <span class=SpellE>Sankaranarayanan</span>, N. Maeda, T. <span class=SpellE>Imoto</span>, R. <span class=SpellE>Pothengil</span>, M. Hussain: Scalable and Scope-Bounded Software Verification in <span class=SpellE>Varvel</span> (<i style='mso-bidi-font-style:normal'>Accepted for publication in the Journal of Automated Software Engineering, Springer, August 2014.</i>)</span></span><span class=Title1><span style='font-size:11.0pt; font-family:"Calibri",sans-serif;mso-ascii-theme-font:minor-latin;mso-fareast-font-family: "MS Mincho";mso-hansi-theme-font:minor-latin;mso-fareast-language:JA'><o:p></o:p></span></span></p> <p class=MsoNormal style='margin-left:.5in;text-indent:-.25in;mso-list:l0 level1 lfo2; tab-stops:.75in'><![if !supportLists]><span class=Title1><span style='font-size:11.0pt;font-family:Symbol;mso-fareast-font-family:Symbol; mso-bidi-font-family:Symbol;mso-fareast-language:JA'><span style='mso-list: Ignore'>·<span style='font:7.0pt "Times New Roman"'>&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp; </span></span></span></span><![endif]><span class=Title1><span style='font-size:11.0pt;font-family:"Calibri",sans-serif;mso-ascii-theme-font: minor-latin;mso-hansi-theme-font:minor-latin'>X. Xiao, G. <span class=SpellE>Balakrishan</span>, F. <span class=SpellE>Ivan i</span>, N. Maeda, and A. Gupta: ARC++: Effective <span class=SpellE>Typestate</span> and Lifetime Dependency Analysis. In Proceedings of the International Symposium on Software Testing and Analysis (ISSTA), July 2014.</span></span><span class=Title1><span style='font-size:11.0pt;font-family: "Calibri",sans-serif;mso-ascii-theme-font:minor-latin;mso-fareast-font-family: "MS Mincho";mso-hansi-theme-font:minor-latin;mso-fareast-language:JA'><o:p></o:p></span></span></p> <p class=MsoNormal style='margin-left:.5in;text-indent:-.25in;mso-list:l0 level1 lfo2; tab-stops:.75in'><![if !supportLists]><span style='font-family:Symbol; mso-fareast-font-family:Symbol;mso-bidi-font-family:Symbol;color:black; mso-themecolor:text1'><span style='mso-list:Ignore'>·<span style='font:7.0pt "Times New Roman"'>&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp; </span></span></span><![endif]><span class=Title1><span style='font-size:11.0pt; font-family:"Calibri",sans-serif;mso-ascii-theme-font:minor-latin;mso-hansi-theme-font: minor-latin;color:black;mso-themecolor:text1'>H. Abbas, G. E. <span class=SpellE>Fainekos</span>, S. <span class=SpellE>Sankaranarayanan</span>, F. <span class=SpellE>Ivan i</span>, and A. Gupta: Probabilistic Temporal Logic Falsification of Cyber-Physical Systems. </span></span><span style='font-size: 11.0pt;font-family:"Calibri",sans-serif;mso-ascii-theme-font:minor-latin; mso-hansi-theme-font:minor-latin'><a href="http://www.informatik.uni-trier.de/%7Eley/db/journals/tecs/tecs12.html#AbbasFSIG13"><span style='mso-fareast-font-family:"Times New Roman";mso-fareast-theme-font:major-fareast; color:black;mso-themecolor:text1'>ACM Transactions on Embedded Computing Systems 12</span></a><span style='color:black;mso-themecolor:text1'>(2s): 95, 2013.</span></span><span style='color:black;mso-themecolor:text1'><o:p></o:p></span></p> <p class=MsoNormal style='margin-left:.5in;text-indent:-.25in;mso-list:l0 level1 lfo2; tab-stops:.75in'><![if !supportLists]><span style='font-size:11.0pt;font-family: Symbol;mso-fareast-font-family:Symbol;mso-bidi-font-family:Symbol;mso-fareast-language: JA'><span style='mso-list:Ignore'>·<span style='font:7.0pt "Times New Roman"'>&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp; </span></span></span><![endif]><span style='font-size:11.0pt;font-family:"Calibri",sans-serif; mso-ascii-theme-font:minor-latin;mso-hansi-theme-font:minor-latin'>P. Garg, F. <span class=SpellE>Ivan i</span>, G. <span class=SpellE>Balakrishnan</span>, N. Maeda, and A. Gupta: Feedback-Directed Unit Test Generation for C/C++ using <span class=SpellE>Concolic</span> Execution. In Proceedings of the International Conference on Software Engineering (ICSE), May 2013.</span><span style='font-size:11.0pt;font-family:"Calibri",sans-serif;mso-ascii-theme-font: minor-latin;mso-fareast-font-family:"MS Mincho";mso-hansi-theme-font:minor-latin; mso-fareast-language:JA'><o:p></o:p></span></p> <p class=MsoNormal style='margin-left:.5in;text-indent:-.25in;mso-list:l0 level1 lfo2; tab-stops:.75in'><![if !supportLists]><span style='font-size:11.0pt;font-family: Symbol;mso-fareast-font-family:Symbol;mso-bidi-font-family:Symbol;mso-fareast-language: JA'><span style='mso-list:Ignore'>·<span style='font:7.0pt "Times New Roman"'>&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp; </span></span></span><![endif]><span style='font-size:11.0pt;font-family:"Calibri",sans-serif; mso-ascii-theme-font:minor-latin;mso-hansi-theme-font:minor-latin'><a href="http://www.informatik.uni-trier.de/%7Eley/pers/hd/g/Ghorbal:Khalil.html"><span style='mso-fareast-font-family:"Times New Roman";mso-fareast-theme-font:major-fareast; color:windowtext;text-decoration:none;text-underline:none'>K. <span class=SpellE>Ghorbal</span></span></a>, <a href="http://www.informatik.uni-trier.de/%7Eley/pers/hd/d/Duggirala:Parasara_Sridhar.html"><span style='mso-fareast-font-family:"Times New Roman";mso-fareast-theme-font:major-fareast; color:windowtext;text-decoration:none;text-underline:none'>P. S. <span class=SpellE>Duggirala</span></span></a>, <a href="http://www.informatik.uni-trier.de/%7Eley/pers/hd/k/Kahlon:Vineet.html"><span style='mso-fareast-font-family:"Times New Roman";mso-fareast-theme-font:major-fareast; color:windowtext;text-decoration:none;text-underline:none'>V. <span class=SpellE>Kahlon</span></span></a>, <a href="http://www.informatik.uni-trier.de/%7Eley/pers/hd/i/Ivancic:Franjo.html"><span style='mso-fareast-font-family:"Times New Roman";mso-fareast-theme-font:major-fareast; color:windowtext;text-decoration:none;text-underline:none'>F. <span class=SpellE>Ivan i</span></span></a></span><span class=MsoHyperlink><span style='font-size:11.0pt;font-family:"Calibri",sans-serif;mso-ascii-theme-font: minor-latin;mso-fareast-font-family:"Times New Roman";mso-fareast-theme-font: major-fareast;mso-hansi-theme-font:minor-latin;color:windowtext;text-decoration: none;text-underline:none'>, and A. Gupta: </span></span><span class=Title1><span style='font-size:11.0pt;font-family:"Calibri",sans-serif;mso-ascii-theme-font: minor-latin;mso-fareast-font-family:"Times New Roman";mso-fareast-theme-font: major-fareast;mso-hansi-theme-font:minor-latin'>Efficient Probabilistic Model Checking of Systems with Ranged Probabilities</span></span><span style='font-size:11.0pt;font-family:"Calibri",sans-serif;mso-ascii-theme-font: minor-latin;mso-hansi-theme-font:minor-latin'>. In the 6<sup>th</sup> International Workshop on Reachability Problems (RP), September 2012.</span><span style='font-size:11.0pt;font-family:"Calibri",sans-serif;mso-ascii-theme-font: minor-latin;mso-fareast-font-family:"MS Mincho";mso-hansi-theme-font:minor-latin; mso-fareast-language:JA'><o:p></o:p></span></p> <p class=MsoNormal style='margin-left:.5in;text-indent:-.25in;mso-list:l0 level1 lfo2; tab-stops:.75in'><![if !supportLists]><span style='font-size:11.0pt;font-family: Symbol;mso-fareast-font-family:Symbol;mso-bidi-font-family:Symbol;mso-fareast-language: JA'><span style='mso-list:Ignore'>·<span style='font:7.0pt "Times New Roman"'>&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp; </span></span></span><![endif]><span style='font-size:11.0pt;font-family:"Calibri",sans-serif; mso-ascii-theme-font:minor-latin;mso-hansi-theme-font:minor-latin'><a href="http://www.informatik.uni-trier.de/%7Eley/pers/hd/y/Yang_0003:Jing.html"><span style='mso-fareast-font-family:"Times New Roman";mso-fareast-theme-font:major-fareast; color:windowtext;text-decoration:none;text-underline:none'>J. Yang</span></a>, <a href="http://www.informatik.uni-trier.de/%7Eley/pers/hd/b/Balakrishnan:Gogul.html"><span style='mso-fareast-font-family:"Times New Roman";mso-fareast-theme-font:major-fareast; color:windowtext;text-decoration:none;text-underline:none'>G. <span class=SpellE>Balakrishnan</span></span></a>, <a href="http://www.informatik.uni-trier.de/%7Eley/pers/hd/m/Maeda:Naoto.html"><span style='mso-fareast-font-family:"Times New Roman";mso-fareast-theme-font:major-fareast; color:windowtext;text-decoration:none;text-underline:none'>N. Maeda</span></a>, <a href="http://www.informatik.uni-trier.de/%7Eley/pers/hd/i/Ivancic:Franjo.html"><span style='mso-fareast-font-family:"Times New Roman";mso-fareast-theme-font:major-fareast; color:windowtext;text-decoration:none;text-underline:none'>F. <span class=SpellE>Ivan i</span></span></a>, A. Gupta, <a href="http://www.informatik.uni-trier.de/%7Eley/pers/hd/s/Sinha:Nishant.html"><span style='mso-fareast-font-family:"Times New Roman";mso-fareast-theme-font:major-fareast; color:windowtext;text-decoration:none;text-underline:none'>N. Sinha</span></a>, <a href="http://www.informatik.uni-trier.de/%7Eley/pers/hd/s/Sankaranarayanan:Sriram.html"><span style='mso-fareast-font-family:"Times New Roman";mso-fareast-theme-font:major-fareast; color:windowtext;text-decoration:none;text-underline:none'>S. <span class=SpellE>Sankaranarayanan</span></span></a>, and <a href="http://www.informatik.uni-trier.de/%7Eley/pers/hd/s/Sharma:Naveen.html"><span style='mso-fareast-font-family:"Times New Roman";mso-fareast-theme-font:major-fareast; color:windowtext;text-decoration:none;text-underline:none'>N. Sharma</span></a></span><span class=MsoHyperlink><span style='font-size:11.0pt;font-family:"Calibri",sans-serif; mso-ascii-theme-font:minor-latin;mso-fareast-font-family:"Times New Roman"; mso-fareast-theme-font:major-fareast;mso-hansi-theme-font:minor-latin; color:windowtext;text-decoration:none;text-underline:none'>: </span></span><span class=Title1><span style='font-size:11.0pt;font-family:"Calibri",sans-serif; mso-ascii-theme-font:minor-latin;mso-fareast-font-family:"Times New Roman"; mso-fareast-theme-font:major-fareast;mso-hansi-theme-font:minor-latin'>Object Model Construction for Inheritance in C++ and Its Applications to Program Analysis</span></span><span style='font-size:11.0pt;font-family:"Calibri",sans-serif; mso-ascii-theme-font:minor-latin;mso-hansi-theme-font:minor-latin'>. In Proceedings of International Conference on Compiler Construction (CC), March 2012.</span><span style='font-size:11.0pt;font-family:"Calibri",sans-serif; mso-ascii-theme-font:minor-latin;mso-fareast-font-family:"MS Mincho"; mso-hansi-theme-font:minor-latin;mso-fareast-language:JA'><o:p></o:p></span></p> <p class=MsoNormal style='margin-left:.5in;text-indent:-.25in;mso-list:l0 level1 lfo2; tab-stops:.75in'><![if !supportLists]><span class=Title1><span style='font-family:Symbol;mso-fareast-font-family:Symbol;mso-bidi-font-family: Symbol'><span style='mso-list:Ignore'>·<span style='font:7.0pt "Times New Roman"'>&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp; </span></span></span></span><![endif]><span style='font-size:11.0pt;font-family: "Calibri",sans-serif;mso-ascii-theme-font:minor-latin;mso-hansi-theme-font: minor-latin'><a href="http://www.informatik.uni-trier.de/%7Eley/pers/hd/g/Ghorbal:Khalil.html"><span style='mso-fareast-font-family:"Times New Roman";mso-fareast-theme-font:major-fareast; color:windowtext;text-decoration:none;text-underline:none'>K. <span class=SpellE>Ghorbal</span></span></a>, <a href="http://www.informatik.uni-trier.de/%7Eley/pers/hd/i/Ivancic:Franjo.html"><span style='mso-fareast-font-family:"Times New Roman";mso-fareast-theme-font:major-fareast; color:windowtext;text-decoration:none;text-underline:none'>F. <span class=SpellE>Ivan i</span></span></a>, <a href="http://www.informatik.uni-trier.de/%7Eley/pers/hd/b/Balakrishnan:Gogul.html"><span style='mso-fareast-font-family:"Times New Roman";mso-fareast-theme-font:major-fareast; color:windowtext;text-decoration:none;text-underline:none'>G. <span class=SpellE>Balakrishnan</span></span></a>, <a href="http://www.informatik.uni-trier.de/%7Eley/pers/hd/m/Maeda:Naoto.html"><span style='mso-fareast-font-family:"Times New Roman";mso-fareast-theme-font:major-fareast; color:windowtext;text-decoration:none;text-underline:none'>N. Maeda</span></a></span><span class=MsoHyperlink><span style='font-size:11.0pt;font-family:"Calibri",sans-serif; mso-ascii-theme-font:minor-latin;mso-fareast-font-family:"Times New Roman"; mso-fareast-theme-font:major-fareast;mso-hansi-theme-font:minor-latin; color:windowtext;text-decoration:none;text-underline:none'>, and A. Gupta: </span></span><span class=Title1><span style='font-size:11.0pt;font-family:"Calibri",sans-serif; mso-ascii-theme-font:minor-latin;mso-fareast-font-family:"Times New Roman"; mso-fareast-theme-font:major-fareast;mso-hansi-theme-font:minor-latin'>Donut Domains: Efficient Non-convex Domains for Abstract Interpretation</span></span><span style='font-size:11.0pt;font-family:"Calibri",sans-serif;mso-ascii-theme-font: minor-latin;mso-hansi-theme-font:minor-latin'>. In Proceedings of the International Conference on Verification, Model Checking, and Abstract Interpretation (<a href="http://www.informatik.uni-trier.de/%7Eley/db/conf/vmcai/vmcai2012.html#GhorbalIBMG12"><span style='mso-fareast-font-family:"Times New Roman";mso-fareast-theme-font:major-fareast; color:windowtext;text-decoration:none;text-underline:none'>VMCAI), January 2012</span></a>.</span><span class=Title1><o:p></o:p></span></p> <p class=MsoNormal style='margin-left:.5in;text-indent:-.25in;mso-list:l0 level1 lfo2; tab-stops:.75in'><![if !supportLists]><span style='font-family:Symbol; mso-fareast-font-family:Symbol;mso-bidi-font-family:Symbol'><span style='mso-list:Ignore'>·<span style='font:7.0pt "Times New Roman"'>&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp; </span></span></span><![endif]><span style='font-size:11.0pt;font-family:"Calibri",sans-serif; mso-ascii-theme-font:minor-latin;mso-hansi-theme-font:minor-latin'>F. <span class=SpellE>Ivan i</span>, G.<span style='mso-spacerun:yes'>  </span><span class=SpellE>Balakrishnan</span>, A. Gupta, S. <span class=SpellE>Sankaranarayanan</span>, N. Maeda, H. <span class=SpellE>Tokuoka</span>, T. <span class=SpellE>Imoto</span>, and Y. Miyazaki<span style='mso-bidi-font-weight:bold'>: DC2: A Framework for Scalable, Scope-Bounded Software Verification</span>. In Proceedings of the <span style='mso-bidi-font-style:italic'>IEEE/ACM International Conference on Automated Software Engineering (ASE)</span>, November 2011. </span></p> <p class=MsoNormal style='margin-left:.5in;text-indent:-.25in;mso-list:l0 level1 lfo2; tab-stops:.75in'><![if !supportLists]><span style='font-size:11.0pt;font-family: Symbol;mso-fareast-font-family:Symbol;mso-bidi-font-family:Symbol;mso-fareast-language: JA'><span style='mso-list:Ignore'>·<span style='font:7.0pt "Times New Roman"'>&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp; </span></span></span><![endif]><span style='font-size:11.0pt;font-family:"Calibri",sans-serif; mso-ascii-theme-font:minor-latin;mso-hansi-theme-font:minor-latin'><a href="http://www.informatik.uni-trier.de/%7Eley/pers/hd/b/Balakrishnan:Gogul.html"><span style='mso-fareast-font-family:"Times New Roman";mso-fareast-theme-font:major-fareast; color:windowtext;text-decoration:none;text-underline:none'>G. <span class=SpellE>Balakrishnan</span></span></a>, <a href="http://www.informatik.uni-trier.de/%7Eley/pers/hd/m/Maeda:Naoto.html"><span style='mso-fareast-font-family:"Times New Roman";mso-fareast-theme-font:major-fareast; color:windowtext;text-decoration:none;text-underline:none'>N. Maeda</span></a>, <a href="http://www.informatik.uni-trier.de/%7Eley/pers/hd/s/Sankaranarayanan:Sriram.html"><span style='mso-fareast-font-family:"Times New Roman";mso-fareast-theme-font:major-fareast; color:windowtext;text-decoration:none;text-underline:none'>S. <span class=SpellE>Sankaranarayanan</span></span></a>, <a href="http://www.informatik.uni-trier.de/%7Eley/pers/hd/i/Ivancic:Franjo.html"><span style='mso-fareast-font-family:"Times New Roman";mso-fareast-theme-font:major-fareast; color:windowtext;text-decoration:none;text-underline:none'>F. </span></a><span style='mso-spacerun:yes'> </span><span class=SpellE>Ivan i</span>, A. Gupta, and <a href="http://www.informatik.uni-trier.de/%7Eley/pers/hd/p/Pothengil:Rakesh.html"><span style='mso-fareast-font-family:"Times New Roman";mso-fareast-theme-font:major-fareast; color:windowtext;text-decoration:none;text-underline:none'>R. <span class=SpellE>Pothengil</span></span></a></span><span class=MsoHyperlink><span style='font-size:11.0pt;font-family:"Calibri",sans-serif;mso-ascii-theme-font: minor-latin;mso-fareast-font-family:"Times New Roman";mso-fareast-theme-font: major-fareast;mso-hansi-theme-font:minor-latin;color:windowtext;text-decoration: none;text-underline:none'>: </span></span><span class=Title1><span style='font-size:11.0pt;font-family:"Calibri",sans-serif;mso-ascii-theme-font: minor-latin;mso-fareast-font-family:"Times New Roman";mso-fareast-theme-font: major-fareast;mso-hansi-theme-font:minor-latin'>Modeling and Analyzing the Interaction of C and C++ Strings</span></span><span style='font-size:11.0pt; font-family:"Calibri",sans-serif;mso-ascii-theme-font:minor-latin;mso-hansi-theme-font: minor-latin'>. In Proceedings of International Conference on Formal Verification of Object-Oriented Software (<span class=SpellE>FoVeOOS</span>), October 2011.</span><span style='font-size:11.0pt;font-family:"Calibri",sans-serif; mso-ascii-theme-font:minor-latin;mso-fareast-font-family:"MS Mincho"; mso-hansi-theme-font:minor-latin;mso-fareast-language:JA'><o:p></o:p></span></p> <p class=MsoNormal style='margin-left:.5in;text-indent:-.25in;mso-list:l0 level1 lfo2; tab-stops:.75in'><![if !supportLists]><span style='font-size:11.0pt;font-family: Symbol;mso-fareast-font-family:Symbol;mso-bidi-font-family:Symbol;mso-fareast-language: JA'><span style='mso-list:Ignore'>·<span style='font:7.0pt "Times New Roman"'>&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp; </span></span></span><![endif]><strong><span style='font-size:11.0pt; font-family:"Calibri",sans-serif;mso-ascii-theme-font:minor-latin;mso-fareast-font-family: "Times New Roman";mso-fareast-theme-font:major-fareast;mso-hansi-theme-font: minor-latin;font-weight:normal;mso-bidi-font-weight:bold'>P. <span class=SpellE>Prabhu</span>, N. Maeda, G. <span class=SpellE>Balakrishnan</span>,</span></strong><strong><span style='font-size:11.0pt;font-family:"Calibri",sans-serif;mso-ascii-theme-font: minor-latin;mso-fareast-font-family:"Times New Roman";mso-fareast-theme-font: major-fareast;mso-hansi-theme-font:minor-latin'> </span></strong><span style='font-size:11.0pt;font-family:"Calibri",sans-serif;mso-ascii-theme-font: minor-latin;mso-hansi-theme-font:minor-latin'>F. <span class=SpellE>Ivan i</span>, and A. Gupta:</span><strong><span style='font-size:11.0pt;font-family:"Calibri",sans-serif; mso-ascii-theme-font:minor-latin;mso-fareast-font-family:"Times New Roman"; mso-fareast-theme-font:major-fareast;mso-hansi-theme-font:minor-latin; font-weight:normal;mso-bidi-font-weight:bold'> <span class=SpellE>Interprocedural</span> Exception Analysis for C++</span></strong><span style='font-size:11.0pt; font-family:"Calibri",sans-serif;mso-ascii-theme-font:minor-latin;mso-hansi-theme-font: minor-latin'>. In Proceedings of the European Conference on Object-Oriented Programming (ECOOP), July 2011.</span><span style='font-size:11.0pt;font-family: "Calibri",sans-serif;mso-ascii-theme-font:minor-latin;mso-fareast-font-family: "MS Mincho";mso-hansi-theme-font:minor-latin;mso-fareast-language:JA'><o:p></o:p></span></p> <p class=MsoNormal style='margin-left:.5in;text-indent:-.25in;mso-list:l0 level1 lfo2; tab-stops:.75in'><![if !supportLists]><span style='font-size:11.0pt;font-family: Symbol;mso-fareast-font-family:Symbol;mso-bidi-font-family:Symbol;mso-fareast-language: JA'><span style='mso-list:Ignore'>·<span style='font:7.0pt "Times New Roman"'>&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp; </span></span></span><![endif]><span style='font-size:11.0pt;font-family:"Calibri",sans-serif; mso-ascii-theme-font:minor-latin;mso-hansi-theme-font:minor-latin'>F. <span class=SpellE>Ivan i</span>, M. K. <span class=SpellE>Ganai</span>, S. <span class=SpellE>Sankaranarayanan</span></span><strong><span style='font-size:11.0pt; font-family:"Calibri",sans-serif;mso-ascii-theme-font:minor-latin;mso-fareast-font-family: "Times New Roman";mso-fareast-theme-font:major-fareast;mso-hansi-theme-font: minor-latin;font-weight:normal;mso-bidi-font-weight:bold'>, and A. Gupta: Numerical Stability Analysis of Floating-point Computations using Software Model Checking</span></strong><b style='mso-bidi-font-weight:normal'><span style='font-size:11.0pt;font-family:"Calibri",sans-serif;mso-ascii-theme-font: minor-latin;mso-hansi-theme-font:minor-latin'>. </span></b><span style='font-size:11.0pt;font-family:"Calibri",sans-serif;mso-ascii-theme-font: minor-latin;mso-hansi-theme-font:minor-latin'>In Proceedings of the </span><em><span style='font-size:11.0pt;font-family:"Calibri",sans-serif;mso-ascii-theme-font: minor-latin;mso-fareast-font-family:"Times New Roman";mso-fareast-theme-font: major-fareast;mso-hansi-theme-font:minor-latin'>ACM/IEEE International Conference on Formal Methods and Models for <span class=SpellE>Codesign</span> (MEMOCODE)</span></em><i style='mso-bidi-font-style:normal'><span style='font-size:11.0pt;font-family: "Calibri",sans-serif;mso-ascii-theme-font:minor-latin;mso-hansi-theme-font: minor-latin'>,</span></i><span style='font-size:11.0pt;font-family:"Calibri",sans-serif; mso-ascii-theme-font:minor-latin;mso-hansi-theme-font:minor-latin'> July 2010. </span><span style='font-size:11.0pt;font-family:"Calibri",sans-serif;mso-ascii-theme-font: minor-latin;mso-fareast-font-family:"MS Mincho";mso-hansi-theme-font:minor-latin; mso-fareast-language:JA'><o:p></o:p></span></p> <p class=MsoNormal style='margin-left:.5in;text-indent:-.25in;mso-list:l0 level1 lfo2; tab-stops:.75in'><![if !supportLists]><span style='font-size:11.0pt;font-family: Symbol;mso-fareast-font-family:Symbol;mso-bidi-font-family:Symbol;mso-fareast-language: JA'><span style='mso-list:Ignore'>·<span style='font:7.0pt "Times New Roman"'>&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp; </span></span></span><![endif]><span style='font-size:11.0pt;font-family:"Calibri",sans-serif; mso-ascii-theme-font:minor-latin;mso-hansi-theme-font:minor-latin'><a href="http://www.informatik.uni-trier.de/%7Eley/db/indices/a-tree/n/Nghiem:Truong.html"><span style='mso-fareast-font-family:"Times New Roman";mso-fareast-theme-font:major-fareast; color:windowtext;text-decoration:none;text-underline:none'>T. Nghiem</span></a>, <a href="http://www.informatik.uni-trier.de/%7Eley/db/indices/a-tree/s/Sankaranarayanan:Sriram.html"><span style='mso-fareast-font-family:"Times New Roman";mso-fareast-theme-font:major-fareast; color:windowtext;text-decoration:none;text-underline:none'>S. <span class=SpellE>Sankaranarayanan</span></span></a>, <a href="http://www.informatik.uni-trier.de/%7Eley/db/indices/a-tree/f/Fainekos:Georgios_E=.html"><span style='mso-fareast-font-family:"Times New Roman";mso-fareast-theme-font:major-fareast; color:windowtext;text-decoration:none;text-underline:none'>G. E. <span class=SpellE>Fainekos</span></span></a>, <a href="http://www.informatik.uni-trier.de/%7Eley/db/indices/a-tree/i/Ivancic:Franjo.html"><span style='mso-fareast-font-family:"Times New Roman";mso-fareast-theme-font:major-fareast; color:windowtext;text-decoration:none;text-underline:none'>F. </span></a><span style='mso-spacerun:yes'> </span><span class=SpellE>Ivan i</span>, A. Gupta, and <a href="http://www.informatik.uni-trier.de/%7Eley/db/indices/a-tree/p/Pappas:George_J=.html"><span style='mso-fareast-font-family:"Times New Roman";mso-fareast-theme-font:major-fareast; color:windowtext;text-decoration:none;text-underline:none'>G. J. Pappas</span></a></span><span class=MsoHyperlink><span style='font-size:11.0pt;font-family:"Calibri",sans-serif; mso-ascii-theme-font:minor-latin;mso-fareast-font-family:"Times New Roman"; mso-fareast-theme-font:major-fareast;mso-hansi-theme-font:minor-latin; color:windowtext;text-decoration:none;text-underline:none'>: </span></span><span style='font-size:11.0pt;font-family:"Calibri",sans-serif;mso-ascii-theme-font: minor-latin;mso-hansi-theme-font:minor-latin'>Monte-Carlo techniques for falsification of temporal properties of non-linear hybrid systems. In Proceedings of the 13th ACM International Conference on Hybrid Systems: Computation and Control (HSCC), March 2010.</span><span style='font-size:11.0pt; font-family:"Calibri",sans-serif;mso-ascii-theme-font:minor-latin;mso-fareast-font-family: "MS Mincho";mso-hansi-theme-font:minor-latin;mso-fareast-language:JA'><o:p></o:p></span></p> <p class=MsoNormal style='margin-left:.5in;text-indent:-.25in;mso-list:l0 level1 lfo2; tab-stops:.75in'><![if !supportLists]><span style='font-size:11.0pt;font-family: Symbol;mso-fareast-font-family:Symbol;mso-bidi-font-family:Symbol;mso-fareast-language: JA'><span style='mso-list:Ignore'>·<span style='font:7.0pt "Times New Roman"'>&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp; </span></span></span><![endif]><span style='font-size:11.0pt;font-family:"Calibri",sans-serif; mso-ascii-theme-font:minor-latin;mso-hansi-theme-font:minor-latin;mso-bidi-font-weight: bold'>W. Harris, </span><span style='font-size:11.0pt;font-family:"Calibri",sans-serif; mso-ascii-theme-font:minor-latin;mso-hansi-theme-font:minor-latin'>S. <span class=SpellE>Sankaranarayanan</span>, F. <span class=SpellE>Ivan i</span><span style='mso-bidi-font-weight:bold'>, and A. Gupta: Program Analysis via <span class=SpellE>Satisfiability</span> <span class=GramE>Modulo</span> Path Programs</span>. In Proceedings of the ACM Symposium on Principles of Programming Languages (POPL), January 2010.</span><span style='font-size:11.0pt; font-family:"Calibri",sans-serif;mso-ascii-theme-font:minor-latin;mso-fareast-font-family: "MS Mincho";mso-hansi-theme-font:minor-latin;mso-fareast-language:JA'><o:p></o:p></span></p> <p class=MsoNormal style='margin-left:.5in;text-indent:-.25in;mso-list:l0 level1 lfo2; tab-stops:.75in'><![if !supportLists]><span style='font-size:11.0pt;font-family: Symbol;mso-fareast-font-family:Symbol;mso-bidi-font-family:Symbol;mso-fareast-language: JA'><span style='mso-list:Ignore'>·<span style='font:7.0pt "Times New Roman"'>&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp; </span></span></span><![endif]><span style='font-size:11.0pt;font-family:"Calibri",sans-serif; mso-ascii-theme-font:minor-latin;mso-hansi-theme-font:minor-latin'>G. <span class=SpellE>Fainekos</span>, S. <span class=SpellE>Sankaranarayanan</span>, F. <span class=SpellE>Ivan i</span>, and A. Gupta: Robustness of Model-based Simulations. In Proceedings of the </span><span class=smalltitle><span style='font-size:11.0pt;font-family:"Calibri",sans-serif;mso-ascii-theme-font: minor-latin;mso-fareast-font-family:"Times New Roman";mso-fareast-theme-font: major-fareast;mso-hansi-theme-font:minor-latin'>IEEE Real-Time Systems Symposium (RTSS), December 2009.</span></span><span style='font-size:11.0pt; font-family:"Calibri",sans-serif;mso-ascii-theme-font:minor-latin;mso-fareast-font-family: "MS Mincho";mso-hansi-theme-font:minor-latin;mso-fareast-language:JA'><o:p></o:p></span></p> <p class=MsoNormal style='margin-left:.5in;text-indent:-.25in;mso-list:l0 level1 lfo2; tab-stops:.75in'><![if !supportLists]><span style='font-size:11.0pt;font-family: Symbol;mso-fareast-font-family:Symbol;mso-bidi-font-family:Symbol;mso-fareast-language: JA'><span style='mso-list:Ignore'>·<span style='font:7.0pt "Times New Roman"'>&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp; </span></span></span><![endif]><span style='font-size:11.0pt;font-family:"Calibri",sans-serif; mso-ascii-theme-font:minor-latin;mso-hansi-theme-font:minor-latin'>G. <span class=SpellE>Balakrishnan</span>, S. <span class=SpellE>Sankaranarayanan</span>, F. <span class=SpellE>Ivan i</span>, and A. Gupta: Refining the Control Structure of Loops using Static Analysis. In Proceedings of the International Conference on Embedded Software (EMSOFT), October 2009.</span><span style='font-size:11.0pt;font-family:"Calibri",sans-serif;mso-ascii-theme-font: minor-latin;mso-fareast-font-family:"MS Mincho";mso-hansi-theme-font:minor-latin; mso-fareast-language:JA'><o:p></o:p></span></p> <p class=MsoNormal style='margin-left:.5in;text-indent:-.25in;mso-list:l0 level1 lfo2; tab-stops:.75in'><![if !supportLists]><span style='font-size:11.0pt;font-family: Symbol;mso-fareast-font-family:Symbol;mso-bidi-font-family:Symbol;mso-fareast-language: JA'><span style='mso-list:Ignore'>·<span style='font:7.0pt "Times New Roman"'>&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp; </span></span></span><![endif]><span style='font-size:11.0pt;font-family:"Calibri",sans-serif; mso-ascii-theme-font:minor-latin;mso-hansi-theme-font:minor-latin'>Z. Yang, C. Wang, F. <span class=SpellE>Ivan i</span>, and A. Gupta: Model Checking Sequential Software Programs via Mixed Symbolic Analysis. ACM Transactions on Design Automation of Electronic Systems 13(1), January 2009.</span><span style='font-size:11.0pt;font-family:"Calibri",sans-serif;mso-ascii-theme-font: minor-latin;mso-fareast-font-family:"MS Mincho";mso-hansi-theme-font:minor-latin; mso-fareast-language:JA'><o:p></o:p></span></p> <p class=MsoNormal style='margin-left:.5in;text-indent:-.25in;mso-list:l0 level1 lfo2; tab-stops:.75in'><![if !supportLists]><span style='font-size:11.0pt;font-family: Symbol;mso-fareast-font-family:Symbol;mso-bidi-font-family:Symbol;mso-fareast-language: JA'><span style='mso-list:Ignore'>·<span style='font:7.0pt "Times New Roman"'>&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp; </span></span></span><![endif]><span style='font-size:11.0pt;font-family:"Calibri",sans-serif; mso-ascii-theme-font:minor-latin;mso-hansi-theme-font:minor-latin'>F. Yu, C. Wang, A. Gupta, and T. <span class=SpellE>Bultan</span>: Modular Verification of Web Services using Efficient Symbolic Encoding and Summarization. In Proceedings of the ACM Foundations on Software Engineering (FSE), November 2008.</span><span style='font-size:11.0pt;font-family:"Calibri",sans-serif; mso-ascii-theme-font:minor-latin;mso-fareast-font-family:"MS Mincho"; mso-hansi-theme-font:minor-latin;mso-fareast-language:JA'><o:p></o:p></span></p> <p class=MsoNormal style='margin-left:.5in;text-indent:-.25in;mso-list:l0 level1 lfo2; tab-stops:.75in'><![if !supportLists]><span style='font-size:11.0pt;font-family: Symbol;mso-fareast-font-family:Symbol;mso-bidi-font-family:Symbol;mso-fareast-language: JA'><span style='mso-list:Ignore'>·<span style='font:7.0pt "Times New Roman"'>&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp; </span></span></span><![endif]><span style='font-size:11.0pt;font-family:"Calibri",sans-serif; mso-ascii-theme-font:minor-latin;mso-hansi-theme-font:minor-latin'>F. <span class=SpellE>Ivan i</span>, Z. Yang, M.K. <span class=SpellE>Ganai</span>, A. Gupta, and P. <span class=SpellE>Ashar</span>: Efficient SAT-based Bounded Model Checking for Software Verification.<span style='mso-spacerun:yes'>  </span>Journal on Theoretical Computer Science (TCS), Volume 404(3), September 2008.</span><span style='font-size:11.0pt;font-family:"Calibri",sans-serif; mso-ascii-theme-font:minor-latin;mso-fareast-font-family:"MS Mincho"; mso-hansi-theme-font:minor-latin;mso-fareast-language:JA'><o:p></o:p></span></p> <p class=MsoNormal style='margin-left:.5in;text-indent:-.25in;mso-list:l0 level1 lfo2; tab-stops:.75in'><![if !supportLists]><span style='font-size:11.0pt;font-family: Symbol;mso-fareast-font-family:Symbol;mso-bidi-font-family:Symbol;mso-fareast-language: JA'><span style='mso-list:Ignore'>·<span style='font:7.0pt "Times New Roman"'>&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp; </span></span></span><![endif]><span style='font-size:11.0pt;font-family:"Calibri",sans-serif; mso-ascii-theme-font:minor-latin;mso-hansi-theme-font:minor-latin'>A. <span class=SpellE>Zaks</span>, Z. Yang, I. <span class=SpellE>Shlyakhter</span>, F. <span class=SpellE>Ivan i</span>, S. <span class=SpellE>Cadambi</span>, M.K. <span class=SpellE>Ganai</span>, A. Gupta, and P. <span class=SpellE>Ashar</span>: <span class=SpellE>Bitwidth</span> Reduction via Symbolic Interval Analysis for Software Model Checking. Transactions Brief Paper in the IEEE Transactions on CAD, volume 27(8), Aug. 2008.</span><span style='font-size:11.0pt;font-family: "Calibri",sans-serif;mso-ascii-theme-font:minor-latin;mso-fareast-font-family: "MS Mincho";mso-hansi-theme-font:minor-latin;mso-fareast-language:JA'><o:p></o:p></span></p> <p class=MsoNormal style='margin-left:.5in;text-indent:-.25in;mso-list:l0 level1 lfo2; tab-stops:.75in'><![if !supportLists]><span style='font-size:11.0pt;font-family: Symbol;mso-fareast-font-family:Symbol;mso-bidi-font-family:Symbol;mso-fareast-language: JA'><span style='mso-list:Ignore'>·<span style='font:7.0pt "Times New Roman"'>&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp; </span></span></span><![endif]><span style='font-size:11.0pt;font-family:"Calibri",sans-serif; mso-ascii-theme-font:minor-latin;mso-hansi-theme-font:minor-latin;mso-bidi-font-family: Arial'>G. </span><span class=SpellE><span style='font-size:11.0pt;font-family: "Calibri",sans-serif;mso-ascii-theme-font:minor-latin;mso-hansi-theme-font: minor-latin'>Balakrishnan</span></span><span style='font-size:11.0pt; font-family:"Calibri",sans-serif;mso-ascii-theme-font:minor-latin;mso-hansi-theme-font: minor-latin;mso-bidi-font-family:Arial'>, S. </span><span class=SpellE><span style='font-size:11.0pt;font-family:"Calibri",sans-serif;mso-ascii-theme-font: minor-latin;mso-hansi-theme-font:minor-latin'>Sankaranarayanan</span></span><span style='font-size:11.0pt;font-family:"Calibri",sans-serif;mso-ascii-theme-font: minor-latin;mso-hansi-theme-font:minor-latin;mso-bidi-font-family:Arial'>, F. </span><span class=SpellE><span style='font-size:11.0pt;font-family:"Calibri",sans-serif; mso-ascii-theme-font:minor-latin;mso-hansi-theme-font:minor-latin'>Ivan i</span></span><span style='font-size:11.0pt;font-family:"Calibri",sans-serif;mso-ascii-theme-font: minor-latin;mso-hansi-theme-font:minor-latin;mso-bidi-font-family:Arial'>, O. Wei, and A. Gupta: SLR: Path-Sensitive Analysis </span><span style='font-size: 11.0pt;font-family:"Calibri",sans-serif;mso-ascii-theme-font:minor-latin; mso-fareast-font-family:"Times New Roman";mso-fareast-theme-font:major-fareast; mso-hansi-theme-font:minor-latin;mso-bidi-font-family:Arial'>through</span><span style='font-size:11.0pt;font-family:"Calibri",sans-serif;mso-ascii-theme-font: minor-latin;mso-hansi-theme-font:minor-latin;mso-bidi-font-family:Arial'> Infeasible-Path Detection and Syntactic-Language Refinement. </span><span style='font-size: 11.0pt;font-family:"Calibri",sans-serif;mso-ascii-theme-font:minor-latin; mso-fareast-font-family:"Times New Roman";mso-fareast-theme-font:major-fareast; mso-hansi-theme-font:minor-latin;mso-bidi-font-family:Arial'>In Proceedings of the Static Analysis Symposium (SAS), July 2008.</span><span style='font-size: 11.0pt;font-family:"Calibri",sans-serif;mso-ascii-theme-font:minor-latin; mso-fareast-font-family:"MS Mincho";mso-hansi-theme-font:minor-latin; mso-fareast-language:JA'><o:p></o:p></span></p> <p class=MsoNormal style='margin-left:.5in;text-indent:-.25in;mso-list:l0 level1 lfo2; tab-stops:.75in'><![if !supportLists]><span style='font-size:11.0pt;font-family: Symbol;mso-fareast-font-family:Symbol;mso-bidi-font-family:Symbol;mso-fareast-language: JA'><span style='mso-list:Ignore'>·<span style='font:7.0pt "Times New Roman"'>&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp; </span></span></span><![endif]><span style='font-size:11.0pt;font-family:"Calibri",sans-serif; mso-ascii-theme-font:minor-latin;mso-fareast-font-family:"Times New Roman"; mso-fareast-theme-font:major-fareast;mso-hansi-theme-font:minor-latin; mso-bidi-font-family:Arial'>S. </span><span class=SpellE><span style='font-size:11.0pt;font-family:"Calibri",sans-serif;mso-ascii-theme-font: minor-latin;mso-fareast-font-family:"Times New Roman";mso-fareast-theme-font: major-fareast;mso-hansi-theme-font:minor-latin'>Sankaranarayanan</span></span><span style='font-size:11.0pt;font-family:"Calibri",sans-serif;mso-ascii-theme-font: minor-latin;mso-fareast-font-family:"Times New Roman";mso-fareast-theme-font: major-fareast;mso-hansi-theme-font:minor-latin;mso-bidi-font-family:Arial'>, S. Chaudhuri, F. </span><span class=SpellE><span style='font-size:11.0pt; font-family:"Calibri",sans-serif;mso-ascii-theme-font:minor-latin;mso-fareast-font-family: "Times New Roman";mso-fareast-theme-font:major-fareast;mso-hansi-theme-font: minor-latin'>Ivan i</span></span><span style='font-size:11.0pt;font-family: "Calibri",sans-serif;mso-ascii-theme-font:minor-latin;mso-fareast-font-family: "Times New Roman";mso-fareast-theme-font:major-fareast;mso-hansi-theme-font: minor-latin;mso-bidi-font-family:Arial'>, and A. Gupta: Dynamic Inference of Likely Data Preconditions over Predicates by Tree Learning.</span><span style='font-size:11.0pt;font-family:"Calibri",sans-serif;mso-ascii-theme-font: minor-latin;mso-hansi-theme-font:minor-latin;mso-bidi-font-family:Arial'> In Proceedings of the International Symposium on Software Testing and Analysis (ISSTA), July 2008.</span><span style='font-size:11.0pt;font-family:"Calibri",sans-serif; mso-ascii-theme-font:minor-latin;mso-fareast-font-family:"MS Mincho"; mso-hansi-theme-font:minor-latin;mso-fareast-language:JA'><o:p></o:p></span></p> <p class=MsoNormal style='margin-left:.5in;text-indent:-.25in;mso-list:l0 level1 lfo2; tab-stops:.75in'><![if !supportLists]><span style='font-size:11.0pt;font-family: Symbol;mso-fareast-font-family:Symbol;mso-bidi-font-family:Symbol;mso-fareast-language: JA'><span style='mso-list:Ignore'>·<span style='font:7.0pt "Times New Roman"'>&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp; </span></span></span><![endif]><span style='font-size:11.0pt;font-family:"Calibri",sans-serif; mso-ascii-theme-font:minor-latin;mso-hansi-theme-font:minor-latin;mso-bidi-font-family: Arial'>S. </span><span class=SpellE><span style='font-size:11.0pt;font-family: "Calibri",sans-serif;mso-ascii-theme-font:minor-latin;mso-hansi-theme-font: minor-latin'>Sankaranarayanan</span></span><span style='font-size:11.0pt; font-family:"Calibri",sans-serif;mso-ascii-theme-font:minor-latin;mso-hansi-theme-font: minor-latin;mso-bidi-font-family:Arial'>, F. </span><span class=SpellE><span style='font-size:11.0pt;font-family:"Calibri",sans-serif;mso-ascii-theme-font: minor-latin;mso-hansi-theme-font:minor-latin'>Ivan i</span></span><span style='font-size:11.0pt;font-family:"Calibri",sans-serif;mso-ascii-theme-font: minor-latin;mso-hansi-theme-font:minor-latin;mso-bidi-font-family:Arial'> and A. Gupta: Mining Library Specifications Using Inductive Logic Programming. In Proceedings of the International Conference on Software Engineering (ICSE), May 2008.</span><span style='font-size:11.0pt;font-family:"Calibri",sans-serif;mso-ascii-theme-font: minor-latin;mso-fareast-font-family:"MS Mincho";mso-hansi-theme-font:minor-latin; mso-fareast-language:JA'><o:p></o:p></span></p> <p class=MsoNormal style='margin-left:.5in;text-indent:-.25in;mso-list:l0 level1 lfo2; tab-stops:.75in'><![if !supportLists]><span style='font-size:11.0pt;font-family: Symbol;mso-fareast-font-family:Symbol;mso-bidi-font-family:Symbol;mso-fareast-language: JA'><span style='mso-list:Ignore'>·<span style='font:7.0pt "Times New Roman"'>&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp; </span></span></span><![endif]><span style='font-size:11.0pt;font-family:"Calibri",sans-serif; mso-ascii-theme-font:minor-latin;mso-hansi-theme-font:minor-latin;mso-bidi-font-family: Arial'>M. K. </span><span class=SpellE><span style='font-size:11.0pt; font-family:"Calibri",sans-serif;mso-ascii-theme-font:minor-latin;mso-hansi-theme-font: minor-latin'>Ganai</span></span><span style='font-size:11.0pt;font-family:"Calibri",sans-serif; mso-ascii-theme-font:minor-latin;mso-hansi-theme-font:minor-latin;mso-bidi-font-family: Arial'> and A. Gupta: Tunneling and Slicing: Towards Scalable BMC. In Proceedings of the IEEE/ACM Design Automation Conference (DAC), June 2008.</span><span style='font-size:11.0pt;font-family:"Calibri",sans-serif;mso-ascii-theme-font: minor-latin;mso-fareast-font-family:"MS Mincho";mso-hansi-theme-font:minor-latin; mso-fareast-language:JA'><o:p></o:p></span></p> <ul style='margin-top:0in' type=disc> <li class=MsoNormal style='mso-list:l0 level1 lfo2'><span style='font-size: 11.0pt;font-family:"Calibri",sans-serif;mso-ascii-theme-font:minor-latin; mso-fareast-font-family:"Times New Roman";mso-fareast-theme-font:major-fareast; mso-hansi-theme-font:minor-latin;mso-bidi-font-family:Arial'>M. K. </span><span class=SpellE><span style='font-size:11.0pt;font-family:"Calibri",sans-serif; mso-ascii-theme-font:minor-latin;mso-fareast-font-family:"Times New Roman"; mso-fareast-theme-font:major-fareast;mso-hansi-theme-font:minor-latin'>Ganai</span></span><span style='font-size:11.0pt;font-family:"Calibri",sans-serif;mso-ascii-theme-font: minor-latin;mso-fareast-font-family:"Times New Roman";mso-fareast-theme-font: major-fareast;mso-hansi-theme-font:minor-latin;mso-bidi-font-family:Arial'> and A. Gupta: Completeness in SMT-based BMC for Software Programs.</span><span style='font-size:11.0pt;font-family:"Calibri",sans-serif;mso-ascii-theme-font: minor-latin;mso-hansi-theme-font:minor-latin;mso-bidi-font-family:Arial'> In Proceedings of the International Conference of Design, Automation and Test in Europe, March 2008.</span><span style='font-size:11.0pt; font-family:"Calibri",sans-serif;mso-ascii-theme-font:minor-latin; mso-hansi-theme-font:minor-latin'><o:p></o:p></span></li> </ul> <p class=MsoNormal style='margin-left:.5in;text-indent:-.25in;mso-list:l0 level1 lfo2; tab-stops:.75in'><![if !supportLists]><span style='font-size:11.0pt;font-family: Symbol;mso-fareast-font-family:Symbol;mso-bidi-font-family:Symbol;mso-fareast-language: JA'><span style='mso-list:Ignore'>·<span style='font:7.0pt "Times New Roman"'>&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp; </span></span></span><![endif]><span style='font-size:11.0pt;font-family:"Calibri",sans-serif; mso-ascii-theme-font:minor-latin;mso-fareast-font-family:"Times New Roman"; mso-fareast-theme-font:major-fareast;mso-hansi-theme-font:minor-latin; mso-bidi-font-family:Arial'>C. Wang, A. Gupta, and F. </span><span class=SpellE><span style='font-size:11.0pt;font-family:"Calibri",sans-serif; mso-ascii-theme-font:minor-latin;mso-fareast-font-family:"Times New Roman"; mso-fareast-theme-font:major-fareast;mso-hansi-theme-font:minor-latin'>Ivan i</span></span><span style='font-size:11.0pt;font-family:"Calibri",sans-serif;mso-ascii-theme-font: minor-latin;mso-fareast-font-family:"Times New Roman";mso-fareast-theme-font: major-fareast;mso-hansi-theme-font:minor-latin;mso-bidi-font-family:Arial'>: Induction in CEGAR for Detecting Counterexamples.</span><span style='font-size: 11.0pt;font-family:"Calibri",sans-serif;mso-ascii-theme-font:minor-latin; mso-hansi-theme-font:minor-latin;mso-bidi-font-family:Arial'> In Proceedings of the International Conference on Formal Methods in Computer Aided Design (FMCAD), November 2007.</span><span style='font-size:11.0pt;font-family:"Calibri",sans-serif; mso-ascii-theme-font:minor-latin;mso-fareast-font-family:"MS Mincho"; mso-hansi-theme-font:minor-latin;mso-fareast-language:JA'><o:p></o:p></span></p> <p class=MsoNormal style='margin-left:.5in;text-indent:-.25in;mso-list:l0 level1 lfo2; tab-stops:.75in'><![if !supportLists]><span style='font-size:11.0pt;font-family: Symbol;mso-fareast-font-family:Symbol;mso-bidi-font-family:Symbol;mso-fareast-language: JA'><span style='mso-list:Ignore'>·<span style='font:7.0pt "Times New Roman"'>&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp; </span></span></span><![endif]><span style='font-size:11.0pt;font-family:"Calibri",sans-serif; mso-ascii-theme-font:minor-latin;mso-hansi-theme-font:minor-latin'>S. <span class=SpellE>Sankaranarayanan</span>, F. <span class=SpellE>Ivan i</span>, and A. Gupta: Program Analysis using Symbolic Ranges. In Proceedings of the International Static Analysis Symposium (SAS), August 2007.</span><span style='font-size:11.0pt;font-family:"Calibri",sans-serif;mso-ascii-theme-font: minor-latin;mso-fareast-font-family:"MS Mincho";mso-hansi-theme-font:minor-latin; mso-fareast-language:JA'><o:p></o:p></span></p> <p class=MsoNormal style='margin-left:.5in;text-indent:-.25in;mso-list:l0 level1 lfo2; tab-stops:.75in'><![if !supportLists]><span style='font-size:11.0pt;font-family: Symbol;mso-fareast-font-family:Symbol;mso-bidi-font-family:Symbol'><span style='mso-list:Ignore'>·<span style='font:7.0pt "Times New Roman"'>&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp; </span></span></span><![endif]><span style='font-size:11.0pt;font-family:"Calibri",sans-serif; mso-ascii-theme-font:minor-latin;mso-hansi-theme-font:minor-latin'>C. Wang, Z. Yang, A. Gupta, and F. <span class=SpellE>Ivan i</span>: Using Counterexamples for Improving the Precision of Reachability Computation with <span class=SpellE>Polyhedra</span>. In Proceedings of the International Conference on Computer Aided Verification (CAV), July 2007.<o:p></o:p></span></p> <p class=MsoNormal style='margin-left:.5in;text-indent:-.25in;mso-list:l0 level1 lfo2; tab-stops:.75in'><![if !supportLists]><span style='font-size:11.0pt;font-family: Symbol;mso-fareast-font-family:Symbol;mso-bidi-font-family:Symbol;color:#1F4E79; mso-themecolor:accent1;mso-themeshade:128;mso-style-textfill-fill-color:#1F4E79; mso-style-textfill-fill-themecolor:accent1;mso-style-textfill-fill-alpha:100.0%; mso-style-textfill-fill-colortransforms:lumm=50000'><span style='mso-list:Ignore'>·<span style='font:7.0pt "Times New Roman"'>&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp; </span></span></span><![endif]><span style='font-size:11.0pt;font-family:"Calibri",sans-serif; mso-ascii-theme-font:minor-latin;mso-hansi-theme-font:minor-latin'>C. Wang, Z. Yang, F. <span class=SpellE>Ivan i</span>, and A. Gupta: Disjunctive Image Computation for Software Verification. ACM Transactions on Design Automation of Electronic Systems 12(2), April 2007. <i style='mso-bidi-font-style:normal'><u><span style='color:#1F4E79;mso-themecolor:accent1;mso-themeshade:128;mso-style-textfill-fill-color: #1F4E79;mso-style-textfill-fill-themecolor:accent1;mso-style-textfill-fill-alpha: 100.0%;mso-style-textfill-fill-colortransforms:lumm=50000'>Winner of the ACM TODAES 2008 Best Paper Award</span></u><span style='color:#1F4E79;mso-themecolor: accent1;mso-themeshade:128;mso-style-textfill-fill-color:#1F4E79;mso-style-textfill-fill-themecolor: accent1;mso-style-textfill-fill-alpha:100.0%;mso-style-textfill-fill-colortransforms: lumm=50000'>.</span></i><span style='color:#1F4E79;mso-themecolor:accent1; mso-themeshade:128;mso-style-textfill-fill-color:#1F4E79;mso-style-textfill-fill-themecolor: accent1;mso-style-textfill-fill-alpha:100.0%;mso-style-textfill-fill-colortransforms: lumm=50000'><o:p></o:p></span></span></p> <p class=MsoNormal style='margin-left:.5in;text-indent:-.25in;mso-list:l0 level1 lfo2; tab-stops:.75in'><![if !supportLists]><span style='font-size:11.0pt;font-family: Symbol;mso-fareast-font-family:Symbol;mso-bidi-font-family:Symbol'><span style='mso-list:Ignore'>·<span style='font:7.0pt "Times New Roman"'>&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp; </span></span></span><![endif]><span style='font-size:11.0pt;font-family:"Calibri",sans-serif; mso-ascii-theme-font:minor-latin;mso-hansi-theme-font:minor-latin'>C. Wang, Z. Yang, F. <span class=SpellE>Ivan i</span>, and A. Gupta: Whodunit? Causal Analysis for Counterexamples. In Proceedings of the International Symposium on Automated Technology for Verification and Analysis (ATVA), September 2006.<o:p></o:p></span></p> <p class=MsoNormal style='margin-left:.5in;text-indent:-.25in;mso-list:l0 level1 lfo2; tab-stops:.75in'><![if !supportLists]><span style='font-size:11.0pt;font-family: Symbol;mso-fareast-font-family:Symbol;mso-bidi-font-family:Symbol;mso-fareast-language: JA'><span style='mso-list:Ignore'>·<span style='font:7.0pt "Times New Roman"'>&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp; </span></span></span><![endif]><span style='font-size:11.0pt;font-family:"Calibri",sans-serif; mso-ascii-theme-font:minor-latin;mso-hansi-theme-font:minor-latin;color:black'>S. <span class=SpellE>Sankaranarayanan</span>, F. <span class=SpellE>Ivan i</span>, I. <span class=SpellE>Shlyakhter</span>, and A. Gupta: Static Analysis in Disjunctive Numerical Domains. In Proceedings of the International Static Analysis Symposium (SAS), August 2006.</span><span style='font-size:11.0pt; font-family:"Calibri",sans-serif;mso-ascii-theme-font:minor-latin;mso-fareast-font-family: "MS Mincho";mso-hansi-theme-font:minor-latin;mso-fareast-language:JA'><o:p></o:p></span></p> <p class=MsoNormal style='margin-left:.5in;text-indent:-.25in;mso-list:l0 level1 lfo2; tab-stops:.75in'><![if !supportLists]><span style='font-size:11.0pt;font-family: Symbol;mso-fareast-font-family:Symbol;mso-bidi-font-family:Symbol;mso-fareast-language: JA'><span style='mso-list:Ignore'>·<span style='font:7.0pt "Times New Roman"'>&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp; </span></span></span><![endif]><span style='font-size:11.0pt;font-family:"Calibri",sans-serif; mso-ascii-theme-font:minor-latin;mso-hansi-theme-font:minor-latin'>H. Jain, F. <span class=SpellE>Ivan i</span>, A. Gupta, I. <span class=SpellE>Shlyakhter</span>, and C. Wang<span style='color:black'>: Using Statically Computed Invariants inside the Predicate Abstraction and Refinement Loop</span>, In Proceedings of the International Conference on Computer Aided Verification (CAV), August 2006. </span><span style='font-size:11.0pt;font-family:"Calibri",sans-serif; mso-ascii-theme-font:minor-latin;mso-fareast-font-family:"MS Mincho"; mso-hansi-theme-font:minor-latin;mso-fareast-language:JA'><o:p></o:p></span></p> <p class=MsoNormal style='margin-left:.5in;text-indent:-.25in;mso-list:l0 level1 lfo2; tab-stops:.75in'><![if !supportLists]><span style='font-size:11.0pt;font-family: Symbol;mso-fareast-font-family:Symbol;mso-bidi-font-family:Symbol;mso-fareast-language: JA'><span style='mso-list:Ignore'>·<span style='font:7.0pt "Times New Roman"'>&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp; </span></span></span><![endif]><span style='font-size:11.0pt;font-family:"Calibri",sans-serif; mso-ascii-theme-font:minor-latin;mso-hansi-theme-font:minor-latin'>A. <span class=SpellE>Zaks</span>, I. <span class=SpellE>Shlyakhter</span>, F. <span class=SpellE>Ivan i</span>, S. <span class=SpellE>Cadambi</span>, Z. Yang, M. K. <span class=SpellE>Ganai</span>, A. Gupta, and P. <span class=SpellE>Ashar</span>: Using Range Analysis for Software Verification. In International Workshop on Software Verification and Validation (SVV), August 2006.</span><span style='font-size:11.0pt;font-family:"Calibri",sans-serif;mso-ascii-theme-font: minor-latin;mso-fareast-font-family:"MS Mincho";mso-hansi-theme-font:minor-latin; mso-fareast-language:JA'><o:p></o:p></span></p> <p class=MsoNormal style='margin-left:.5in;text-indent:-.25in;mso-list:l0 level1 lfo2; tab-stops:.75in'><![if !supportLists]><span style='font-size:11.0pt;font-family: Symbol;mso-fareast-font-family:Symbol;mso-bidi-font-family:Symbol;mso-fareast-language: JA'><span style='mso-list:Ignore'>·<span style='font:7.0pt "Times New Roman"'>&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp; </span></span></span><![endif]><span style='font-size:11.0pt;font-family:"Calibri",sans-serif; mso-ascii-theme-font:minor-latin;mso-hansi-theme-font:minor-latin'>Z. Yang, C. Wang, A. Gupta, and F. <span class=SpellE>Ivan i</span>. Mixed Symbolic Representations for Model Checking Software Programs. In Proceedings of the ACM-IEEE International Conference on Formal Methods and Models for <span class=SpellE>Codesign</span> (MEMOCODE), July 2006.</span><span style='font-size:11.0pt;font-family:"Calibri",sans-serif;mso-ascii-theme-font: minor-latin;mso-fareast-font-family:"MS Mincho";mso-hansi-theme-font:minor-latin; mso-fareast-language:JA'><o:p></o:p></span></p> <p class=MsoNormal style='margin-left:.5in;text-indent:-.25in;mso-list:l0 level1 lfo2; tab-stops:.75in'><![if !supportLists]><span style='font-size:11.0pt;font-family: Symbol;mso-fareast-font-family:Symbol;mso-bidi-font-family:Symbol;mso-fareast-language: JA'><span style='mso-list:Ignore'>·<span style='font:7.0pt "Times New Roman"'>&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp; </span></span></span><![endif]><span style='font-size:11.0pt;font-family:"Calibri",sans-serif; mso-ascii-theme-font:minor-latin;mso-fareast-font-family:"MS Mincho"; mso-hansi-theme-font:minor-latin;mso-fareast-language:JA'>C. Wang, Z. Yang, and F. <span class=SpellE>Ivan i</span>, and A. Gupta: Disjunctive Image Computation for Embedded Software Verification. IEEE Design Automation and Test Europe (DATE), March 2006. <o:p></o:p></span></p> <ul style='margin-top:0in' type=disc> <li class=MsoNormal style='mso-list:l0 level1 lfo2'><span style='font-size: 11.0pt;font-family:"Calibri",sans-serif;mso-ascii-theme-font:minor-latin; mso-hansi-theme-font:minor-latin'>F. <span class=SpellE>Ivan i</span>, I. <span class=SpellE>Shlyakhter</span>, M. <span class=SpellE>Ganai</span>, A. Gupta, V. <span class=SpellE>Kahlon</span>, C. Wang, and Z. Yang: Model Checking C Programs using F-Soft. Invited paper in the Proceedings of the IEEE International Conference on Computer Design (ICCD), October 2005.<o:p></o:p></span></li> <li class=MsoNormal style='mso-list:l0 level1 lfo2'><span style='font-size: 11.0pt;font-family:"Calibri",sans-serif;mso-ascii-theme-font:minor-latin; mso-hansi-theme-font:minor-latin'>F. <span class=SpellE>Ivan i</span>, Z. Yang, M. K. <span class=SpellE>Ganai</span>, A. Gupta, I. <span class=SpellE>Shlyakhter</span>, and P. <span class=SpellE>Ashar</span><span style='mso-bidi-font-weight:bold'>: F-Soft: Software Verification Platform</span>. In Proceedings of the International Conference on Computer Aided Verification (CAV), July 2005.<o:p></o:p></span></li> <li class=MsoNormal style='mso-list:l0 level1 lfo2'><span style='font-size: 11.0pt;font-family:"Calibri",sans-serif;mso-ascii-theme-font:minor-latin; mso-hansi-theme-font:minor-latin'>H. Jain, F. <span class=SpellE>Ivan i</span>, A. Gupta, and M. K. <span class=SpellE>Ganai</span><span style='mso-bidi-font-weight: bold'>: Localization and Register Sharing for Predicate Abstraction</span>. In Proceedings of Tools and Algorithms for Construction and Analysis of Systems (TACAS), April 2005. <o:p></o:p></span></li> <li class=MsoNormal style='mso-list:l0 level1 lfo2'><span style='font-size: 11.0pt;font-family:"Calibri",sans-serif;mso-ascii-theme-font:minor-latin; mso-hansi-theme-font:minor-latin'>F. <span class=SpellE>Ivan i</span>, Z. Yang, M. K. <span class=SpellE>Ganai</span>, A. Gupta, and P. <span class=SpellE>Ashar</span><span style='mso-bidi-font-weight:bold'>: Efficient SAT-based Bounded Model Checking for Software Verification</span>, in International Symposium on Leveraging Applications of Formal Methods (<span class=SpellE>ISoLA</span>), November 2004.</span><span style='font-size: 10.0pt;font-family:"Calibri",sans-serif;mso-ascii-theme-font:minor-latin; mso-hansi-theme-font:minor-latin'><o:p></o:p></span></li> </ul> <h2 style='margin-bottom:0in;margin-bottom:.0001pt;tab-stops:354.75pt'><a name=decisionproc><span style='font-size:12.0pt;font-family:"Calibri",sans-serif; mso-ascii-theme-font:minor-latin;mso-hansi-theme-font:minor-latin'>Automatic Decision Procedures</span></a><span style='font-size:12.0pt;font-family:"Calibri",sans-serif; mso-ascii-theme-font:minor-latin;mso-hansi-theme-font:minor-latin'> <span style='mso-tab-count:1'>                                                                </span><o:p></o:p></span></h2> <p class=MsoNormal style='margin-left:.5in;text-indent:-.25in;mso-list:l0 level1 lfo2; tab-stops:.75in'><![if !supportLists]><span style='font-size:11.0pt;font-family: Symbol;mso-fareast-font-family:Symbol;mso-bidi-font-family:Symbol;mso-fareast-language: JA'><span style='mso-list:Ignore'>·<span style='font:7.0pt "Times New Roman"'>&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp; </span></span></span><![endif]><span style='font-size:11.0pt;font-family:"Calibri",sans-serif; mso-ascii-theme-font:minor-latin;mso-hansi-theme-font:minor-latin'>S. <span class=GramE>Gao</span>, M. K. <span class=SpellE>Ganai</span>, F. <span class=SpellE>Ivan i</span>, A. Gupta, S. <span class=SpellE>Sankaranarayanan</span>, and E. M. Clarke</span><strong><span style='font-size:11.0pt;font-family:"Calibri",sans-serif; mso-ascii-theme-font:minor-latin;mso-fareast-font-family:"Times New Roman"; mso-fareast-theme-font:major-fareast;mso-hansi-theme-font:minor-latin'>: </span></strong><strong><span style='font-size:11.0pt;font-family:"Calibri",sans-serif;mso-ascii-theme-font: minor-latin;mso-fareast-font-family:"Times New Roman";mso-fareast-theme-font: major-fareast;mso-hansi-theme-font:minor-latin;font-weight:normal;mso-bidi-font-weight: bold'>Integrating ICP and LRA Solvers for Deciding Nonlinear Real Arithmetic Problems</span></strong><b style='mso-bidi-font-weight:normal'><span style='font-size:11.0pt;font-family:"Calibri",sans-serif;mso-ascii-theme-font: minor-latin;mso-hansi-theme-font:minor-latin'>.</span></b><span style='font-size:11.0pt;font-family:"Calibri",sans-serif;mso-ascii-theme-font: minor-latin;mso-hansi-theme-font:minor-latin'> In Proceedings of the International Conference on </span><em><span style='font-size:11.0pt; font-family:"Calibri",sans-serif;mso-ascii-theme-font:minor-latin;mso-fareast-font-family: "Times New Roman";mso-fareast-theme-font:major-fareast;mso-hansi-theme-font: minor-latin'>Formal Methods in Computer Aided Design (FMCAD)</span></em><i style='mso-bidi-font-style:normal'><span style='font-size:11.0pt;font-family: "Calibri",sans-serif;mso-ascii-theme-font:minor-latin;mso-hansi-theme-font: minor-latin'>,</span></i><span style='font-size:11.0pt;font-family:"Calibri",sans-serif; mso-ascii-theme-font:minor-latin;mso-hansi-theme-font:minor-latin'> October 2010. </span><span style='font-size:11.0pt;font-family:"Calibri",sans-serif; mso-ascii-theme-font:minor-latin;mso-fareast-font-family:"MS Mincho"; mso-hansi-theme-font:minor-latin;mso-fareast-language:JA'><o:p></o:p></span></p> <p class=MsoListParagraph style='text-indent:-.25in;mso-list:l0 level1 lfo2'><![if !supportLists]><span style='font-size:11.0pt;font-family:Symbol;mso-fareast-font-family:Symbol; mso-bidi-font-family:Symbol'><span style='mso-list:Ignore'>·<span style='font:7.0pt "Times New Roman"'>&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp; </span></span></span><![endif]><span style='font-size:11.0pt;font-family:"Calibri",sans-serif; mso-ascii-theme-font:minor-latin;mso-hansi-theme-font:minor-latin'>C. Wang, A. Gupta, and M. K. <span class=SpellE>Ganai</span>: Predicate Learning and Selective Theory Deduction for a Difference Logic Solver. In Proceedings of the ACM/IEEE Design Automation Conference (DAC), July 2006. <o:p></o:p></span></p> <ul style='margin-top:0in' type=disc> <li class=MsoNormal style='mso-list:l0 level1 lfo2'><span style='font-size: 11.0pt;font-family:"Calibri",sans-serif;mso-ascii-theme-font:minor-latin; mso-hansi-theme-font:minor-latin'>M. K. <span class=SpellE>Ganai</span>, M. <span class=SpellE>Talupur</span>, and A. Gupta: SDSAT: Tight Integration of Small Domain Encoding and Lazy Approaches in a Separation Logic Solver. In Proceedings of Tools and Algorithms for Construction and Analysis of Systems (TACAS), March 2006.<o:p></o:p></span></li> <li class=MsoNormal style='mso-list:l0 level1 lfo2'><span style='font-size: 11.0pt;font-family:"Calibri",sans-serif;mso-ascii-theme-font:minor-latin; mso-hansi-theme-font:minor-latin'>C. Wang, F. <span class=SpellE>Ivan i</span>, M. K. <span class=SpellE>Ganai</span>, and A. Gupta: Deciding Separation Logic formulae by SAT and Incremental Negative Cycle Elimination, In Proceedings of International Conference on Logic for Artificial Intelligence and Reasoning (LPAR), December 2005.<o:p></o:p></span></li> <li class=MsoNormal style='mso-list:l0 level1 lfo2'><span style='font-size: 11.0pt;font-family:"Calibri",sans-serif;mso-ascii-theme-font:minor-latin; mso-hansi-theme-font:minor-latin'>M. K. <span class=SpellE>Ganai</span>, L. Zhang, A. Gupta, P. <span class=SpellE>Ashar</span>, and S. Malik: Combining Strengths of Circuit-based and CNF-based Algorithms for a High-performance SAT Solver. In Proceedings of the ACM/IEEE Design Automation Conference (DAC), June 2002.<o:p></o:p></span></li> </ul> <h2 style='margin-bottom:0in;margin-bottom:.0001pt'><a name=eda><span style='font-size:12.0pt;font-family:"Calibri",sans-serif;mso-ascii-theme-font: minor-latin;mso-hansi-theme-font:minor-latin'>Verification in Electronic Design Automation<o:p></o:p></span></a></h2> <span style='mso-bookmark:eda'></span> <ul style='margin-top:0in' type=disc> <li class=MsoNormal style='mso-list:l0 level1 lfo2'><span style='font-size: 11.0pt;font-family:"Calibri",sans-serif;mso-ascii-theme-font:minor-latin; mso-fareast-font-family:"Times New Roman";mso-fareast-theme-font:major-fareast; mso-hansi-theme-font:minor-latin;mso-bidi-font-family:Arial'>C. Wang, H. Kim, and A. Gupta: Hybrid CEGAR: Combining Variable Hiding and Predicate Abstraction.</span><span style='font-size:11.0pt;font-family:"Calibri",sans-serif; mso-ascii-theme-font:minor-latin;mso-hansi-theme-font:minor-latin; mso-bidi-font-family:Arial'> In Proceedings of the International Conference on Computer Aided Design (ICCAD), November 2007.</span><span style='font-size:11.0pt;font-family:"Calibri",sans-serif;mso-ascii-theme-font: minor-latin;mso-hansi-theme-font:minor-latin'><o:p></o:p></span></li> <li class=MsoNormal style='mso-list:l0 level1 lfo2'><span style='font-size: 11.0pt;font-family:"Calibri",sans-serif;mso-ascii-theme-font:minor-latin; mso-fareast-font-family:"MS Mincho";mso-hansi-theme-font:minor-latin; mso-fareast-language:JA'>M. K. <span class=SpellE>Ganai</span> and A. Gupta: Efficient BMC for Multi-clock Systems with Clocked Specifications. In Proceedings of Asia and South Pacific Design Automation Conference (ASP-DAC), January 2007. </span><span style='font-size:11.0pt;font-family:"Calibri",sans-serif; mso-ascii-theme-font:minor-latin;mso-hansi-theme-font:minor-latin'><o:p></o:p></span></li> <li class=MsoNormal style='mso-list:l0 level1 lfo2'><span style='font-size: 11.0pt;font-family:"Calibri",sans-serif;mso-ascii-theme-font:minor-latin; mso-fareast-font-family:"MS Mincho";mso-hansi-theme-font:minor-latin; mso-fareast-language:JA'>M. K. <span class=SpellE>Ganai</span>, A. Gupta, A. <span class=SpellE>Mukaiyama</span>, and K. Wakabayashi: Synthesizing  Verification Aware Models: How and Why? In Proceedings of the IEEE VLSI Design Conference, January 2007.</span><span style='font-size:11.0pt; font-family:"Calibri",sans-serif;mso-ascii-theme-font:minor-latin; mso-hansi-theme-font:minor-latin'><o:p></o:p></span></li> <li class=MsoNormal style='mso-list:l0 level1 lfo2'><span style='font-size: 11.0pt;font-family:"Calibri",sans-serif;mso-ascii-theme-font:minor-latin; mso-fareast-font-family:"MS Mincho";mso-hansi-theme-font:minor-latin; mso-fareast-language:JA'>M. K. <span class=SpellE>Ganai</span> and A. Gupta: Accelerating High-level Bounded Model Checking. In Proceedings of the IEEE International Conference on Computer-Aided Design (ICCAD), November 2006.</span><span style='font-size:11.0pt;font-family:"Calibri",sans-serif; mso-ascii-theme-font:minor-latin;mso-hansi-theme-font:minor-latin'><o:p></o:p></span></li> <li class=MsoNormal style='mso-list:l0 level1 lfo2'><span style='font-size: 11.0pt;font-family:"Calibri",sans-serif;mso-ascii-theme-font:minor-latin; mso-hansi-theme-font:minor-latin'>A. Gupta, M. K. <span class=SpellE>Ganai</span> and C. Wang: SAT-Based Verification Methods and Applications in Hardware Verification. In the International School on Formal Methods for the Design of Computer, Communication and Software Systems: Hardware Verification, <span class=SpellE>Bertinoro</span>, <span class=GramE>May</span> 2006.<o:p></o:p></span></li> <li class=MsoNormal style='mso-list:l0 level1 lfo2'><span style='font-size: 11.0pt;font-family:"Calibri",sans-serif;mso-ascii-theme-font:minor-latin; mso-hansi-theme-font:minor-latin'>D. Tang, S. Malik, A. Gupta, and C. N. <span class=SpellE>Ip</span><span style='mso-bidi-font-weight:bold'>: Symmetry Reduction in SAT-based Model Checking</span>. In Proceedings of International Conference on Computer Aided Verification (CAV), July 2005.<o:p></o:p></span></li> <li class=MsoNormal style='mso-list:l0 level1 lfo2'><span style='font-size: 11.0pt;font-family:"Calibri",sans-serif;mso-ascii-theme-font:minor-latin; mso-hansi-theme-font:minor-latin'>M. K. <span class=SpellE>Ganai</span>, A. Gupta, and P. <span class=SpellE>Ashar</span>: Beyond<span style='mso-bidi-font-weight:bold'> Safety: Customized SAT-based Model Checking</span>. In Proceedings of the ACM/IEEE Design Automation Conference (DAC), June 2005.<o:p></o:p></span></li> <li class=MsoNormal style='mso-list:l0 level1 lfo2'><span style='font-size: 11.0pt;font-family:"Calibri",sans-serif;mso-ascii-theme-font:minor-latin; mso-hansi-theme-font:minor-latin'>M. K. <span class=SpellE>Ganai</span>, A. Gupta, and P. <span class=SpellE>Ashar</span><span style='mso-bidi-font-weight: bold'>: <span class=SpellE>DiVer</span>: SAT-based Model Checking Platform for Large Scale Systems</span>. In Proceedings of Tools and Algorithms for Construction and Analysis of Systems (TACAS), April<i> </i>2005<i>. </i><o:p></o:p></span></li> <li class=MsoNormal style='mso-list:l0 level1 lfo2'><span style='font-size: 11.0pt;font-family:"Calibri",sans-serif;mso-ascii-theme-font:minor-latin; mso-hansi-theme-font:minor-latin'>M. K. <span class=SpellE>Ganai</span>, A. Gupta, and P. <span class=SpellE>Ashar</span><span style='mso-bidi-font-weight: bold'>: Verification of Embedded Memory Systems using Efficient Memory Modeling</span>.<span style='mso-bidi-font-weight:bold'> </span>In Proceedings of<span style='mso-bidi-font-weight:bold'> the IEEE Design Automation and Test Europe (</span>DATE), March 2005. <o:p></o:p></span></li> <li class=MsoNormal style='mso-list:l0 level1 lfo2'><span style='font-size: 11.0pt;font-family:"Calibri",sans-serif;mso-ascii-theme-font:minor-latin; mso-hansi-theme-font:minor-latin'>M. R. Prasad, A. <span class=SpellE>Biere</span>, and A. Gupta: A Survey of Recent Advances in SAT-based Verification. In <span style='color:black'>International Journal on Software Tools for Technology Transfer (STTT), Vol. 7(2):156 173, April 2005</span>.<o:p></o:p></span></li> <li class=MsoNormal style='mso-list:l0 level1 lfo2'><span style='font-size: 11.0pt;font-family:"Calibri",sans-serif;mso-ascii-theme-font:minor-latin; mso-hansi-theme-font:minor-latin;mso-bidi-font-weight:bold'>A. Gupta, </span><span style='font-size:11.0pt;font-family:"Calibri",sans-serif;mso-ascii-theme-font: minor-latin;mso-hansi-theme-font:minor-latin'>M. K. <span class=SpellE>Ganai</span>, and P. <span class=SpellE>Ashar</span><span style='mso-bidi-font-weight: bold'>: Lazy Constraints and SAT Heuristics for Proof-based Abstraction</span>. In Proceedings of the IEEE International Conference on VLSI Design, January 2005. <o:p></o:p></span></li> <li class=MsoNormal style='mso-list:l0 level1 lfo2'><span style='font-size: 11.0pt;font-family:"Calibri",sans-serif;mso-ascii-theme-font:minor-latin; mso-hansi-theme-font:minor-latin'>M. K. <span class=SpellE>Ganai</span>, A. Gupta, and P. <span class=SpellE>Ashar</span><span style='mso-bidi-font-weight: bold'>: Efficient SAT-based Unbounded Model Checking Using Circuit <span class=SpellE>Cofactoring</span></span>.<span style='mso-bidi-font-weight: bold'> </span>In Proceedings of the ACM/IEEE International Conference on Computer-Aided Design (ICCAD), November 2004<span style='mso-bidi-font-weight: bold'>.</span> <o:p></o:p></span></li> </ul> <p class=MsoListParagraph style='text-indent:-.25in;mso-list:l0 level1 lfo2'><![if !supportLists]><span style='font-size:11.0pt;font-family:Symbol;mso-fareast-font-family:Symbol; mso-bidi-font-family:Symbol'><span style='mso-list:Ignore'>·<span style='font:7.0pt "Times New Roman"'>&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp; </span></span></span><![endif]><span style='font-size:11.0pt;font-family:"Calibri",sans-serif; mso-ascii-theme-font:minor-latin;mso-hansi-theme-font:minor-latin'>A. Gupta, A. A. <span class=SpellE>Bayazit</span>, and Y. Mahajan: Verification Languages. Invited article in the  The Industrial Information Technology Handbook , Ed. R. <span class=SpellE>Zurawski</span>, CRC Press, <span class=GramE>November</span> 2004. <o:p></o:p></span></p> <ul style='margin-top:0in' type=disc> <li class=MsoNormal style='mso-list:l0 level1 lfo2'><span style='font-size: 11.0pt;font-family:"Calibri",sans-serif;mso-ascii-theme-font:minor-latin; mso-hansi-theme-font:minor-latin'>M. K. <span class=SpellE>Ganai</span>, A. Gupta, and P. <span class=SpellE>Ashar</span><span style='mso-bidi-font-weight: bold'>: Efficient Modeling of Embedded Memories in Bounded Model Checking</span>.<span style='mso-bidi-font-weight:bold'> </span>In Proceedings of the International Conference on Computer Aided Verification (CAV), July 2004. <o:p></o:p></span></li> <li class=MsoNormal style='mso-list:l0 level1 lfo2'><span style='font-size: 11.0pt;font-family:"Calibri",sans-serif;mso-ascii-theme-font:minor-latin; mso-hansi-theme-font:minor-latin'>A. Gupta, M. K. <span class=SpellE>Ganai</span>, Z. Yang, and P. <span class=SpellE>Ashar</span>: Iterative Abstraction using SAT-based BMC with Proof Analysis. In Proceedings of the ACM/IEEE International Conference on Computer-Aided Design (ICCAD), November 2003. <o:p></o:p></span></li> <li class=MsoNormal style='mso-list:l0 level1 lfo2'><span style='font-size: 11.0pt;font-family:"Calibri",sans-serif;mso-ascii-theme-font:minor-latin; mso-hansi-theme-font:minor-latin'>M. K. <span class=SpellE>Ganai</span>, A. Gupta, Z. Yang, and P. <span class=SpellE>Ashar</span>: Efficient Distributed SAT and SAT-based Distributed Bounded Model Checking. In Proceedings of the Conference on Correct Hardware Designs and Verification Methods (CHARME), September 2003.<span style='mso-spacerun:yes'>  </span><o:p></o:p></span></li> <li class=MsoNormal style='mso-list:l0 level1 lfo2'><span style='font-size: 11.0pt;font-family:"Calibri",sans-serif;mso-ascii-theme-font:minor-latin; mso-hansi-theme-font:minor-latin'>A. Gupta, C. Wang, M. K. <span class=SpellE>Ganai</span>, Z. Yang, P. <span class=SpellE>Ashar</span>: Abstraction and BDDs Complement SAT-based BMC in <span class=SpellE>DiVer</span>. In Proceedings of the International Conference on Computer Aided Verification (CAV), July 2003. <o:p></o:p></span></li> <li class=MsoNormal style='mso-list:l0 level1 lfo2'><span style='font-size: 11.0pt;font-family:"Calibri",sans-serif;mso-ascii-theme-font:minor-latin; mso-hansi-theme-font:minor-latin'>A. Gupta, M. K. <span class=SpellE>Ganai</span>, C. Wang, Z. Yang, and P. <span class=SpellE>Ashar</span>: Learning from BDDs in SAT-based Bounded Model Checking. In Proceedings of the ACM/IEEE Design Automation Conference (DAC), June 2003. <o:p></o:p></span></li> <li class=MsoNormal style='mso-list:l0 level1 lfo2'><span style='font-size: 11.0pt;font-family:"Calibri",sans-serif;mso-ascii-theme-font:minor-latin; mso-hansi-theme-font:minor-latin'>A. Gupta: Assertion-based Verification Turns the Corner. In IEEE Design &amp; Test of Computers, Volume 19, No. 4, 2002.<o:p></o:p></span></li> <li class=MsoNormal style='mso-list:l0 level1 lfo2'><span style='font-size: 11.0pt;font-family:"Calibri",sans-serif;mso-ascii-theme-font:minor-latin; mso-hansi-theme-font:minor-latin'>A. E. <span class=SpellE>Casavant</span>, A. Gupta, P. <span class=SpellE>Ashar</span>, X. G. Liu, A. <span class=SpellE>Mukaiyama</span>, and K. Wakabayashi: Property-Specific Witness Graph Generation for Guided Simulation. In Proceedings of the IEEE Conference on VLSI Design, January 2002. <o:p></o:p></span></li> <li class=MsoNormal style='mso-list:l0 level1 lfo2'><span style='font-size: 11.0pt;font-family:"Calibri",sans-serif;mso-ascii-theme-font:minor-latin; mso-hansi-theme-font:minor-latin'>A. Gupta, Z. Yang, P. <span class=SpellE>Ashar</span>, L. Zhang, and S. Malik: Partition Based Decision Heuristics for Image Computation Using SAT and BDDs. In Proceedings of the ACM/IEEE International Conference on Computer-Aided Design (ICCAD), Nov. 2001. <o:p></o:p></span></li> <li class=MsoNormal style='mso-list:l0 level1 lfo2'><span style='font-size: 11.0pt;font-family:"Calibri",sans-serif;mso-ascii-theme-font:minor-latin; mso-hansi-theme-font:minor-latin'>P. <span class=SpellE>Ashar</span>, A. Gupta, and S. Malik: Using Complete-1-Distinguishability for FSM equivalence checking. <span style='color:black;background:white'>ACM Transactions on Design Automation of Electronic Systems (TODAES), Volume 6 Issue 4, October 2001</span></span><span class=apple-converted-space><span style='font-size:11.0pt;font-family:"Calibri",sans-serif;mso-ascii-theme-font: minor-latin;mso-fareast-font-family:"Times New Roman";mso-fareast-theme-font: major-fareast;mso-hansi-theme-font:minor-latin;color:black;background: white'>.</span></span><span style='font-size:11.0pt;font-family:"Calibri",sans-serif; mso-ascii-theme-font:minor-latin;mso-hansi-theme-font:minor-latin'><o:p></o:p></span></li> <li class=MsoNormal style='mso-list:l0 level1 lfo2'><span style='font-size: 11.0pt;font-family:"Calibri",sans-serif;mso-ascii-theme-font:minor-latin; mso-hansi-theme-font:minor-latin'>A. Gupta, <span class=SpellE>Anubhav</span> Gupta, Z. Yang, and P. <span class=SpellE>Ashar</span>: Dynamic Detection and Removal of Inactive Clauses in SAT with Application in Image Computation. In Proceedings of the ACM/IEEE Design Automation Conference (DAC), June 2001. <o:p></o:p></span></li> <li class=MsoNormal style='mso-list:l0 level1 lfo2'><span style='font-size: 11.0pt;font-family:"Calibri",sans-serif;mso-ascii-theme-font:minor-latin; mso-hansi-theme-font:minor-latin'>A. Gupta, Z. Yang, P. <span class=SpellE>Ashar</span>, and <span class=SpellE>Anubhav</span> Gupta: SAT-based Image Computation with Application in Reachability Analysis. In Proceedings of the Conference on Formal Methods in Computer-Aided Design (FMCAD), Nov. 2000. <o:p></o:p></span></li> <li class=MsoNormal style='mso-list:l0 level1 lfo2'><span style='font-size: 11.0pt;font-family:"Calibri",sans-serif;mso-ascii-theme-font:minor-latin; mso-hansi-theme-font:minor-latin'>A. Gupta and P. <span class=SpellE>Ashar</span>: Fast Error Diagnosis for Combinational Verification. In Proceedings of the IEEE VLSI Design Conference, January 2000.<o:p></o:p></span></li> <li class=MsoNormal style='mso-list:l0 level1 lfo2'><span style='font-size: 11.0pt;font-family:"Calibri",sans-serif;mso-ascii-theme-font:minor-latin; mso-hansi-theme-font:minor-latin'>P. <span class=SpellE>Ashar</span>, A. <span class=SpellE>Raghunathan</span>, A. Gupta, and S. Bhattacharya: Verification of Scheduling in the Presence of Loops Using <span class=SpellE>Uninterpreted</span> Symbolic Simulation. In Proceedings of the IEEE International Conference on Computer Design (ICCD), October 1999.<o:p></o:p></span></li> <li class=MsoNormal style='mso-list:l0 level1 lfo2'><span style='font-size: 11.0pt;font-family:"Calibri",sans-serif;mso-ascii-theme-font:minor-latin; mso-hansi-theme-font:minor-latin'>A. Gupta, P. <span class=SpellE>Ashar</span>, and S. Malik: Exploiting Retiming in a Guided Simulation Based Validation Methodology. In Proceedings of the Conference on Correct Hardware Design and Verification Methods (<span style='mso-bidi-font-style:italic'>CHARME)</span>, September 1999.<o:p></o:p></span></li> <li class=MsoNormal style='mso-list:l0 level1 lfo2'><span style='font-size: 11.0pt;font-family:"Calibri",sans-serif;mso-ascii-theme-font:minor-latin; mso-hansi-theme-font:minor-latin'>A. Gupta and P. <span class=SpellE>Ashar</span>: Integrating a Boolean <span class=SpellE>Satisfiability</span> Checker and BDDs for Combinational Verification. In Proceedings of the IEEE <span style='mso-bidi-font-style:italic'>VLSI Design Conference</span>, January 1998.<o:p></o:p></span></li> <li class=MsoNormal style='mso-list:l0 level1 lfo2'><span style='font-size: 11.0pt;font-family:"Calibri",sans-serif;mso-ascii-theme-font:minor-latin; mso-hansi-theme-font:minor-latin'>A. Gupta, P. <span class=SpellE>Ashar</span> and S. Malik: Toward Formalizing a Simulation Based Verification Methodology. In Proceedings of the ACM/IEEE Design Automation Conference (DAC), June 1997.<o:p></o:p></span></li> <li class=MsoNormal style='mso-list:l0 level1 lfo2'><span style='font-size: 11.0pt;font-family:"Calibri",sans-serif;mso-ascii-theme-font:minor-latin; mso-hansi-theme-font:minor-latin'>P. <span class=SpellE>Ashar</span>, A. Gupta, and S. Malik: Using Complete-1-Distinguishability for FSM equivalence checking. In Proceedings of the ACM/IEEE International Conference on Computer-Aided Design (ICCAD), June 1996. <o:p></o:p></span></li> <li class=MsoNormal style='mso-list:l0 level1 lfo2'><span style='font-size: 11.0pt;font-family:"Calibri",sans-serif;mso-ascii-theme-font:minor-latin; mso-hansi-theme-font:minor-latin'>A. Gupta: Formal Hardware Verification Methods: A Survey. In Formal Methods in System Design, Kluwer Academic Publishers, Volume 1 (Nos. 2 &amp; 3), October 1992.<o:p></o:p></span></li> </ul> <p class=MsoNormal style='margin-left:40.5pt'><span style='font-size:10.0pt; mso-bidi-font-size:12.0pt;font-family:"Calibri",sans-serif;mso-ascii-theme-font: minor-latin;mso-hansi-theme-font:minor-latin'><o:p>&nbsp;</o:p></span></p> <p class=MsoNormal style='margin-left:40.5pt;text-indent:-22.5pt'><span style='font-size:11.0pt;mso-bidi-font-size:12.0pt;font-family:"Calibri",sans-serif; mso-ascii-theme-font:minor-latin;mso-hansi-theme-font:minor-latin'><o:p>&nbsp;</o:p></span></p> <p class=MsoNormal><a name=phd><b style='mso-bidi-font-weight:normal'><span style='font-family:"Calibri",sans-serif;mso-ascii-theme-font:minor-latin; mso-hansi-theme-font:minor-latin'>BDD-based Verification (related to Ph. D. Thesis)</span></b></a><b style='mso-bidi-font-weight:normal'><span style='font-family:"Calibri",sans-serif;mso-ascii-theme-font:minor-latin; mso-hansi-theme-font:minor-latin'> <o:p></o:p></span></b></p> <p class=MsoListParagraph style='text-indent:-.25in;mso-list:l0 level1 lfo2'><![if !supportLists]><span style='font-size:11.0pt;font-family:Symbol;mso-fareast-font-family:Symbol; mso-bidi-font-family:Symbol'><span style='mso-list:Ignore'>·<span style='font:7.0pt "Times New Roman"'>&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp; </span></span></span><![endif]><span style='font-size:11.0pt;font-family:"Calibri",sans-serif; mso-ascii-theme-font:minor-latin;mso-hansi-theme-font:minor-latin'>Aarti Gupta: Inductive Boolean Function Manipulation: A Hardware Verification Methodology for Automatic Induction, Ph.D. Thesis, Computer Science, Carnegie Mellon University, October 1994.<o:p></o:p></span></p> <ul style='margin-top:0in' type=disc> <li class=MsoNormal style='color:#5B9BD5;mso-themecolor:accent1;mso-list:l0 level1 lfo2'><span style='font-size:11.0pt;font-family:"Calibri",sans-serif;mso-ascii-theme-font: minor-latin;mso-hansi-theme-font:minor-latin;color:windowtext'>A. Gupta and A. L. Fisher: Tradeoffs in Canonical Sequential Function Representations. In Proceedings of the IEEE International Conference on Computer Design (ICCD), October 1994. <i style='mso-bidi-font-style:normal'><u><span style='color:#1F4E79;mso-themecolor:accent1;mso-themeshade:128;mso-style-textfill-fill-color: #1F4E79;mso-style-textfill-fill-themecolor:accent1;mso-style-textfill-fill-alpha: 100.0%;mso-style-textfill-fill-colortransforms:lumm=50000'>Winner of Outstanding Paper Award</span></u></i><u><span style='color:#1F4E79; mso-themecolor:accent1;mso-themeshade:128;mso-style-textfill-fill-color: #1F4E79;mso-style-textfill-fill-themecolor:accent1;mso-style-textfill-fill-alpha: 100.0%;mso-style-textfill-fill-colortransforms:lumm=50000'>.</span></u><span style='color:#1F4E79;mso-themecolor:accent1;mso-themeshade:128;mso-style-textfill-fill-color: #1F4E79;mso-style-textfill-fill-themecolor:accent1;mso-style-textfill-fill-alpha: 100.0%;mso-style-textfill-fill-colortransforms:lumm=50000'><o:p></o:p></span></span></li> <li class=MsoNormal style='mso-list:l0 level1 lfo2'><span style='font-size: 11.0pt;font-family:"Calibri",sans-serif;mso-ascii-theme-font:minor-latin; mso-hansi-theme-font:minor-latin'>A. Gupta and A. L. Fisher: Representation and Symbolic Manipulation of Linearly Inductive Boolean Functions. In Proceedings of the ACM/IEEE International Conference on Computer-Aided Design (ICCAD), November 1993.<o:p></o:p></span></li> <li class=MsoNormal style='mso-list:l0 level1 lfo2'><span style='font-size: 11.0pt;font-family:"Calibri",sans-serif;mso-ascii-theme-font:minor-latin; mso-hansi-theme-font:minor-latin'>A. Gupta and A. L. Fisher: Parametric Circuit Representation Using Inductive Boolean Functions. In Proceedings of the International Conference on Computer Aided Verification (CAV), June 1993.<o:p></o:p></span></li> </ul> <p class=MsoNormal style='margin-left:40.5pt;text-indent:-22.5pt'><span style='font-size:11.0pt;mso-bidi-font-size:12.0pt;font-family:"Calibri",sans-serif; mso-ascii-theme-font:minor-latin;mso-hansi-theme-font:minor-latin'><o:p>&nbsp;</o:p></span></p> <p class=MsoNormal><a name=masters><b style='mso-bidi-font-weight:normal'><span style='font-family:"Calibri",sans-serif;mso-ascii-theme-font:minor-latin; mso-hansi-theme-font:minor-latin'>Computer Systems (related to Master s Thesis)</span></b></a><b style='mso-bidi-font-weight:normal'><span style='font-family:"Calibri",sans-serif; mso-ascii-theme-font:minor-latin;mso-hansi-theme-font:minor-latin'><o:p></o:p></span></b></p> <ul style='margin-top:0in' type=disc> <li class=MsoNormal style='mso-list:l0 level1 lfo2'><span style='font-size: 11.0pt;font-family:"Calibri",sans-serif;mso-ascii-theme-font:minor-latin; mso-hansi-theme-font:minor-latin'>A. Gupta and A. L. Fisher: Flexible Parallel Polygon Rendering. In Proceedings of the International Conference on Parallel Processing (ICPP), July 1990.<o:p></o:p></span></li> <li class=MsoNormal style='mso-list:l0 level1 lfo2'><span style='font-size: 11.0pt;font-family:"Calibri",sans-serif;mso-ascii-theme-font:minor-latin; mso-hansi-theme-font:minor-latin'>M. J. Chung, E. J. Toy, and A. Gupta.<span style='mso-spacerun:yes'>  </span>A Highly Parallel Computer in Wafer Scale Integration. In Proceedings of the Conference on VLSI and Computers (<span class=SpellE>CompEuro</span>), July 1987.<o:p></o:p></span></li> <li class=MsoNormal style='mso-list:l0 level1 lfo2'><span style='font-size: 11.0pt;font-family:"Calibri",sans-serif;mso-ascii-theme-font:minor-latin; mso-hansi-theme-font:minor-latin'>M. J. Chung, and E. J. Toy, and A. Gupta: A Parallel Computer based on Cube Connected Cycles for Wafer Scale Integration. In Proceedings of the ACM/IEEE Fall Joint Computer Conference, November 1986.<o:p></o:p></span></li> </ul> <div> <p style='margin-left:.5in'><a name="0.2_SV"></a><span style='font-size:10.5pt; font-family:"Arial",sans-serif'>&nbsp;</span></p> </div> <div class=MsoNormal align=center style='text-align:center'><span style='font-family:"Arial",sans-serif;mso-fareast-font-family:"Times New Roman"'> <hr size=2 width="100%" align=center> </span></div> <p>&nbsp;</p> <p><o:p>&nbsp;</o:p></p> </div> </body> </html>