Pith. sign in

REVIEW 4 major objections 4 minor 45 references

Type-Directed Program Synthesis and Constraint Generation for Library Portability

T0 review · 4 major / 4 minor · reviewed 2026-08-14 · deepseek-v4-flash

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗ Review JSON

Pith's one-line read A compiler can learn black-box numerical libraries from samples and type annotations, then find equivalent code sections and suggest replacements with newer accelerator libraries.

desk verdict A practical, honestly-limited systems paper: real speedups from synthesizing black-box library behavior and generalizing constraints, though 'equivalent' overclaims what sampling-based checks can support. read the letter →

arxiv 1908.04546 v3 pith:S6IRJFYI submitted 2019-08-13 cs.PL cs.PF

Bruce Collie , Philip Ginsbach , Michael F.P. O'Boyle This is my paper · ORCID
classification cs.PLcs.PF
keywords programsynthesislibraryportabilityconstraintgenerationbehavioralequivalencegraphmatchingacceleratorlibrariesAPImigrationtypeannotations
verification ladder T0 review T1 audit T2 compute T3 formal

The pith

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The reading

This paper claims that a program can be ported from one numerical library to a newer accelerator library even when neither library's source code is available. The compiler side learns a library's behavior by synthesizing an implementation from its type signature, lightweight vendor annotations, and input/output examples, then turns several synthesized implementations into a generalized constraint pattern. That pattern is used to search the user's program for code that behaves the same way, and the discovered sections are presented as replacements. The paper reports that adopting the suggested replacements improves end-to-end performance of large scientific and deep-learning programs by 1.1x to over 10x. If the claim holds, developers can keep pace with rapidly changing accelerator libraries without rewriting or maintaining multiple versions of their code.

What carries the argument

The load-bearing object is the instruction graph together with the equivalence relation that merges nodes across different synthesized versions. Each synthesized program in static single assignment form becomes a graph $G=(V,E)$ with edges $a \xrightarrow{n} b$ meaning instruction $a$ is the $n$-th argument of instruction $b$; an equivalence relation $\sim$ on vertices is scored by a metric that rewards merging similar instructions and punishes mismatched opcodes and broken argument relations. Optimizing that metric with an evolutionary search produces a quotient graph whose surviving, frequently occurring classes define the generalized constraints. This is what lets the system move from one accidental synthesized implementation to a pattern broad enough to match real user code.

What would settle it

Run the original library and the synthesized replacement on inputs that are not drawn from the random sample distribution, such as zero-length arrays, NaNs or infinities, negative strides, and size arguments at the limit of the data type; one observable difference in output on such an input disproves the claimed behavioral equivalence for that candidate.

Watch

Extended reading notes

Core claim

On its own terms, the paper's discovery is a complete pipeline from black-box library to replacement suggestion. Given a library function's type signature and a handful of annotations, which arguments point to memory, how large, and which are outputs, the system composes small control-flow fragments into candidate programs, fills them with stochastically sampled arithmetic instructions, and keeps the first candidate that matches the library on random input/output tests. Multiple such synthesized programs are then represented as graphs whose nodes are instructions and whose edges record argument relationships; an equivalence relation computed by maximizing a metric merges corresponding nodes across graphs, and equivalence classes that appear too rarely are discarded. The surviving structure is emitted as a generalized constraint description, and a satisfiability-solver-based search finds user-code regions satisfying the constraints. The system maps those regions back to source locations and proposes a call to the new library, subject to developer sign-off and a dynamic output check.

Load-bearing premise

The system only checks that a synthesized replacement agrees with the original library on a large random sample of inputs, so the whole method rests on the assumption that agreement on those samples means agreement on every input the program will actually encounter.

Editorial extensions

If this is right

  • A program whose only link to a vendor library is through calls or inlined copies can be migrated to a different accelerator library without a human writing a semantic model by hand.
  • Porting to new hardware is a matter of pointing the pipeline at a library for that hardware: the paper demonstrates moving a neural-network framework to an OpenCL-based BLAS library on a machine that does not support the original vendor GPU API.
  • Because the constraints are generated from multiple synthesized examples, the matcher can recognize code that is not textually identical, including hand-written loops and inlined library bodies.
  • The replacement suggestions are filtered by running the old and new code on the same inputs before presentation, so the developer only signs off on candidates that already agree on observed examples.
  • On the evaluated scientific and deep-learning workloads, applying the suggested replacements yields end-to-end speedups from roughly 1.1x to more than 10x.

