{"253441":{"#nid":"253441","#data":{"type":"event","title":"Software Engineering Seminar: Aws Albarghouthi, University of Toronto","body":[{"value":"\u003Cp\u003E\u003Cstrong\u003ESpeaker: Aws Albarghouthi\u003Cbr \/\u003E\u003C\/strong\u003E\u003C\/p\u003E\u003Cp\u003E\u003Cstrong\u003ETitle: From Bounded to Unbounded Proofs of Correctness\u003C\/strong\u003E\u003C\/p\u003E\u003Cp\u003E\u003Cstrong\u003EAbstract:\u003C\/strong\u003E Automatically proving correctness of software systems is a fundamental problem that has never seemed more important, given the increasing complexity of software systems and our absolute reliance on them. In this talk, I will describe generic, automated, push-button techniques for verifying safety of software systems, that is, proving that every execution of a program does not cause a crash (e.g., via division by zero) and satisfies intended functionality (e.g., programmer-supplied assertions). Since a program can have infinitely many possible executions, verifying each execution separately is impossible. Instead, I focus on examining a small number of program executions and using Craig interpolation to devise hypotheses explaining why the whole program might be safe. I will present new techniques for computing \u0022good\u0022 hypotheses (interpolants) and discuss our success with verifying (and finding bugs in) large C programs, including Linux device drivers.\u003C\/p\u003E\u003Cp\u003E\u003Cstrong\u003EBio:\u003C\/strong\u003E Aws Albarghouthi is a graduating PhD candidate at the University of Toronto, where he works with Marsha Chechik. Aws\u0027s overarching research goal is ensuring correctness, reliability, and security of software systems by arming developers with efficient tools and techniques for reasoning about their programs. His research has contributed to the areas of verification and program analysis, automated theorem proving, as well as program synthesis. Notably, his automated verification tool UFO won the largest number of verification categories in the recent International Software Verification Competition (SV-COMP\u002713).\u003C\/p\u003E","summary":null,"format":"limited_html"}],"field_subtitle":"","field_summary":"","field_summary_sentence":"","uid":"27263","created_gmt":"2013-11-11 12:12:34","changed_gmt":"2017-04-13 21:23:53","author":"Elizabeth Ndongi","boilerplate_text":"","field_publication":"","field_article_url":"","field_event_time":{"event_time_start":"2013-11-25T14:00:00-05:00","event_time_end":"2013-11-25T14:00:00-05:00","event_time_end_last":"2013-11-25T14:00:00-05:00","gmt_time_start":"2013-11-25 19:00:00","gmt_time_end":"2013-11-25 19:00:00","gmt_time_end_last":"2013-11-25 19:00:00","rrule":null,"timezone":"America\/New_York"},"extras":[],"groups":[{"id":"47223","name":"College of Computing"},{"id":"50875","name":"School of Computer Science"}],"categories":[],"keywords":[],"core_research_areas":[],"news_room_topics":[],"event_categories":[{"id":"1795","name":"Seminar\/Lecture\/Colloquium"}],"invited_audience":[{"id":"78751","name":"Undergraduate students"},{"id":"78761","name":"Faculty\/Staff"},{"id":"174045","name":"Graduate students"}],"affiliations":[],"classification":[],"areas_of_expertise":[],"news_and_recent_appearances":[],"phone":[],"contact":[{"value":"\u003Cp\u003E\u003Ca href=\u0022mailto:naik@cc.gatech.edu\u0022\u003Enaik@cc.gatech.edu\u003C\/a\u003E\u003C\/p\u003E","format":"limited_html"}],"email":[],"slides":[],"orientation":[],"userdata":""}}}