Travelled to:1 × Austria
1 × Canada
1 × Croatia
1 × Cyprus
1 × Estonia
1 × Hungary
1 × India
1 × Italy
2 × China
2 × United Kingdom
28 × USA
3 × France
Collaborated with:I.Dillig T.Dillig R.Sharma R.S.0001 M.Sagiv S.Anand E.Schkufza O.Bastani M.Bauer B.Hackett A.V.Nori M.Naik B.R.Churchill S.Bansal S.Treichler P.Hanrahan L.Clapp P.Hawkins N.G.Bronson P.Liang Wonyeol Lee 0001 K.Fisher M.C.Rinard J.Vitek G.Golan-Gueta J.Kodumal T.Terauchi E.Yahav Z.DeVito G.Ramalingam S.Gupta B.Hariharan D.Terei S.Goldsmith D.S.Wilkerson J.Whaley O.Shacham M.T.Vechev Y.Feng K.L.McMillan J.M.Tamayo J.Clark S.Heule O.Padon J. F. Bastien M.Houston J.Y.Park M.Ren T.J.Knight K.Fatahalian W.J.Dally O.Ziv D.Ritchie M.Fisher J.Hegarty A.X.Zheng M.I.Jordan B.Liblit Elliott Slaughter Manolis Papadakis Gilbert Louis Bernstein S.Bugrara M.Erez
Talks about:program (10) use (10) data (7) superoptim (5) analysi (5) static (5) memori (5) invari (5) infer (5) perform (4)
Person: Alex Aiken
DBLP: Aiken:Alex
Facilitated 2 volumes:
EdEdContributed to:
2015
2015
20152015
2014
2014
2014201420142014
2014
2013
201320132013
201320122012201220122011
201120112011201120112010201020102009
2008200820082007
200720072007200720062006
2006
20062006201620162017
2019201620172018201820192017Wrote 63 papers:
- ISSTA-2015-ClappAA #data flow #mining #named #specification
- Modelgen: mining explicit information flow specifications from concrete executions (LC, SA, AA), pp. 129–140.
- OOPSLA-2015-0001SCA
- Conditionally correct superoptimization (RS, ES, BRC, AA), pp. 147–162.
- OOPSLA-2015-BastaniAA #android #data flow #verification
- Interactively verifying absence of explicit information flows in Android apps (OB, SA, AA), pp. 299–315.
- PLDI-2015-SharmaBA #gpu #source code #verification
- Verification of producer-consumer synchronization in GPU programs (RS, MB, AA), pp. 88–98.
- PLDI-2015-ZivAGRS #concurrent
- Composing concurrency control (OZ, AA, GGG, GR, MS), pp. 240–249.
- POPL-2015-BastaniAA #context-free grammar #reachability #specification #using
- Specification Inference Using Context-Free Language Reachability (OB, SA, AA), pp. 553–566.
- CAV-2014-0001A #invariant #random #using
- From Invariant Checking to Invariant Inference Using Randomized Search (RS, AA), pp. 88–105.
- FSE-2014-FengADA #android #detection #named #semantics #static analysis
- Apposcopy: semantics-based detection of Android malware through static analysis (YF, SA, ID, AA), pp. 576–587.
- ISMM-2014-TereiAV #component #memory management #named #off the shelf
- M3: high-performance memory management from off-the-shelf components (DT, AA, JV), pp. 3–13.
- ISSTA-2014-ShachamYGABSV #independence #verification
- Verifying atomicity via data independence (OS, EY, GGG, AA, NGB, MS, MTV), pp. 26–36.
- PLDI-2014-DeVitoRFAH #generative #runtime #using
- First-class runtime generation of high-performance types using exotypes (ZD, DR, MF, AA, PH), p. 11.
- PLDI-2014-Schkufza0A #float #optimisation #precise #probability #source code
- Stochastic optimization of floating-point programs with tunable precision (ES, RS, AA), p. 9.
- POPL-2014-SharmaNA #program analysis #trade-off
- Bias-variance tradeoffs in program analysis (RS, AVN, AA), pp. 127–138.
- PPoPP-2014-BauerTA #named #performance
- Singe: leveraging warp specialization for high performance on GPUs (MB, ST, AA), pp. 119–130.
- ASPLOS-2013-Schkufza0A #probability
- Stochastic superoptimization (ES, RS, AA), pp. 305–316.
- ESOP-2013-SharmaGHALN #algebra #approach #data-driven #invariant
- A Data Driven Approach for Algebraic Loop Invariants (RS, SG, BH, AA, PL, AVN), pp. 574–592.
- OOPSLA-2013-SharmaSCA #data-driven #equivalence
- Data-driven equivalence checking (RS, ES, BRC, AA), pp. 391–406.
- OOPSLA-2013-TreichlerBA #clustering
- Language support for dynamic, hierarchical data partitioning (ST, MB, AA), pp. 495–514.
- PLDI-2013-DeVitoHAHV #multi #named
- Terra: a multi-stage language for high-performance computing (ZD, JH, AA, PH, JV), pp. 105–116.
- SAS-2013-0001GHAN #concept #geometry #learning #verification
- Verification as Learning Geometric Concepts (RS, SG, BH, AA, AVN), pp. 388–411.
- CAV-2012-DilligDMA #smt
- Minimum Satisfying Assignments for SMT (ID, TD, KLM, AA), pp. 394–409.
- CAV-2012-SharmaNA #classification
- Interpolants as Classifiers (RS, AVN, AA), pp. 71–87.
- ESOP-2012-HawkinsAFRS #reasoning
- Reasoning about Lock Placements (PH, AA, KF, MCR, MS), pp. 336–356.
- OOPSLA-2012-TamayoABS #behaviour #comprehension #database
- Understanding the behavior of database operations under program control (JMT, AA, NGB, MS), pp. 983–996.
- PLDI-2012-DilligDA #abduction #automation #fault #using
- Automated error diagnosis using abductive inference (ID, TD, AA), pp. 181–192.
- PLDI-2012-HawkinsAFRS #concurrent #data transformation #representation #synthesis
- Concurrent data representation synthesis (PH, AA, KF, MCR, MS), pp. 417–428.
- CAV-2011-SharmaDDA #generative #invariant #using
- Simplifying Loop Invariant Generation Using Splitter Predicates (RS, ID, TD, AA), pp. 703–719.
- ESEC-FSE-2011-HackettA #morphism #polymorphism
- Inferring data polymorphism in systems code (BH, AA), pp. 332–342.
- OOPSLA-2011-Golan-GuetaBARSY #automation #using
- Automatic fine-grain locking using shape properties (GGG, NGB, AA, GR, MS, EY), pp. 225–242.
- OOPSLA-2011-ShachamBASVY #concurrent #testing
- Testing atomicity of composed concurrent operations (OS, NGB, AA, MS, MTV, EY), pp. 51–64.
- PLDI-2011-DilligDAS #composition #precise #source code #summary
- Precise and compact modular procedure summaries for heap manipulating programs (ID, TD, AA, MS), pp. 567–577.
- PLDI-2011-HawkinsAFRS #data transformation #representation #synthesis
- Data representation synthesis (PH, AA, KF, MCR, MS), pp. 38–49.
- POPL-2011-DilligDA #precise #reasoning #source code #using
- Precise reasoning for programs using containers (ID, TD, AA), pp. 187–200.
- PPoPP-2011-BauerCSA #memory management #parallel #programming
- Programming the memory hierarchy revisited: supporting irregular parallelism in sequoia (MB, JC, ES, AA), pp. 13–24.
- ESOP-2010-DilligDA
- Fluid Updates: Beyond Strong vs. Weak Updates (ID, TD, AA), pp. 246–266.
- OOPSLA-2010-DilligDA #abstraction #axiom #invariant #memory management
- Symbolic heap abstraction with demand-driven axiomatization of memory invariants (ID, TD, AA), pp. 397–410.
- SAS-2010-DilligDA #constraints #online #scalability #source code #static analysis
- Small Formulas for Large Programs: On-Line Constraint Simplification in Scalable Static Analysis (ID, TD, AA), pp. 236–252.
- CAV-2009-DilligDA #integer #linear #proving
- Cuts from Proofs: A Complete and Practical Technique for Solving Linear Inequalities over Integers (ID, TD, AA), pp. 233–247.
- OSDI-2008-BansalA #using
- Binary Translation Using Peephole Superoptimizers (SB, AA), pp. 177–192.
- PLDI-2008-DilligDA #analysis #scalability
- Sound, complete and scalable path-sensitive analysis (ID, TD, AA), pp. 270–280.
- PPoPP-2008-HoustonPRKFADH #interface #memory management #multi #runtime
- A portable runtime interface for multi-level memory hierarchies (MH, JYP, MR, TJK, KF, AA, WJD, PH), pp. 143–152.
- ESEC-FSE-2007-GoldsmithAW #complexity #empirical
- Measuring empirical computational complexity (SG, AA, DSW), pp. 395–404.
- PASTE-2007-AikenBDDHH #overview
- An overview of the saturn project (AA, SB, ID, TD, BH, PH), pp. 43–48.
- PLDI-2007-DilligDA #consistency #detection #fault #nondeterminism #semantics #using
- Static error detection using semantic inconsistency inference (ID, TD, AA), pp. 435–445.
- PLDI-2007-KodumalA #constraints #set
- Regularly annotated set constraints (JK, AA), pp. 331–341.
- POPL-2007-NaikA #alias #concurrent #detection
- Conditional must not aliasing for static race detection (MN, AA), pp. 327–338.
- PPoPP-2007-KnightPRHEFADH #compilation #memory management
- Compilation for explicitly managed memory hierarchies (TJK, JYP, MR, MH, ME, KF, AA, WJD, PH), pp. 226–236.
- ASPLOS-2006-BansalA #automation #generative
- Automatic generation of peephole superoptimizers (SB, AA), pp. 394–403.
- FSE-2006-HackettA #alias #how #question
- How is aliasing used in systems software? (BH, AA), pp. 69–80.
- ICML-2006-ZhengJLNA #debugging #identification #multi #statistics
- Statistical debugging: simultaneous identification of multiple bugs (AXZ, MIJ, BL, MN, AA), pp. 1105–1112.
- LICS-2006-TerauchiA #on the #polymorphism #recursion
- On Typability for Rank-2 Intersection Types with Polymorphic Recursion (TT, AA), pp. 111–122.
- PLDI-2006-NaikAW #concurrent #detection #effectiveness #java
- Effective static race detection for Java (MN, AA, JW), pp. 308–319.
- FSE-2016-ClappBAA #user interface
- Minimizing GUI event traces (LC, OB, SA, AA), pp. 422–434.
- OOPSLA-2016-TreichlerBSSA #clustering
- Dependent partitioning (ST, MB, RS0, ES, AA), pp. 344–358.
- OOPSLA-2017-PapadakisB0AH #graph #named
- Seam: provably safe local edits on graphs (MP, GLB, RS0, AA, PH), p. 29.
- ECOOP-2019-Bastani0CAA #analysis #points-to #specification
- Eventually Sound Points-To Analysis with Specifications (OB, RS0, LC, SA, AA), p. 28.
- PLDI-2016-HeuleS0A #automation #learning #set #synthesis
- Stratified synthesis: automatically learning the x86-64 instruction set (SH, ES, RS0, AA), pp. 237–250.
- PLDI-2016-LeeSA #float #verification
- Verifying bit-manipulations of floating-point (WL0, RS0, AA), pp. 70–84.
- PLDI-2017-Bastani0AL
- Synthesizing program input grammars (OB, RS0, AA, PL), pp. 95–110.
- PLDI-2018-Bastani0AL #learning #points-to #specification
- Active learning of points-to specifications (OB, RS0, AA, PL), pp. 678–692.
- POPL-2018-Lee0A #automation #correctness #implementation #on the #proving
- On automatically proving the correctness of math.h implementations (WL0, RS0, AA), p. 32.
- PLDI-2019-ChurchillP0A #equivalence #semantics
- Semantic program alignment for equivalence checking (BRC, OP, RS0, AA), pp. 1027–1040.
- ASPLOS-2017-ChurchillSBA
- Sound Loop Superoptimization for Google Native Client (BRC, RS0, JFB, AA), pp. 313–326.