Reading between the lines

Editorial extensions of the paper, not claims the author makes directly.

  • A natural extension the paper only gestures at is replacing the random-sample check with a solver-based equivalence proof for the synthesized candidate, which would turn the proposed refactoring into a verified compiler transformation.
  • The same graph-matching generalization could be applied in the reverse direction: mine existing codebases for repeated computational idioms and recommend library calls for patterns that are not yet tied to any library, rather than only migrating code away from an old API.
  • Since the metric weights in the matching step were hand-tuned for the evaluated kernels, applying the approach to a different domain may require re-tuning; learning those weights from labeled matches is a plausible, testable improvement.
  • The reported speedups are end-to-end but measured after a developer accepted the suggested replacements, so practical gain also depends on how often the synthesis step fails, as it did for the softmax numerical trick.
Share X Bluesky LinkedIn Reddit HN

Signed reviews

No signed human review yet.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, and a circularity audit.

Referee Report

4 major / 4 minor

Summary. The paper presents a system for library portability that combines oracle-guided program synthesis with constraint-based matching. Given only a library's type signature plus lightweight vendor-supplied annotations, the system synthesizes LLVM IR implementations of black-box library functions from random input/output examples. It then generalizes multiple synthesized implementations into IDL constraints via a graph-matching algorithm and uses an SMT-based search (carried over from prior work) to locate matching code sections in user applications, suggesting replacements that use new accelerator libraries. The system is evaluated on NWChem, Abinit, Pathsample, Darknet, and Parboil, targeting Intel MKL, NVIDIA CUDA libraries, and CLBlast, with reported end-to-end speedups from 1.1x to over 10x. The paper claims that the system can 'recover equivalent code' from existing programs and automatically port them to new library interfaces.

Significance. The problem addressed is real and timely: scientific and deep-learning code bases are increasingly tied to vendor-specific numerical libraries, and porting them to new accelerator APIs is labor-intensive. The proposed pipeline, from synthesized library models to automatically generalized constraints, is a plausible and practical way to assist developers in this process. The evaluation is grounded in large, widely used applications and reports genuine end-to-end speedups, not just microbenchmark gains. The paper is also unusually honest about its limitations: it explicitly acknowledges that the correctness notion is unsound, that false positives occur in matching, and that some functions (e.g., SOFTMAX) cannot be synthesized with the current fragment set. The two main contributions, oracle-guided LLVM synthesis with annotated signatures and automatic constraint generalization from examples, are concrete and potentially reusable.

major comments (4)
  1. [Section IV-E and Abstract] The central correctness notion is load-bearing for the paper's main claim, but it is explicitly unsound. Section IV-E defines correct(s) as s(x_i) approximately equal to r(x_i) on a set of random sample inputs and immediately states that 'this correctness decision is unsound.' All downstream steps, including constraint generalization and replacement suggestion, inherit this limitation. The evaluation confirms that the risk is real rather than theoretical: Section VII-E and Table III record false positive matches for SCAL and COPY in NWChem and Darknet under generalized constraints, and Section VII-F lists random I/O sampling as a source of unsound behavior. The dynamic testing used to eliminate false positives is applied per candidate and itself depends on the same sampling assumption; no end-to-end differential check of the transformed applications on their actual inputs is reported. Consequently, the abstract's claims that the system 'can recover equivalent code' and 'automatically port them to new interfaces' outstrip what is verified. The authors should either temper these claims to 'candidate replacements' that the developer signs off on, or add an evaluation that checks behavioral equivalence of the transformed binaries on the benchmark inputs (and report the results).
  2. [Section VII-E, Table III] The evaluation required a post-hoc 'nested loop correction' for the system to detect GEMM, GEMV, and SPMV at all. The text says that these kernels 'were not discovered by the generalized constraints' and that 'a mechanical post-processing step fixed these constraints' after the authors discovered a consistent difference between Clang's code generator and the synthesizer. This is a post-hoc repair identified during evaluation, not a designed feature of the approach. Since the reported speedups depend heavily on detecting dense linear algebra kernels, the paper should specify exactly what the post-processing step does, why it is generally applicable beyond the three kernels, and how it interacts with the claimed automaticity of constraint generation. Without this, the claim that the system generally recovers library-like code from user programs is not established.
  3. [Section V-B] The generalization metric in Section V-B depends on five parameters p1 through p5, and the text states that 'by trial and error we assigned the following values': p1 = 1.0, p2 = 0.5, p3 = 0.5, p4 = 0.5. The value of p5 is omitted, and no sensitivity analysis is provided. Because the constraint generalization is one of the paper's two main contributions, the lack of any evaluation of how sensitive matches are to these hand-tuned weights makes it difficult to assess the generality of the approach. At minimum, the authors should report p5, describe the range of values tried, and show that the matching results (Table III) are stable to reasonable variations in the weights.
  4. [Section III-D and VII-E] The practical workflow relies on the developer signing off on each replacement and on dynamic testing to eliminate false positives, but the evaluation does not quantify this burden. Table III reports only the final TP/FP/FN counts after false-positive testing; it does not report how many candidates were dynamically tested and rejected before the accepted replacements were identified, nor how much developer time was involved. Since the paper claims to reduce developer burden, it should at least report the number of candidates considered per application and the number of false positives that were caught by dynamic testing before the authors were left with the correct replacements.
