Travelled to:1 × China
1 × India
1 × Italy
1 × Spain
1 × Switzerland
1 × The Netherlands
1 × United Kingdom
23 × USA
4 × Canada
Collaborated with:R.Gupta E.Torlak ∅ M.L.Soffa A.Shankar M.Sridharan A.Solar-Lezama S.Chasins C.Wang A.Cheung S.Barman S.Chandra P.M.Phothilimthana M.Xu M.D.Hill V.A.Saraswat V.Sarkar G.Ammons J.R.Larus T.Hottelier Y.Pu S.Srivastava A.Raabe D.Mandelin S.Anik A.T.0001 D.Dhurjati Kartik Chandra M.Sagiv D.Kimelman A.S.Köksal G.Arnold L.Tancau S.A.Seshia J.Galenson M.Arnold C.G.Jones S.J.Fink S.Rubin T.M.Chilimbi G.Fedyukovich Maaz Bin Safeer Ahmad L.A.Meyerovich M.E.Torok E.Atkinson S.S.Sastry J.E.Smith D.Gopan L.Shan L.Xu R.M.Rabbah K.Ebcioglu S.Gulwani P.Reames B.Hartmann K.Sen S.Litvak N.Dor N.Rinetzky J.Hölzl Y.Feng I.Dillig A.Bhattacharya D.Culler T.Jelvis R.Shah N.Totla J.Fisher N.Piterman N.Tung C.Rodarmor Archibald Samuel Elliott An Wang 0003 Abhinav Jangda Bastian Hagedorn Henrik Barthels Samuel J. Kaufman V.Grover
Talks about:synthesi (13) program (13) analysi (10) sketch (6) data (6) solver (4) sensit (4) elimin (4) code (4) aid (4)
Person: Rastislav Bodík
DBLP: Bod=iacute=k:Rastislav
Facilitated 3 volumes:
Ed
Ed
EdContributed to:
2015
2015
2015
2014
2014
201320132013
2013
201220112011
201020102010
2009
20092008
2008200820082007200620062005200520032002200019991999199819981998
19971997201620162017201820172018202020162019Wrote 55 papers:
- ICFP-2015-Bodik #synthesis
- Program synthesis: opportunities for the next decade (RB), p. 1.
- OOPSLA-2015-HottelierB #constraints #layout #relational #synthesis
- Synthesis of layout engines from relational constraints (TH, RB), pp. 74–88.
- Onward-2015-BarmanBCTBC #interactive #synthesis #tool support #towards
- Toward tool support for interactive synthesis (SB, RB, SC, ET, AB, DC), pp. 121–136.
- ICSE-2014-GalensonRBHS #interactive #named #synthesis
- CodeHint: dynamic and interactive synthesis of code snippets (JG, PR, RB, BH, KS), pp. 653–663.
- PLDI-2014-PhothilimthanaJSTCB #architecture #compilation #named #power management
- Chlorophyll: synthesis-aided compiler for low-power spatial architectures (PMP, TJ, RS, NT, SC, RB), p. 42.
- PLDI-2014-TorlakB #lightweight #virtual machine
- A lightweight symbolic virtual machine for solver-aided host languages (ET, RB), p. 54.
- GPCE-2013-Bodik #biology #modelling #programming language
- Modeling biology with solver-aided programming languages (RB), pp. 1–2.
- Onward-2013-TorlakB
- Growing solver-aided languages with rosette (ET, RB), pp. 135–152.
- POPL-2013-KoksalPSBFP #biology #modelling #synthesis
- Synthesis of biological models from mutation experiments (ASK, YP, SS, RB, JF, NP), pp. 469–482.
- PPoPP-2013-MeyerovichTAB #attribute grammar #parallel #synthesis
- Parallel schedule synthesis for attribute grammars (LAM, MET, EA, RB), pp. 187–196.
- CAV-2012-BodikT #constraints #source code #theorem proving
- Synthesizing Programs with Constraint Solvers (RB, ET), p. 3.
- ICSE-2011-ChandraTBB #debugging
- Angelic debugging (SC, ET, SB, RB), pp. 121–130.
- OOPSLA-2011-PuBS #algorithm #first-order #programming #synthesis
- Synthesis of first-order dynamic programming algorithms (YP, RB, SS), pp. 83–98.
- FSE-2010-LitvakDBRS #analysis #dependence
- Field-sensitive program dependence analysis (SL, ND, RB, NR, MS), pp. 287–296.
- ICFP-2010-ArnoldHKBS #matrix #specification #verification
- Specifying and verifying sparse matrix codes (GA, JH, ASK, RB, MS), pp. 249–260.
- POPL-2010-BodikCGKTBR #nondeterminism #programming
- Programming with angelic nondeterminism (RB, SC, JG, DK, NT, SB, CR), pp. 339–352.
- DAC-2009-RaabeB #hardware #sketching
- Synthesizing hardware from sketches (AR, RB), pp. 623–624.
- SAS-2009-Bodik #algorithm #source code #synthesis
- Algorithmic Program Synthesis with Partial Programs and Decision Procedures (RB), p. 1.
- OOPSLA-2008-ShankarAB #dynamic analysis #lightweight #named
- Jolt: lightweight dynamic analysis and removal of object churn (AS, MA, RB), pp. 127–142.
- PEPM-2008-Bodik #sketching #synthesis
- Software synthesis with sketching (RB), pp. 1–2.
- PLDI-2008-Solar-LezamaJB #concurrent #data type #sketching
- Sketching concurrent data structures (ASL, CGJ, RB), pp. 136–148.
- PPoPP-2008-ChandraSSB #analysis #data type #distributed #locality #type inference
- Type inference for locality analysis of distributed data structures (SC, VAS, VS, RB), pp. 11–22.
- PLDI-2007-ShankarB #automation #data type #invariant #java #named
- DITTO: automatic incrementalization of data structure invariant checks (in Java) (AS, RB), pp. 310–319.
- PLDI-2007-Solar-LezamaATBSS #sketching
- Sketching stencils (ASL, GA, LT, RB, VAS, SAS), pp. 167–178.
- PLDI-2007-SridharanFB #slicing
- Thin slicing (MS, SJF, RB), pp. 112–122.
- ASPLOS-2006-Solar-LezamaTBSS #combinator #finite #sketching #source code
- Combinatorial sketching for finite programs (ASL, LT, RB, SAS, VAS), pp. 404–415.
- ASPLOS-2006-XuHB #memory management #reduction #transitive
- A regulated transitive reduction (RTR) for longer memory race recording (MX, MDH, RB), pp. 49–60.
- PLDI-2006-SridharanB #analysis #java #points-to
- Refinement-based context-sensitive points-to analysis for Java (MS, RB), pp. 387–400.
- OOPSLA-2005-ShankarSBS #analysis #runtime
- Runtime specialization with optimistic heap analysis (AS, SSS, RB, JES), pp. 327–343.
- OOPSLA-2005-SridharanGSB #analysis #java #points-to
- Demand-driven points-to analysis for Java (MS, DG, LS, RB), pp. 59–76.
- PLDI-2005-MandelinXBK #api #mining
- Jungloid mining: helping to navigate the API jungle (DM, LX, RB, DK), pp. 48–61.
- PLDI-2005-Solar-LezamaRBE #programming #sketching #source code
- Programming by sketching for bit-streaming programs (ASL, RMR, RB, KE), pp. 281–294.
- PLDI-2005-XuBH #detection #source code
- A serializability violation detector for shared-memory server programs (MX, RB, MDH), pp. 1–14.
- PLDI-2003-AmmonsMBL #concept analysis #debugging #specification
- Debugging temporal specifications with concept analysis (GA, DM, RB, JRL), pp. 182–195.
- POPL-2002-AmmonsBL #mining #specification
- Mining specifications (GA, RB, JRL), pp. 4–16.
- POPL-2002-RubinBC #framework #optimisation #performance
- An efficient profile-analysis framework for data-layout optimizations (SR, RB, TMC), pp. 140–153.
- PLDI-2000-BodikGS #array #bound #named
- ABCD: eliminating array bounds checks on demand (RB, RG, VS), pp. 321–333.
- CC-1999-GuptaB
- Register Pressure Sensitive Redundancy Elimination (RG, RB), pp. 107–121.
- PLDI-1999-BodikGS #analysis #design #evaluation
- Load-Reuse Analysis: Design and Evaluation (RB, RG, MLS), pp. 64–76.
- Best-of-PLDI-1998-BodikGS98a
- Complete removal of redundant expressions (with retrospective) (RB, RG, MLS), pp. 596–611.
- PLDI-1998-BodikGS
- Complete Removal of Redundant Computations (RB, RG, MLS), pp. 1–14.
- POPL-1998-BodikA #analysis
- Path-Sensitive Value-Flow Analysis (RB, SA), pp. 237–251.
- ESEC-FSE-1997-BodikGS #data flow #using
- Refining Data Flow Information Using Infeasible Paths (RB, RG, MLS), pp. 361–377.
- PLDI-1997-BodikG #slicing #using
- Partial Dead Code Elimination using Slicing Transformations (RB, RG), pp. 159–170.
- PLDI-1997-BodikGS #branch #interprocedural
- Interprocedural Conditional Branch Elimination (RB, RG, MLS), pp. 146–158.
- CC-2016-PhothilimthanaT #framework #named
- GreenThumb: superoptimizer construction framework (PMP, AT0, RB, DD), pp. 261–262.
- OOPSLA-2016-BarmanCBG #automation #named #web
- Ringer: web automation by demonstration (SB, SC, RB, SG), pp. 748–764.
- OOPSLA-2017-ChasinsB #execution #reuse #web
- Skip blocks: reusing execution history to accelerate web scripts (SC, RB), p. 28.
- OOPSLA-2018-WangCB #query #reasoning #relational
- Speeding up symbolic reasoning for relational queries (CW, AC, RB), p. 25.
- PLDI-2017-FedyukovichAB #parallel #source code #synthesis
- Gradual synthesis for static parallelization of single-pass array-processing programs (GF, MBSA, RB), pp. 572–585.
- PLDI-2017-WangCB #query #sql
- Synthesizing highly expressive SQL queries from input-output examples (CW, AC, RB), pp. 452–466.
- POPL-2018-ChandraB #named #reasoning #type system
- Bonsai: synthesis-based reasoning for type systems (KC, RB), p. 34.
- POPL-2020-WangFBCD #visualisation
- Visualization by example (CW, YF, RB, AC, ID), p. 28.
- ASPLOS-2016-PhothilimthanaT #scalability
- Scaling up Superoptimization (PMP, AT0, RB, DD), pp. 297–310.
- ASPLOS-2019-PhothilimthanaE #data flow #gpu #kernel #synthesis
- Swizzle Inventor: Data Movement Synthesis for GPU Kernels (PMP, ASE, AW0, AJ, BH, HB, SJK, VG, ET, RB), pp. 65–78.