{"639640":{"#nid":"639640","#data":{"type":"event","title":"PhD Defense by Ravi Mangal ","body":[{"value":"\u003Cp\u003E\u003Cstrong\u003ETitle:\u003C\/strong\u003E Reasoning about Programs in Statistically Modeled First-Order Environments\u003C\/p\u003E\r\n\r\n\u003Cp\u003E\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: Friday, October 9\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\/840259460\u0022 target=\u0022_blank\u0022\u003Ehttps:\/\/bluejeans.com\/840259460\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, Partner 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 dissertation are programs and algorithms that reason about programs using their syntactic structure. \u0026nbsp;Such algorithms, referred to as \u003Cem\u003Eprogram verification algorithms\u003C\/em\u003E in the literature, are designed to find proofs of propositions about program behavior.\u003C\/p\u003E\r\n\r\n\u003Cp\u003E\u0026nbsp;\u003C\/p\u003E\r\n\r\n\u003Cp\u003EThis dissertation adopts the perspective that programs operate in environments that can be modeled statistically. In other words, program inputs are samples drawn from a generative statistical model. This statistical perspective has two main advantages.\u0026nbsp; First, it allows us to reason about programs that are not expected to exhibit the desired behavior on all program inputs, such as neural networks that are learnt from data, by formulating and proving probabilistic propositions about program behavior. Second, it enables us to simplify the search for proofs of non-probabilistic propositions about program behavior by designing program verification algorithms that are capable of inferring \u0026quot;likely\u0026quot; hypotheses about the program environment.\u003C\/p\u003E\r\n\r\n\u003Cp\u003E\u0026nbsp;\u003C\/p\u003E\r\n\r\n\u003Cp\u003EThe first contribution of this dissertation is a pair of program verification algorithms for finding proofs of \u003Cem\u003Eprobabilistic robustness\u003C\/em\u003E of neural networks. \u0026nbsp;A trained neural network \u003Cstrong\u003Ef\u003C\/strong\u003E is probabilistically robust if, for a pair of inputs that is randomly generated as per the environment statistical model, \u003Cstrong\u003Ef\u003C\/strong\u003E is likely to demonstrate \u003Cstrong\u003Ek-\u003C\/strong\u003ELipschitzness,\u0026nbsp;i.e., the distance between the outputs computed by \u003Cstrong\u003Ef\u003C\/strong\u003E is upper-bounded by the \u003Cstrong\u003Ek\u003Csup\u003Eth\u003C\/sup\u003E\u003C\/strong\u003E multiple of the distance between the pair of inputs. A proof of probabilistic robustness guarantees that the neural network is unlikely to exhibit divergent behaviors on similar inputs.\u003C\/p\u003E\r\n\r\n\u003Cp\u003E\u0026nbsp;\u003C\/p\u003E\r\n\r\n\u003Cp\u003EThe second contribution of this dissertation is a generic algorithmic framework, referred to as \u003Cem\u003Eobservational abstract interpreters\u003C\/em\u003E, for designing algorithms that compute \u003Cem\u003Ehypothetical\u003C\/em\u003E semantic program invariants. Semantic invariants are logical predicates about program behavior and are used in program proofs as lemmas. The well-studied algorithmic framework of abstract interpretation provides a standard recipe for constructing algorithms that compute semantic program invariants. Observational abstract interpreters extend this framework to allow for computing hypothetical invariants that are valid only under specific hypotheses about program environments. These hypotheses are inferred from observations of program behavior and are embedded as dynamic\/run-time checks in the program to ensure the validity of program proofs that use hypothetical invariants.\u003C\/p\u003E\r\n","summary":null,"format":"limited_html"}],"field_subtitle":"","field_summary":"","field_summary_sentence":[{"value":"Reasoning about Programs in Statistically Modeled First-Order Environments"}],"uid":"27707","created_gmt":"2020-09-28 15:34:38","changed_gmt":"2020-09-28 15:34:38","author":"Tatianna Richardson","boilerplate_text":"","field_publication":"","field_article_url":"","field_event_time":{"event_time_start":"2020-10-09T12:00:00-04:00","event_time_end":"2020-10-09T14:00:00-04:00","event_time_end_last":"2020-10-09T14:00:00-04:00","gmt_time_start":"2020-10-09 16:00:00","gmt_time_end":"2020-10-09 18:00:00","gmt_time_end_last":"2020-10-09 18:00:00","rrule":null,"timezone":"America\/New_York"},"extras":[],"groups":[{"id":"221981","name":"Graduate Studies"}],"categories":[],"keywords":[{"id":"100811","name":"Phd Defense"}],"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":"78751","name":"Undergraduate students"}],"affiliations":[],"classification":[],"areas_of_expertise":[],"news_and_recent_appearances":[],"phone":[],"contact":[],"email":[],"slides":[],"orientation":[],"userdata":""}}}