minor comments (4)
  1. [Section VI-A] The text contains a typo: 'hese are significant applications' should read 'These are significant applications.'
  2. [Table III caption and Section VII-E] The caption of Table III explains that results are quoted as x/y/z/w for the four algorithm versions, but Section VII-E describes the four versions only in words. The mapping between the four versions and the four positions in the tuples should be stated explicitly in the text to make the table readable.
  3. [Section V-B] In the metric definition, p5 appears as an additive constant but its value is never listed with the other parameters. Please provide its assigned value or remove it from the metric.
  4. [Algorithm 1 and Section IV-C] Algorithm 1 samples n instructions at each dataflow block, but n is never defined or discussed. Please state how n is chosen and whether it varies across the evaluated functions.

Circularity Check

0 steps flagged · score 0.0 of 10

No circular derivation: new synthesis and constraint-generation contributions are validated against external libraries and applications, with acknowledged approximate equivalence not presented as a formal derivation.

full rationale

The paper's central chain is: synthesize library implementations from vendor annotations and IO examples; generalize several synthesized IRs into IDL constraints; search user code with the IDL/SMT matcher; present matches for developer sign-off; and measure end-to-end speedups after replacement. None of these steps reduces to its own input. The synthesis stage uses oracle-guided testing, and Section IV-E explicitly defines correct(s) by sampled input/output agreement and states 'This correctness decision is unsound; there is no way to establish formally that a candidate program will behave correctly on every possible input.' This is a candid soundness limitation, not a circular definition of the contribution. The constraint-generalization metric weights in Section V-B are hand-tuned constants, not fitted to the reported speedups. The IDL/SMT machinery from [13] is prior work by overlapping authors, but the paper explicitly restricts its contribution to the library-centric phases in Section III-C and treats IDL as a black box; the new results are evaluated against external applications (NWChem, Abinit, Pathsample, Darknet, Parboil) with hand-identified ground-truth matches and measured performance, not against the cited work's outputs. The reported false positives for SCAL/COPY and the unlearned SOFTMAX are presented as limitations and addressed by dynamic testing, again without any fitted quantity being renamed as a prediction. Overall, the derivation is self-contained with respect to the paper's new claims, and the self-citation is not load-bearing.

Assumptions & free parameters 4 free parameters · 5 assumptions · 0 invented entities

The central claim rests on several unstated or weakly supported premises: random I/O equivalence, annotation completeness, fragment coverage, approximate graph matching, and the correctness of prior IDL search. Free parameters are either unspecified (I/O sample set, instruction count n) or hand-tuned (metric weights p1..p4). The fragment set is not fully enumerated and is known to be incomplete (SOFTMAX). No invented entities are introduced.

