Santiago Gonzalez

DREU 2014 - MIT

August 14, 2014

I can't believe this was my last week! I am very far along automatically generating the most general client as an abstract syntax tree (AST) within the Sketch compiler frontend. I plan to finish this early next week. Dr. Solar-Lezama and I have discussed plans to continue this work when I return home. We are going to present at a poster competition in OOPSLA this October (the project got accepted, yay!), and we are hoping to get a paper submitted to PLDI in November. This was nothing short of an amazing summer!

August 8, 2014

This week, I have finished writing a most general client test implementation in Sketch. I tested the implementation over various numbers of iterations. For 5 iterations of the most general client's loop, the verification took ~27 seconds. For 6, ~6 minutes. For 7, ~1:40 hours. This exponential nature is expected, and can't be improved upon, since the Sketch synthesizer is based on a SAT solver (an NP-complete problem). I found that Sketch was able to find all the erroneous differences that I introduced in my example packages in just a couple iterations. Next week, I will add a new pass to the compiler that automatically generates a most general client for every parent-child package relationship in a program. This week, I also attended Rishabh Singh's (one of the PhD students in the research group) thesis defenses on Accessible Programing using Program Synthesis. I was surprised to learn that he worked on FlashFill feature of Microsoft Excel.

August 1, 2014

This week, Dr. Solar-Lezama and I have finished formulating a most general client for package equivalence verification. We have decided to dogfood the most general client and write it in Sketch. Implementing the client in Sketch will allow us to harness the synthesizer's power to go through all important possible solutions. Next week will involve finishing up a test implementation for the set example and beginning to add this functionality to the compiler. This week, I also attended two very interesting thesis defenses; Driving Story Generation with Learnable Character Models and Smten and the Art of Satisfiability Based Search (Dr. Solar-Lezama was on this thesis committee).

July 25, 2014

This week, Dr. Solar-Lezama has been absent to attend the CAV (Computer Aided Verification) conference in Vienna, he should be back this coming Monday. I continued working towards formulating a mathematically correct most general client. I also took advantage of this time to meet with the graduate administrator for the EECS department, regarding the application process for the PhD program, and write the DREU program's progress report, available here. Additionally, I added a Photo Gallery to this website with some of the pictures that I have taken while being here. On Tuesday, I attended the first chocolate tasting organized by the IT department here at CSAIL; I am on my way to becoming more of a chocolate snob.

July 18, 2014

This week, Dr. Solar-Lezama and I started discussing how we will formulate a most general client to verify equivalency between a set of packages. I have begun to think about what characteristics the most general client's call sequence must have to ensure adequate generality. Dr. Solar-Lezama returned this Wednesday and left to go to the CAV (Computer Aided Verification) conference in Vienna on Thursday. He will be gone all next week though has said he will be able to Skype. I also attended PhD student's thesis defense on "Discovering Linguistic Structures in Speech: Models and Applications" which described a novel method of segmenting audio streams into phonemes, syllables, and words without any a priori knowledge.

July 11, 2014

Earlier this week, I finished implementing the type-checking rules for the package system. I have tested it out using several small Sketch programs to evaluate that it catches all weird, edge-cases. Additionally, I have written an extended abstract regarding the project for a poster competition that will take place in the OOPSLA (Object-Oriented Programming, Systems, Languages, and Applications) conference, this November. You can download the extended abstract here. Dr. Solar-Lezama left for a conference this Thursday and will be back next week to discuss further work, which will involve constructing a most general client to verify package equivalence.

July 3, 2014

I am quite far along implementing the type rules into the Sketch compiler front-end (which is written in Java) as a compiler pass using a standard visitor pattern that analyzes the AST (Abstract Syntax Tree). I suspect that I will finish implementing this early next week. Dr. Solar-Lezama has begun to tell me what the next steps for the package system are. I also attended a seminar this week on Practical Techniques for Auto-Active Verification, which is very applicable to the area of research I am working in. Overall, I have really enjoyed these past few weeks here at MIT.

June 27, 2014

This week, I worked on finalizing the type rules with Dr. Solar-Lezama and thinking about the various edge cases that might violate the intended rules. A finalized PDF of these rules is available here. Dr. Solar-Lezama started to give me basic information regarding the functioning of the compiler's visitor patterns so that I could start implementing the type rules as a new compiler pass. This week, I also attended a seminar on Quantitative Program Correctness.

June 20, 2014

This week, Dr. Solar-Lezama introduced me to the formal notation used to represent type-checking rules and had me work on such rules for the new package system in Sketch. I read "Type Systems" by Luca Cardelli, of Microsoft Research, to gain familiarity with type systems. A finalized PDF of these rules is available here. Also, this week I attended a seminar here at MIT regarding pedestrian avoidance in smart-cars.

June 13, 2014

This is my first week of the DREU here at MIT. Dr. Solar-Lezama was at a conference in Edinburgh this past week so I will see him on Monday. We met previously on Saturday where he gave me a brief overview of what I was going to be working on during the summer. I started familiarizing myself with the Sketch language this week along with the basic structure of the AST (Abstract Syntax Tree) that is utilized by the compiler front-end.