Armando Solar-Lezama
Associate Professor without Tenure

e-mail:
phone: (617) 258-9727
mit_logo.gif
asolar_180.jpg
""

Research Agenda:

I work with the Computer Assisted Programming Group; our goal is to develop techniques and tools that exploit automated reasoning and large amounts of computing power to tackle challenging programming problems.


(new) Sketch Version 1.6.4 Released (May 15, 2013) :
This version corresponds to changeset 94f44fb of the sketch-backend and changeset b44adca of the sketch-frontend. You can download an easy-to-install (relatively speaking)  source distribution from here:
Tar ball    
sketch-1.6.4.tar.gz  
  
Working version of Sketch Manual


Teaching:
  • Spring 2013: 6.00 Introduction to Computer Science and Programming
  • Spring 2012: 6.005 Elements of Software Construction
  • Fal 2011: 6.820 Foundations of Program Analysis
  • Fall 2010: 6.820 Foundations of Program Analysis
  • Spring 2010: 6.005 Elements of Software Construction
  • Fall 2009: 6.883 Foundations of Program Analysis with Martin Rinard
  • Spring 2009: 6.035 Computer Language Engineering with Saman Amarasinghe
  • IAP 2009: 3 day mini-course on Sketching

Recent Publications:
Rishabh Singh, Sumit Gulwani, Armando Solar-Lezama: Automated Feedback Generation for Introductory Programming Assignments PLDI 13
Alvin Cheung, Armando Solar-Lezama, Samuel Madden: Optimizing Database-Backed Applications with Program Synthesis PLDI 13
Alvin Cheung, Owen Arden, Sam Madden, Armando Solar-Lezama, and Andrew Myers: StatusQuo: Making Familiar Abstractions Perform Using Program Analysis, Best paper award. CIDR 13
Alvin Cheung, Armando Solar-Lezama, Samuel Madden: Using program synthesis for social recommendations CIKM 12
Swarat Chaudhuri, Armando Solar-Lezama: Euler: A System for Numerical Optimization of Programs CAV 12
Rishabh Singh, Armando Solar-Lezama: SPT: Storyboard Programming Tool CAV 12
Jean Yang, Kuat Yessenov, Armando Solar-Lezama: A language for automatically enforcing privacy policies. POPL 12
Vijay Ganesh, Charles W. O'Donnell, Mate Soos, Srinivas Devadas, Martin C. Rinard, Armando Solar-Lezama: Lynx: A Programmatic SAT Solver for the RNA-Folding Problem SAT 12
Kuat Yessenov, Zhilei Xu, Armando Solar-Lezama: Data-Driven Synthesis for Object-Oriented Frameworks, in OOPSLA 2011 (SPLASH) OOPSLA 11
Rishabh Singh, Armando Solar-Lezama: Synthesizing data structure manipulations from storyboards, in ACM SIGSOFT Symposium on the Foundations of Software Engineering FSE 11
Alvin Cheung, Armando Solar-Lezama, Samuel Madden: Partial replay of long-running applications, in ACM SIGSOFT Symposium on the Foundations of Software Engineering FSE 11
Swarat Chaudhuri, Armando Solar-Lezama: Smoothing a Program Soundly and Robustly, in 23rd International Conference on Computer Aided Verification CAV 11
Swarat Chaudhuri, Armando Solar-Lezama, "Smooth Interpretation", in ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI '10) [Slides] PLDI 10
Armando Solar-Lezama, "Program Synthesis by Sketching", PhD Thesis Berkeley 08
Armando Solar-Lezama, Christopher G. Jones, Rastislav Bodik, "Sketching Concurrent Datastructures"in ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI '08) PLDI 08
  Armando Solar-Lezama, Gilad Arnold, Liviu Tancau, Rastislav Bodik, Vijay Saraswat, Sanjit Seshia, "Sketching Stencils" in ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI '07) PLDI 07
  Armando Solar-Lezama, Liviu Tancau, Rastislav Bodik, Vijay Saraswat, Sanjit A. Seshia, "Combinatorial Sketching for Finite Programs", Proceedings of ASPLOS 2006. ASPLOS 06
  Armando Solar-Lezama, Rodric Rabbah, Rastislav Bodik, and Kemal Ebcioglu, "Programming by Sketching for Bitstreaming Programs", PLDI 2005, Best paper award. PLDI 05

Contact:
MIT Computer Science and Artificial Intelligence Laboratory
The Stata Center, Building 32-G840
32 Vassar Street
Cambridge, MA 02139
Assistant: Sally Lee (sally@ csail.mit.edu)