free parameters (4)
  • matching metric weights p1..p4 = p1=1.0, p2=0.5, p3=0.5, p4=0.5; p5 unspecified
    Chosen by trial and error in Section V-B2; they determine how aggressively IR nodes are merged into equivalence classes and hence which generalized constraints are generated.
  • random I/O sample set for behavioral equivalence = not specified
    Section IV-E defines correctness as equality on all sampled inputs but does not state sample count, distribution, or seed; equivalence strength is therefore undefined.
  • instruction sampling count n in Algorithm 1 = not specified
    Algorithm 1 takes parameter n for the number of instructions sampled per dataflow block; no default or range is given.
  • max fragment composition count = 3
    Section IV-C3: exhaustive search over compositions of up to 3 fragments, with random sampling if no solution; this bound is a design choice that limits the learned program space.
assumptions (5)
  • domain assumption Randomized input/output testing is sufficient to establish behavioral equivalence for library functions.
    Section IV-E states the correctness decision is unsound; the entire replacement pipeline inherits this assumption.
  • domain assumption Vendor annotations (size, output, enum, pack, indices) accurately capture the semantic information needed for synthesis and can be extracted from documentation.
    Section IV-A/B relies on these annotations to constrain control-flow and memory behavior; if annotations are incomplete, synthesis may fail or produce wrong programs.
  • ad hoc to paper The set of hand-written control-flow fragments and heuristics covers the implementations of the target library functions.
    Section IV-C says fragments are composed to synthesize programs; the paper lists only examples, not the full fragment set. SOFTMAX is not learned (Section VII-E), evidence the coverage is incomplete.
  • domain assumption Graph matching with the hand-tuned metric approximates semantic equivalence of LLVM IR instructions.
    Section V-B checks opcode equality and argument relations but is explicitly an approximate metric; false positives and negatives are observed (Section VII-E).
  • domain assumption The IDL constraint language and SMT search from prior work [13] are correct as used.
    Section V-D treats the SMT search as a black box from earlier papers by the same group; no verification is provided.

how reviews work

0 comments
Cite this review

Pith. "Pith review of Type-Directed Program Synthesis and Constraint Generation for Library Portability." pith.science (2026). https://pith.science/paper/S6IRJFYI

@misc{pith2026190804546,
  author       = {Pith},
  title        = {Pith review of: Type-Directed Program Synthesis and Constraint Generation for Library Portability},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/S6IRJFYI}},
  note         = {Machine review of arXiv:1908.04546}
}
abstract

Fast numerical libraries have been a cornerstone of scientific computing for decades, but this comes at a price. Programs may be tied to vendor specific software ecosystems resulting in polluted, non-portable code. As we enter an era of heterogeneous computing, there is an explosion in the number of accelerator libraries required to harness specialized hardware. We need a system that allows developers to exploit ever-changing accelerator libraries, without over-specializing their code. As we cannot know the behavior of future libraries ahead of time, this paper develops a scheme that assists developers in matching their code to new libraries, without requiring the source code for these libraries. Furthermore, it can recover equivalent code from programs that use existing libraries and automatically port them to new interfaces. It first uses program synthesis to determine the meaning of a library, then maps the synthesized description into generalized constraints which are used to search the program for replacement opportunities to present to the developer. We applied this approach to existing large applications from the scientific computing and deep learning domains. Using our approach, we show speedups ranging from 1.1$\times$ to over 10$\times$ on end to end performance when using accelerator libraries.

Figures

Figures reproduced from arXiv: 1908.04546 by the authors.

Figure 1
Figure 1. Porting BLAS to MKL, managing API evolution. On the left is code taken from NWChem [10], a widely-used chemical [PITH_FULL_IMAGE:figures/full_fig_p002_1.png] view at source ↗
Figure 2
Figure 2. An overview of the data flow through the different stages of our system. Inputs are shown in blue on the left, intermediate [PITH_FULL_IMAGE:figures/full_fig_p003_2.png] view at source ↗
Figure 3
Figure 3. A simplified illustration of how our synthesizer learns [PITH_FULL_IMAGE:figures/full_fig_p004_3.png] view at source ↗
Figures from the paper (4 more)
Figure 4
Figure 4. Figure 4: Generating constraints from synthesized candidates: Our matching algorithm transforms synthesized programs into [PITH_FULL_IMAGE:figures/full_fig_p006_4.png]
Figure 5
Figure 5. Figure 5: Generalizing Constraints: Candidate constraints from two LLVM IR versions of a dot product are matched. The algorithm [PITH_FULL_IMAGE:figures/full_fig_p007_5.png]
Figure 6
Figure 6. Figure 6: Performance achievable by adopting code replacements suggested by our tools, for both Intel MKL and Nvidia CUDA [PITH_FULL_IMAGE:figures/full_fig_p009_6.png]
Figure 7
Figure 7. Figure 7: Performance results for neural network inference on [PITH_FULL_IMAGE:figures/full_fig_p009_7.png]

