{"171011":{"#nid":"171011","#data":{"type":"event","title":"SE Seminar: Emina Torlak, University of California, Berkeley","body":[{"value":"\u003Cp\u003E\u003Cstrong\u003ETitle:\u003C\/strong\u003E Programming with Constraint Solvers:\u0026nbsp; Toward a Shared Infrastructure for Code Code\u0026nbsp;Checking, Angelic Execution, Debugging, and Synthesis\u003C\/p\u003E\u003Cp\u003E\u003Cstrong\u003EAbstract:\u003C\/strong\u003E\u003C\/p\u003E\u003Cp\u003EDecision procedures have helped automate key aspects of programming: coming up with a code fragment that implements a desired behavior (synthesis); establishing that an implementation satisfies a desired property (code checking); locating code fragments that cause an undesirable behavior (debugging); and running a partially implemented program to test its existing behaviors (angelic execution).\u0026nbsp; Each of these aspects is supported, at least in part, by a family of formal tools.\u0026nbsp; Most such tools are built on infrastructures that are tailored for a particular purpose, e.g., Boogie for verification and Sketch for synthesis.\u0026nbsp; But so far, no single infrastructure provides a platform for automating the full spectrum of programming activities, making it hard to share advances (in encodings, abstractions, and domain-specific optimizations) across different families of tools.\u003C\/p\u003E\u003Cp\u003E\u0026nbsp;This talk outlines a path toward a shared infrastructure for computer-aided programming, drawing lessons from a decade of collective experience in using relational constraint solvers to design and analyze software.\u0026nbsp; We start with a relational view of the heap pioneered in the early work on the Alloy language and Analyzer.\u0026nbsp; We then derive an encoding of programs in the bounded relational logic of Kodkod, which extends Alloy with support for partial models.\u0026nbsp; Next, we show by example how to use such an encoding to build a program checker, an angelic oracle, an automated debugger, and a template-based synthesis tool.\u0026nbsp; We conclude by discussing some of the challenges involved in lifting the low-level commonalities between these systems into an efficient infrastructure for prototyping and embedding of programming tools.\u003C\/p\u003E\u003Cp\u003E\u003Cstrong\u003E\u0026nbsp;Bio:\u003C\/strong\u003E Emina Torlak is a computer scientist at U.C. Berkeley.\u0026nbsp; She received her Ph.D. (2009), M.Eng. (2004) and B.Sc. (2003) in Computer Science from MIT.\u0026nbsp; Emina is interested in improving software design and development through automation.\u0026nbsp;\u0026nbsp; She has developed a variety of tools for helping programmers with lightweight formal reasoning, code and memory model analysis, debugging, and testing.\u0026nbsp; Her current projects focus on software synthesis for high performance computing.\u003C\/p\u003E\u003Cp\u003E\u0026nbsp;\u003C\/p\u003E","summary":null,"format":"limited_html"}],"field_subtitle":"","field_summary":"","field_summary_sentence":[{"value":"Programming with Constraint Solvers:  Toward a Shared Infrastructure for Code Checking, Angelic Execution, Debugging, and Synthesis"}],"uid":"27263","created_gmt":"2012-11-14 09:06:29","changed_gmt":"2016-10-08 02:01:17","author":"Elizabeth Ndongi","boilerplate_text":"","field_publication":"","field_article_url":"","field_event_time":{"event_time_start":"2012-11-19T11:00:00-05:00","event_time_end":"2012-11-19T11:00:00-05:00","event_time_end_last":"2012-11-19T11:00:00-05:00","gmt_time_start":"2012-11-19 16:00:00","gmt_time_end":"2012-11-19 16:00:00","gmt_time_end_last":"2012-11-19 16:00:00","rrule":null,"timezone":"America\/New_York"},"extras":[],"groups":[{"id":"47223","name":"College of Computing"}],"categories":[],"keywords":[],"core_research_areas":[],"news_room_topics":[],"event_categories":[{"id":"1795","name":"Seminar\/Lecture\/Colloquium"}],"invited_audience":[],"affiliations":[],"classification":[],"areas_of_expertise":[],"news_and_recent_appearances":[],"phone":[],"contact":[{"value":"\u003Cp\u003E\u003Ca href=\u0022mailto:ndongi@cc.gatech.edu\u0022\u003Endongi@cc.gatech.edu\u003C\/a\u003E\u003C\/p\u003E\u003Cp\u003E\u0026nbsp;\u003C\/p\u003E","format":"limited_html"}],"email":[],"slides":[],"orientation":[],"userdata":""}}}