Travelled to:1 × Canada
1 × Hungary
15 × USA
2 × Italy
Collaborated with:S.Chaudhuri A.Cheung R.Singh S.Madden X.Qiu K.Yessenov R.Bodík I.Kuraj J.S.Foster Z.Xu J.Jeon S.Kong S.Gao S.Itzhaky L.Tancau V.A.Saraswat S.A.Seshia M.Clochard S.Gulwani J.Yang C.G.Jones James Koppel Varot Premtoon O.Bastani Xin Zhang 0035 N.Polikarpova X.Wang N.Zeldovich M.F.Kaashoek R.M.Rabbah K.Ebcioglu S.Kamil R.Singh R.Krosnick V.Ganesh C.W.O'Donnell M.Soos S.Devadas M.C.Rinard G.Arnold Jean Yang 0001 Travis Hance T.H.Austin C.Flanagan S.Chong J.Kapinski J.V.Deshmukh N.Roohi N.Aréchiga Rohit Singh 0002 Yongquan Lu C.E.Leiserson R.A.Chowdhury Benjamin Mariano J.Reese Siyuan Xu T.Nguyen
Talks about:program (12) synthesi (9) sketch (7) data (4) use (4) structur (3) languag (3) databas (3) system (3) smooth (3)
Person: Armando Solar-Lezama
DBLP: Solar-Lezama:Armando
Contributed to:
2015
2015
2014
2014
2014
2013
20132012
20122012
201220112011
2011201020082007
2006200520182019201620172018201920162017Wrote 33 papers:
- CAV-2015-JeonQSF #adaptation #parallel #synthesis
- Adaptive Concretization for Parallel Program Synthesis (JJ, XQ, ASL, JSF), pp. 377–394.
- ESEC-FSE-2015-JeonQFS #java #named #sketching
- JSketch: sketching for Java (JJ, XQ, JSF, ASL), pp. 934–937.
- POPL-2014-ChaudhuriCS #proving #synthesis #using
- Bridging boolean and quantitative synthesis using smoothed proof search (SC, MC, ASL), pp. 207–220.
- SIGMOD-2014-CheungMS #database #lazy evaluation #named #query
- Sloth: being lazy is a virtue (when issuing database queries) (AC, SM, ASL), pp. 931–942.
- VMCAI-2014-SinghSXKS #composition #modelling #sketching #synthesis #using
- Modular Synthesis of Sketches Using Models (RS, RS, ZX, RK, ASL), pp. 395–414.
- PLDI-2013-CheungSM #optimisation #query #synthesis
- Optimizing database-backed applications with query synthesis (AC, ASL, SM), pp. 3–14.
- PLDI-2013-SinghGS #automation #feedback #generative #programming
- Automated feedback generation for introductory programming assignments (RS, SG, ASL), pp. 15–26.
- SOSP-2013-WangZKS #behaviour #towards
- Towards optimization-safe systems: analyzing the impact of undefined behavior (XW, NZ, MFK, ASL), pp. 260–275.
- CAV-2012-ChaudhuriS #named #optimisation #source code
- Euler: A System for Numerical Optimization of Programs (SC, ASL), pp. 732–737.
- CAV-2012-SinghS #named #programming
- SPT: Storyboard Programming Tool (RS, ASL), pp. 738–743.
- CIKM-2012-CheungSM #recommendation #social #synthesis #using
- Using program synthesis for social recommendations (AC, ASL, SM), pp. 1732–1736.
- POPL-2012-YangYS #automation #policy #privacy
- A language for automatically enforcing privacy policies (JY, KY, ASL), pp. 85–96.
- SAT-2012-GaneshOSDRS #named #problem #satisfiability
- Lynx: A Programmatic SAT Solver for the RNA-Folding Problem (VG, CWO, MS, SD, MCR, ASL), pp. 143–156.
- CAV-2011-ChaudhuriS #robust
- Smoothing a Program Soundly and Robustly (SC, ASL), pp. 277–292.
- ESEC-FSE-2011-CheungSM
- Partial replay of long-running applications (AC, ASL, SM), pp. 135–145.
- ESEC-FSE-2011-SinghS #data type
- Synthesizing data structure manipulations from storyboards (RS, ASL), pp. 289–299.
- OOPSLA-2011-YessenovXS #data-driven #framework #object-oriented #synthesis
- Data-driven synthesis for object-oriented frameworks (KY, ZX, ASL), pp. 65–82.
- PLDI-2010-ChaudhuriS
- Smooth interpretation (SC, ASL), pp. 279–291.
- PLDI-2008-Solar-LezamaJB #concurrent #data type #sketching
- Sketching concurrent data structures (ASL, CGJ, RB), pp. 136–148.
- PLDI-2007-Solar-LezamaATBSS #sketching
- Sketching stencils (ASL, GA, LT, RB, VAS, SAS), pp. 167–178.
- ASPLOS-2006-Solar-LezamaTBSS #combinator #finite #sketching #source code
- Combinatorial sketching for finite programs (ASL, LT, RB, SAS, VAS), pp. 404–415.
- PLDI-2005-Solar-LezamaRBE #programming #sketching #source code
- Programming by sketching for bit-streaming programs (ASL, RMR, RB, KE), pp. 281–294.
- CAV-2018-KongSG #problem
- Delta-Decision Procedures for Exists-Forall Problems over the Reals (SK, ASL, SG), pp. 219–235.
- CAV-2019-GaoKDRSAK #induction #proving
- Numerically-Robust Inductive Proof Rules for Continuous Dynamical Systems (SG, JK, JVD, NR, ASL, NA, SK), pp. 137–154.
- OOPSLA-2016-Itzhaky0SYLLC #algorithm #divide and conquer #programming #using
- Deriving divide-and-conquer dynamic programming algorithms using solver-aided transformations (SI, RS0, ASL, KY, YL, CEL, RAC), pp. 145–164.
- OOPSLA-2017-QiuS #synthesis
- Natural synthesis of provably-correct data-structure manipulations (XQ, ASL), p. 28.
- OOPSLA-2018-KoppelPS #incremental #parametricity #syntax
- One tool, many languages: language-parametric transformation with incremental parametric syntax (JK, VP, ASL), p. 28.
- OOPSLA-2019-Bastani0S #probability #verification
- Probabilistic verification of fairness properties via concentration (OB, XZ0, ASL), p. 27.
- OOPSLA-2019-MarianoRXNQFS #algebra #library #specification #synthesis
- Program synthesis with algebraic library specifications (BM, JR, SX, TN, XQ, JSF, ASL), p. 25.
- PLDI-2016-KamilCIS
- Verified lifting of stencil computations (SK, AC, SI, ASL), pp. 711–726.
- PLDI-2016-PolikarpovaKS #polymorphism #refinement #synthesis
- Program synthesis from polymorphic refinement types (NP, IK, ASL), pp. 522–538.
- PLDI-2016-YangHASFC #data flow #information management #precise
- Precise, dynamic information flow for database-backed applications (JY0, TH, THA, ASL, CF, SC), pp. 631–647.
- PLDI-2017-YessenovKS #api #named
- DemoMatch: API discovery from demonstrations (KY, IK, ASL), pp. 64–78.