Discussion (0). Continue with ORCID to comment.

Reference graph

Works this paper leans on

45 extracted references · 25 canonical work pages

  1. [1]

    Portability in scientific computing: The molecular dynamics non-bonded forces calculation as a case study,

    A. Sedova, A. Tharrington, and B. Messer, “Portability in scientific computing: The molecular dynamics non-bonded forces calculation as a case study,” 08 2018

    work page 2018

  2. [2]

    The scalability-efficiency/maintainability- portability trade-off in simulation software engineering: Examples and a preliminary systematic literature review,

    D. Pflüger, M. Mehl, J. Valentin, F. Lindner, D. Pfander, S. Wagner, D. Graziotin, and Y . Wang, “The scalability-efficiency/maintainability- portability trade-off in simulation software engineering: Examples and a preliminary systematic literature review,” in Proceedings of the Fourth International Workshop on Software Engineering for HPC in Computational ...

    work page doi:10.1109/se 2016

  3. [3]

    PyTorch,

    “PyTorch,” https://pytorch.org/

    work page

  4. [4]

    Darknet: Open Source Neural Networks in C,

    J. Redmon, “Darknet: Open Source Neural Networks in C,” 2013. [Online]. Available: http://pjreddie.com/darknet/

    work page 2013

  5. [5]

    NVIDIA cuBLAS,

    “NVIDIA cuBLAS,” https://developer.nvidia.com/cublas

    work page

  6. [6]

    clMathLibraries clBLAS,

    “clMathLibraries clBLAS,” https://github.com/clMathLibraries/clBLAS

    work page

  7. [7]

    NVIDIA cuDNN,

    “NVIDIA cuDNN,” https://developer.nvidia.com/cudnn, 2018

    work page 2018

  8. [8]

    Intel® Compute Library for Deep Neural Networks (clDNN),

    “Intel® Compute Library for Deep Neural Networks (clDNN),” https: //01.org/cldnn

    work page

