Synthesis

Synthesis

From Verification to Synthesis Sumit Gulwani [email protected] Microsoft Research, Redmond August 2013 Marktoberdorf Summer School Lectures: Part 1 Synthesis Goal: Synthesize a computational concept in some underlying language from user intent using some search technique. State of the art: We can synthesize programs of size 10-20. 2 Dimensions in Synthesis Language(Application) Programs Straight-line programs Automata Queries

User Intent (Ambiguity) Logic, Natural Language Examples, Demonstrations/Traces Program Search Technique (Algorithm) SAT/SMT solvers (Formal Methods) A*-style goal-directed search (AI) Version space algebras (Machine Learning) PPDP 2010: Dimensions in Program Synthesis, 3 Compilers vs. Synthesizers Dimensio Compilers n Synthesizers

Concept Language Executable Program User Intent Structured language Search Technique Syntax-directed translation (No new algorithmic insights) Variety of concepts: Program, Automata, Query, Sequence Variety/mixed form of constraints: logic,

examples, traces Uses some kind of search (Discovers new algorithmic insights) 4 From verification to synthesis Bitvector algorithms (PLDI 2011, ICSE 2012) General loopy programs (POPL 2010) SIMD algorithms (PPoPP 2013) Program inverses (PLDI 2011) Graph algorithms (OOPSLA 2010) End-user Programming (Examples & Natural Language)

Syntactic string transformations: Flash Fill (POPL 2011) Semantic string transformations (VLDB 2012) Table layout transformations (PLDI 2011) Smartphone scripts (MobiSys 2013) Computer-aided Education Problem Synthesis (AAAI 2012, CHI 2013) Solution Synthesis (PLDI 2011, IJCAI 2013) Feedback Synthesis (PLDI 2013, IJCAI 2013) Content Authoring (CHI 2012) 5 From Verification to Synthesis Applicatio Generating n Synthesis

Constraint Bitvector Location variables Loopy Alg. Template-based SIMD Relational verification Inverses Template-based + symbolic execution Solving Synthesis Constraint CEGIS + SMT SMT CEGIS + Reachability value graph SMT Graph Alg. Reference: Path-based Inductive Synthesis for Program Inversion,

PLDI 2011, Srivastava, Gulwani, Chaudhuri, Foster 6 Dimensions in Synthesis Language Programs Straight-line programs Automata Queries User Intent Logic, Natural Language Examples, Demonstrations/Traces Program Search Technique SAT/SMT solvers (Formal Methods) A*-style goal-directed search (AI) Version space algebras (Machine Learning) 7 Program Inversion: Example

In-place run-length encoding: A = [1,1,1,0,0,2,2,2,2] Encoder A=[1,0,2] N=[3,2,4] Decoder A=[1,1,1,0,0,2,2,2,2] IN(A,n); Assume (n >= 0) i, m := 0, 0; // parallel assignment while (i0) r,i, A[i] := r-1, i+1,

A[m]; m := m+1; 8 Program Inversion as Synthesis Problem In-place run-length encoding: A = [1,1,1,0,0,2,2,2,2] Encoder A=[1,0,2] N=[3,2,4] Decoder A=[1,1,1,0,0,2,2,2,2] E = { 0, 1, m1, r1, i1, A[i], A[m], N[m] } IN(A,n); Assume (n >= 0) i, m := 0, 0; // parallel assignment while (i

A[m], N[m], m, i := A[i], r, m+1, i+1; OUT(A,N,m); IN(A,N,m) i, m := e1, e2; // ei E while (p1) // pi P r := e3; while (p2) r,i, A[e4] := e5, e6, e7; m := e8; 9 Synthesis Technique Inductive invariant required to establish correctness are too sophisticated. We use symbolic execution to generate verification condition for correctness on certain paths in the original and the inverted program. This generates constraints of the form 10

Related Work: Program Sketching Reference: Program Synthesis by Sketching, Phd Thesis 2008, Armando Solar-Lezama (Advisor: Ras Bodik @ UCBerkeley) Key Ideas: Write an arbitrary program with holes, where each hole takes values from a finite domain. Use CEGIS to generate SAT constraints on holes. Cons: Not as efficient as domain-specific synthesizers. (On bitvector benchmark, times out on 9/25 tasks, and on the remaining it is slower by 20x on average). Pros: A very powerful formalism that can be used to model a variety of synthesis problems. 11

Recently Viewed Presentations

  • Calorimetry - teachnlearnchem.com

    Calorimetry - teachnlearnchem.com

    Burning of a Match. Zumdahl, Zumdahl, DeCoste, World of Chemistry2002, page 293. Energy released to the surrounding as heat. Surroundings. System (Reactants)
  • Unit 4 Lesson 8 - Miss Valenti's Web-site

    Unit 4 Lesson 8 - Miss Valenti's Web-site

    Unit 4 Lesson 8. Multiply with Decimals Greater Than 1 . Find the Fiction. 4 x 0.2 would have 1 decimal place. 3 x 0.07 would have 2 decimal places. 0.8 x 0.4 would have 3 decimal places. Oh where,...
  • Common Loon 28  36 inches Migration Water Small

    Common Loon 28 36 inches Migration Water Small

    Common Loon 28 - 36 inches Migration Water Small fish and crustaceans Tundra Swan 53 inches Migration Water, fields Grasses, seeds, aquatic plants Hooded Merganser 16-19 inches Breeding Water Fish Sharp-Shinned Hawk 10-14 inches Year round Mixed woods and thickets...
  • The Feasts of Israel - Bible Study Resource Center

    The Feasts of Israel - Bible Study Resource Center

    I will seek out these sheep that are lost and scattered." Aren't you glad that the Lord is our shepherd? And that He has sought us out, scattered and bruised He found us, and He drew us into His fold,...
  • Bi 1 Tm hiu v du lch Ti

    Bi 1 Tm hiu v du lch Ti

    Bài 1 Tìm hiểu về du lịch Tài liệu này được xây dựng với sự hỗ trợ tài chính của Liên minh Châu Âu. Tổ chức SNV và ILO hoàn toàn chịu trách nhiệm về nội dung của tài liệu...
  • NCLB Updates Association of Compensatory Educators of Texas

    NCLB Updates Association of Compensatory Educators of Texas

    If a district reserves funds off the top for the following services within their campuses, the equitable services rule applies. Title I Part A PNP allocation for 'off the top' reservations is calculated by 'available funds…must be proportional to the...
  • HSC GEOGRAPHY Overview - mrstevennewman.com

    HSC GEOGRAPHY Overview - mrstevennewman.com

    Culturally, people with money want to be where other people with money are. Hence the Cultural Authority Mega Cities A definition based purely on population Size. Syllabus uses old United Nations Definition of 8 million or more inhabitants of a...
  • Required Yearly Trainings Objective: To be able to

    Required Yearly Trainings Objective: To be able to

    Online through Moodle. Employees receive an email with instructions and a link to follow from Risk Management. Use your Mineonline login and password to log into Moodle. Tip! You can usually open the training and the quiz simultaneously to save...