{"637224":{"#nid":"637224","#data":{"type":"event","title":"PhD Proposal by Ravi Mangal","body":[{"value":"\u003Cp\u003E\u003Cstrong\u003ETitle:\u003C\/strong\u003E Reasoning about Programs in Statistically Modeled Environments\u003C\/p\u003E\r\n\r\n\u003Cp\u003E\u003Cbr \/\u003E\r\n\u0026nbsp;\u003C\/p\u003E\r\n\r\n\u003Cp\u003ERavi Mangal\u003C\/p\u003E\r\n\r\n\u003Cp\u003ESchool of Computer Science\u003C\/p\u003E\r\n\r\n\u003Cp\u003EGeorgia Institute of Technology\u003C\/p\u003E\r\n\r\n\u003Cp\u003E\u003Ca href=\u0022https:\/\/www.cc.gatech.edu\/~rmangal3\/\u0022 target=\u0022_blank\u0022\u003Ehttps:\/\/www.cc.gatech.edu\/~rmangal3\/\u003C\/a\u003E\u003C\/p\u003E\r\n\r\n\u003Cp\u003E\u0026nbsp;\u003C\/p\u003E\r\n\r\n\u003Cp\u003E\u003Cstrong\u003EDate\u003C\/strong\u003E: Thursday, July 30\u003Csup\u003Eth\u003C\/sup\u003E, 2020\u003C\/p\u003E\r\n\r\n\u003Cp\u003E\u003Cstrong\u003ETime\u003C\/strong\u003E: 11:00 AM -1:00 PM (EDT)\u003C\/p\u003E\r\n\r\n\u003Cp\u003E\u003Cstrong\u003ELocation:\u003C\/strong\u003E\u0026nbsp;\u003Ca href=\u0022https:\/\/bluejeans.com\/350947608\u0022 target=\u0022_blank\u0022\u003Ehttps:\/\/bluejeans.com\/350947608\u003C\/a\u003E\u003C\/p\u003E\r\n\r\n\u003Cp\u003E**Note: this proposal is remote-only**\u003C\/p\u003E\r\n\r\n\u003Cp\u003E\u0026nbsp;\u003C\/p\u003E\r\n\r\n\u003Cp\u003E\u003Cstrong\u003ECommittee:\u003C\/strong\u003E\u003C\/p\u003E\r\n\r\n\u003Cp\u003EDr. Alessandro Orso (Advisor), School of Computer Science, Georgia Institute of Technology\u003C\/p\u003E\r\n\r\n\u003Cp\u003EDr. Vivek Sarkar, School of Computer Science, Georgia Institute of Technology\u003C\/p\u003E\r\n\r\n\u003Cp\u003EDr. Qirun Zhang, School of Computer Science, Georgia Institute of Technology\u003C\/p\u003E\r\n\r\n\u003Cp\u003EDr. Bill Harris, Principal Scientist, Galois,Inc\u003C\/p\u003E\r\n\r\n\u003Cp\u003EDr. Aditya Nori, Sr. Principal Research Manager, Microsoft Research\u003C\/p\u003E\r\n\r\n\u003Cp\u003E\u0026nbsp;\u003C\/p\u003E\r\n\r\n\u003Cp\u003E\u003Cstrong\u003EAbstract:\u003C\/strong\u003E\u003C\/p\u003E\r\n\r\n\u003Cp\u003EThe objects of study in this proposal are programs and algorithms that use the syntactic structure of programs to reason about them. \u0026nbsp;Such algorithms, referred to as program verification algorithms in the literature, are designed to find proofs (in some background logic) of propositions about program behavior.\u003C\/p\u003E\r\n\r\n\u003Cp\u003E\u0026nbsp;\u003C\/p\u003E\r\n\r\n\u003Cp\u003EThis proposal adopts the perspective that programs operate in a world\/environment that can be modeled statistically. In other words, the inputs of a program are drawn from some distribution. This statistical perspective is relatively unexplored, though not new, in the context of program verification literature, and it enables us to formulate probabilistic propositions about program behavior. \u0026nbsp;Probabilistic propositions are particularly useful for reasoning about programs learnt from data (like neural networks) that are not expected to exhibit the desired behavior on all program inputs (or in all environments). \u0026nbsp;In this proposal, I define a notion of \u003Cem\u003Eprobabilistic robustness\/Lipschitzness\u003C\/em\u003E for neural networks. A trained neural network \u003Cem\u003Ef\u003C\/em\u003E is probabilistically robust if, for a randomly generated pair of inputs, \u003Cem\u003Ef\u003C\/em\u003E is likely to demonstrate \u003Cem\u003Ek\u003C\/em\u003E-Lipschitzness, i.e., the distance between the outputs computed by \u003Cem\u003Ef\u003C\/em\u003E is upper-bounded by the \u003Cem\u003Ek\u003Csup\u003Eth\u003C\/sup\u003E\u003C\/em\u003E multiple of the distance between the pair of inputs. I also present verification algorithms for finding proofs of probabilistic robustness of neural networks.\u003C\/p\u003E\r\n\r\n\u003Cp\u003E\u0026nbsp;\u003C\/p\u003E\r\n\r\n\u003Cp\u003EVerifying probabilistic robustness of neural networks is just one application of the statistical perspective on program environments. In order to enable generic program verification algorithms (that are agnostic to the proposition to be proven or the programming language) to benefit from this statistical perspective, this proposal presents\u003Cem\u003E observational abstract interpreters\u003C\/em\u003E, a generalization of standard abstract interpreters that are used for computing semantic program invariants. The invariants computed by observational abstract interpreters are permitted to be hypothetical (i.e. conditioned on hypotheses), with the hypotheses based on observed behaviors of the program. The validity of the proofs of program correctness computed using hypothetical semantic invariants is ensured by embedding the hypotheses as run time\/dynamic checks in the program. We state the metatheoretic guarantees, i.e., theorems about the behavior of observational abstract interpreters, that are expected to hold. These metatheoretic propositions remain to be proven. Proving these theorems and mechanizing them in a proof assistant represents the pending work.\u003C\/p\u003E\r\n","summary":null,"format":"limited_html"}],"field_subtitle":"","field_summary":"","field_summary_sentence":[{"value":"Reasoning about Programs in Statistically Modeled Environments"}],"uid":"27707","created_gmt":"2020-07-23 15:46:02","changed_gmt":"2020-07-23 15:46:02","author":"Tatianna Richardson","boilerplate_text":"","field_publication":"","field_article_url":"","field_event_time":{"event_time_start":"2020-07-30T12:00:00-04:00","event_time_end":"2020-07-30T14:00:00-04:00","event_time_end_last":"2020-07-30T14:00:00-04:00","gmt_time_start":"2020-07-30 16:00:00","gmt_time_end":"2020-07-30 18:00:00","gmt_time_end_last":"2020-07-30 18:00:00","rrule":null,"timezone":"America\/New_York"},"extras":[],"groups":[{"id":"221981","name":"Graduate Studies"}],"categories":[],"keywords":[{"id":"102851","name":"Phd proposal"}],"core_research_areas":[],"news_room_topics":[],"event_categories":[{"id":"1788","name":"Other\/Miscellaneous"}],"invited_audience":[{"id":"78761","name":"Faculty\/Staff"},{"id":"78771","name":"Public"},{"id":"174045","name":"Graduate students"},{"id":"78751","name":"Undergraduate students"}],"affiliations":[],"classification":[],"areas_of_expertise":[],"news_and_recent_appearances":[],"phone":[],"contact":[],"email":[],"slides":[],"orientation":[],"userdata":""}}}