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.9 Released (April, 2015) :

This version corresponds to changeset d9f004c9a54c of the sketch-backend and changeset ec77eebbcc0a of the sketch-frontend. You can download an easy-to-install (relatively speaking)  source distribution from here:
Tar ball    
sketch-1.6.9.tar.gz  
 
Working version of Sketch Manual
If you want to be notified about new releases or major bug-fixes, you can subscribe to the sketch users mailing list.


Teaching:

  • Fall  2013: 6.820 Foundations of Program Analysis
  • 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:

Swarat Chaudhuri, Martin Clochard, Armando Solar-Lezama: Bridging Boolean and Quantitative Synthesis Using Smoothed Proof Search POPL 14
Rohit Singh, Rishabh Singh, Zhilei Xu, Rebecca Krosnick and Armando Solar-Lezama: Modular Synthesis of Sketches using Models VMCAI 14
Xi Wang, Nickolai Zeldovich, M. Frans Kaashoek, Armando Solar-Lezama: Towards optimization-safe systems: analyzing the impact of undefined behavior. Best paper award. SOSP 13
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)