Show all 45 references
  1. [9]

    Accelerating Search- based Program Synthesis Using Learned Probabilistic Models,

    W. Lee, K. Heo, R. Alur, and M. Naik, “Accelerating Search- based Program Synthesis Using Learned Probabilistic Models,” in Proceedings of the 39th ACM SIGPLAN Conference on Programming Language Design and Implementation , ser. PLDI 2018. New York, NY , USA: ACM, 2018, pp. 436...

    2018

  2. [10]

    NWChem: A comprehensive and scalable open-source solution for large scale molecular simulations,

    M. Valiev, E. J. Bylaska, N. Govind, K. Kowalski, T. P. Straatsma, H. J. J. Van Dam, D. Wang, J. Nieplocha, E. Apra, T. L. Windus, and W. A. de Jong, “NWChem: A comprehensive and scalable open-source solution for large scale molecular simulations,” Computer Physics Communicati...

  3. [11]

    Intel® Math Kernel Library (MKL),

    “Intel® Math Kernel Library (MKL),” https://software.intel.com/mkl

  4. [12]

    A theory of formal synthesis via inductive learning,

    S. Jha and S. A. Seshia, “A theory of formal synthesis via inductive learning,” Acta Informatica , vol. 54, no. 7, pp. 693–726, Nov 2017. [Online]. Available: https://doi.org/10.1007/s00236-017-0294-5

    2017 doi

  5. [13]

    Automatic Matching of Legacy Code to Heterogeneous APIs: An Idiomatic Approach,

    P. Ginsbach, T. Remmelg, M. Steuwer, B. Bodin, C. Dubach, and M. F. P. O’Boyle, “Automatic Matching of Legacy Code to Heterogeneous APIs: An Idiomatic Approach,” in Proceedings of the Twenty-Third International Conference on Architectural Support for Programming Languages and ...

    2018

  6. [14]

    QuickCheck: A Lightweight Tool for Random Testing of Haskell Programs,

    K. Claessen and J. Hughes, “QuickCheck: A Lightweight Tool for Random Testing of Haskell Programs,” in Proceedings of the Fifth ACM SIGPLAN International Conference on Functional Programming , ser. ICFP ’00. New York, NY , USA: ACM, 2000, pp. 268–279. [Online]. Available: http...

  7. [15]

    CAnDL: A Domain Specific Language for Compiler Analysis,

    P. Ginsbach, L. Crawford, and M. F. P. O’Boyle, “CAnDL: A Domain Specific Language for Compiler Analysis,” in Proceedings of the 27th International Conference on Compiler Construction , ser. CC 2018. New York, NY , USA: ACM, 2018, pp. 151–162. [Online]. Available: http://doi.ac...

    2018

  8. [16]

    XNOR-Net: ImageNet Classification Using Binary Convolutional Neural Networks,

    M. Rastegari, V . Ordonez, J. Redmon, and A. Farhadi, “XNOR-Net: ImageNet Classification Using Binary Convolutional Neural Networks,” in Computer Vision – ECCV 2016 , ser. Lecture Notes in Computer Science, B. Leibe, J. Matas, N. Sebe, and M. Welling, Eds. Springer Internationa...

    2016

  9. [17]

    You Only Look Once: Unified, Real-Time Object Detection,

    J. Redmon, S. Divvala, R. Girshick, and A. Farhadi, “You Only Look Once: Unified, Real-Time Object Detection,” in 2016 IEEE Conference on Computer Vision and Pattern Recognition (CVPR) , Jun. 2016, pp. 779–788

    2016

  10. [18]

    YOLO9000: Better, Faster, Stronger,

    J. Redmon and A. Farhadi, “YOLO9000: Better, Faster, Stronger,” in 2017 IEEE Conference on Computer Vision and Pattern Recognition (CVPR), Jul. 2017, pp. 6517–6525

    2017

  11. [19]

    CLBlast: A Tuned OpenCL BLAS Library,

    C. Nugteren, “CLBlast: A Tuned OpenCL BLAS Library,” in Proceedings of the International Workshop on OpenCL , ser. IWOCL ’18. New York, NY , USA: ACM, 2018, pp. 5:1–5:10. [Online]. Available: http://doi.acm.org/10.1145/3204919.3204924

    2018

  12. [20]

    Characterising across-stack optimisations for deep convolutional neural networks,

    J. Turner, J. Cano, V . Radu, E. J. Crowley, M. O’Boyle, and A. Storkey, “Characterising across-stack optimisations for deep convolutional neural networks,” in 2018 IEEE International Symposium on Workload Char- acterization (IISWC), Sep. 2018, pp. 101–110

    2018

  13. [21]

    Synthesis of Loop-free Programs,

    S. Gulwani, S. Jha, A. Tiwari, and R. Venkatesan, “Synthesis of Loop-free Programs,” in Proceedings of the 32Nd ACM SIGPLAN Conference on Programming Language Design and Implementation , ser. PLDI ’11. New York, NY , USA: ACM, 2011, pp. 62–73. [Online]. Available: http://doi.a...

    2011

  14. [22]

    Stochastic Superoptimization,

    E. Schkufza, R. Sharma, and A. Aiken, “Stochastic Superoptimization,” in Proceedings of the Eighteenth International Conference on Architectural Support for Programming Languages and Operating Systems, ser. ASPLOS ’13. New York, NY , USA: ACM, 2013, pp. 305–

    2013

  15. [23]

    Stepping Stones to Inductive Synthesis of Low-Level Looping Programs,

    C. D. Rosin, “Stepping Stones to Inductive Synthesis of Low-Level Looping Programs,” arXiv:1811.10665 [cs], Nov. 2018

    2018 arXiv

  16. [24]

    The role of refactorings in api evolu- tion,

    D. Dig and R. Johnson, “The role of refactorings in api evolu- tion,” in 21st IEEE International Conference on Software Maintenance (ICSM’05). IEEE, 2005, pp. 389–398

    2005

  17. [25]

    How are java software developers using the elipse ide?

    G. C. Murphy, M. Kersten, and L. Findlater, “How are java software developers using the elipse ide?” IEEE software , vol. 23, no. 4, pp. 76–83, 2006

    2006

  18. [26]

    Catchup! capturing and replaying refactorings to support api evolution,

    J. Henkel and A. Diwan, “Catchup! capturing and replaying refactorings to support api evolution,” in Proceedings. 27th International Conference on Software Engineering, 2005. ICSE 2005. IEEE, 2005, pp. 274–283

    2005

  19. [27]

    Apidiff: Detecting api breaking changes,

    A. Brito, L. Xavier, A. Hora, and M. T. Valente, “Apidiff: Detecting api breaking changes,” in 2018 IEEE 25th International Conference on Software Analysis, Evolution and Reengineering (SANER). IEEE, 2018, pp. 507–511

    2018

  20. [28]

    The Sketching Approach to Program Synthesis,

    A. Solar-Lezama, “The Sketching Approach to Program Synthesis,” in Programming Languages and Systems , ser. Lecture Notes in Computer Science. Springer, Berlin, Heidelberg, Dec. 2009, pp. 4–13. [Online]. Available: https://link.springer.com/chapter/10.1007/ 978-3-642-10672-9_3

    2009

  21. [29]

    Synthesis of Recursive ADT Transformations from Reusable Templates,

    J. P. Inala, N. Polikarpova, X. Qiu, B. S. Lerner, and A. Solar- Lezama, “Synthesis of Recursive ADT Transformations from Reusable Templates,” in Tools and Algorithms for the Construction and Analysis of Systems , ser. Lecture Notes in Computer Science, A. Legay and T. Margari...

    2017

  22. [30]

    Modular Synthesis of Sketches Using Models,

    R. Singh, R. Singh, Z. Xu, R. Krosnick, and A. Solar-Lezama, “Modular Synthesis of Sketches Using Models,” in Verification, Model Checking, and Abstract Interpretation , ser. Lecture Notes in Computer Science, K. L. McMillan and X. Rival, Eds. Springer Berlin Heidelberg, 2014, ...

    2014

  23. [31]

    Synthesizing Highly Expressive SQL Queries from Input-output Examples,

    C. Wang, A. Cheung, and R. Bodik, “Synthesizing Highly Expressive SQL Queries from Input-output Examples,” in Proceedings of the 38th ACM SIGPLAN Conference on Programming Language Design and Implementation, ser. PLDI 2017. New York, NY , USA: ACM, 2017, pp. 452–466. [Online]....

    2017 doi

  24. [32]

    Test-driven Synthesis,

    D. Perelman, S. Gulwani, D. Grossman, and P. Provost, “Test-driven Synthesis,” in Proceedings of the 35th ACM SIGPLAN Conference on Programming Language Design and Implementation , ser. PLDI ’14. New York, NY , USA: ACM, 2014, pp. 408–418. [Online]. Available: http://doi.acm.o...

    2014

  25. [33]

    Synthesizing Data Structure Transformations from Input-output Examples,

    J. K. Feser, S. Chaudhuri, and I. Dillig, “Synthesizing Data Structure Transformations from Input-output Examples,” in Proceedings of the 36th ACM SIGPLAN Conference on Programming Language Design and Implementation, ser. PLDI ’15. New York, NY , USA: ACM, 2015, pp. 229–239. [...

    2015 doi

  26. [34]

    Souper: A Synthesizing Superoptimizer,

    R. Sasnauskas, Y . Chen, P. Collingbourne, J. Ketema, G. Lup, J. Taneja, and J. Regehr, “Souper: A Synthesizing Superoptimizer,” arXiv:1711.04422 [cs], Nov. 2017. [Online]. Available: http://arxiv.org/ abs/1711.04422

    2017 arXiv

  27. [35]

    Automating String Processing in Spreadsheets Using Input- output Examples,

    S. Gulwani, “Automating String Processing in Spreadsheets Using Input- output Examples,” in Proceedings of the 38th Annual ACM SIGPLAN- SIGACT Symposium on Principles of Programming Languages , ser. POPL ’11. New York, NY , USA: ACM, 2011, pp. 317–330. [Online]. Available: htt...

    2011

  28. [36]

    Synthesis of Machine Code from Semantics,

    V . Srinivasan and T. Reps, “Synthesis of Machine Code from Semantics,” in Proceedings of the 36th ACM SIGPLAN Conference on Programming Language Design and Implementation , ser. PLDI ’15. New York, NY , USA: ACM, 2015, pp. 596–607. [Online]. Available: http://doi.acm.org/10.1...

    2015

  29. [38]

    Checking Correctness of Code Generator Architecture Specifications,

    N. Hasabnis, R. Qiao, and R. Sekar, “Checking Correctness of Code Generator Architecture Specifications,” in Proceedings of the 13th Annual IEEE/ACM International Symposium on Code Generation and Optimization , ser. CGO ’15. Washington, DC, USA: IEEE Computer Society, 2015, pp....

    2015

  30. [40]

    Gradual Synthesis for Static Parallelization of Single-pass Array-processing Programs,

    G. Fedyukovich, M. B. S. Ahmad, and R. Bodik, “Gradual Synthesis for Static Parallelization of Single-pass Array-processing Programs,” in Proceedings of the 38th ACM SIGPLAN Conference on Programming Language Design and Implementation , ser. PLDI 2017. New York, NY , USA: ACM,...

    2017

  31. [41]

    Helium: Lifting high-performance stencil kernels from stripped x86 binaries to halide dsl code,

    C. Mendis, J. Bosboom, K. Wu, S. Kamil, J. Ragan-Kelley, S. Paris, Q. Zhao, and S. Amarasinghe, “Helium: Lifting high-performance stencil kernels from stripped x86 binaries to halide dsl code,” in ACM SIGPLAN Conference on Programming Language Design and Implementation, Portla...

    2015

  32. [42]

    Halide: A Language and Compiler for Optimizing Parallelism, Locality, and Recomputation in Image Processing Pipelines,

    J. Ragan-Kelley, C. Barnes, A. Adams, S. Paris, F. Durand, and S. Amarasinghe, “Halide: A Language and Compiler for Optimizing Parallelism, Locality, and Recomputation in Image Processing Pipelines,” in Proceedings of the 34th ACM SIGPLAN Conference on Programming Language Des...

    2013

  33. [43]

    Verified Lifting of Stencil Computations,

    S. Kamil, A. Cheung, S. Itzhaky, and A. Solar-Lezama, “Verified Lifting of Stencil Computations,” in Proceedings of the 37th ACM SIGPLAN Conference on Programming Language Design and Implementation , ser. PLDI ’16. New York, NY , USA: ACM, 2016, pp. 711–726. [Online]. Available...

    2016

  34. [44]

    Type-and-example-directed Program Synthesis,

    P.-M. Osera and S. Zdancewic, “Type-and-example-directed Program Synthesis,” in Proceedings of the 36th ACM SIGPLAN Conference on Programming Language Design and Implementation , ser. PLDI ’15. New York, NY , USA: ACM, 2015, pp. 619–630. [Online]. Available: http://doi.acm.org...

    2015

  35. [45]

    Program Synthesis from Polymorphic Refinement Types,

    N. Polikarpova, I. Kuraj, and A. Solar-Lezama, “Program Synthesis from Polymorphic Refinement Types,” in Proceedings of the 37th ACM SIGPLAN Conference on Programming Language Design and Implementation, ser. PLDI ’16. New York, NY , USA: ACM, 2016, pp. 522–538. [Online]. Availa...

    2016 doi

  36. [316]

    Available: http://doi.acm.org/10.1145/2451116.2451150

    [Online]. Available: http://doi.acm.org/10.1145/2451116.2451150

  37. [2010]

    Available: http://www.sciencedirect.com/science/article/ pii/S0010465510001438

    [Online]. Available: http://www.sciencedirect.com/science/article/ pii/S0010465510001438

Pith tools

Reviewed August 14, 2026 · model on record in the stance chip above.