Export Citations
Save this search
Please login to be able to save your searches and receive alerts for new content matching your search criteria.
- research-articleJune 2022
DISTAL: the distributed tensor algebra compiler
PLDI 2022: Proceedings of the 43rd ACM SIGPLAN International Conference on Programming Language Design and ImplementationJune 2022, Pages 286–300https://doi.org/10.1145/3519939.3523437We introduce DISTAL, a compiler for dense tensor algebra that targets modern distributed and heterogeneous systems. DISTAL lets users independently describe how tensors and computation map onto target machines through separate format and scheduling ...
Quartz: superoptimization of Quantum circuits
- Mingkuan Xu,
- Zikun Li,
- Oded Padon,
- Sina Lin,
- Jessica Pointing,
- Auguste Hirth,
- Henry Ma,
- Jens Palsberg,
- Alex Aiken,
- Umut A. Acar,
- Zhihao Jia
PLDI 2022: Proceedings of the 43rd ACM SIGPLAN International Conference on Programming Language Design and ImplementationJune 2022, Pages 625–640https://doi.org/10.1145/3519939.3523433Existing quantum compilers optimize quantum circuits by applying circuit transformations designed by experts. This approach requires significant manual effort to design and implement circuit transformations for different quantum devices, which use ...
- research-articleJune 2021
Adaptive restarts for stochastic synthesis
PLDI 2021: Proceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and ImplementationJune 2021, Pages 696–709https://doi.org/10.1145/3453483.3454071We consider the problem of program synthesis from input-output examples via stochastic search. We identify a robust feature of stochastic synthesis: The search often progresses through a series of discrete plateaus. We observe that the distribution of ...
- research-articleJune 2020
First-order quantified separators
PLDI 2020: Proceedings of the 41st ACM SIGPLAN Conference on Programming Language Design and ImplementationJune 2020, Pages 703–717https://doi.org/10.1145/3385412.3386018Quantified first-order formulas, often with quantifier alternations, are increasingly used in the verification of complex systems. While automated theorem provers for first-order logic are becoming more robust, invariant inference tools that handle ...
Semantic program alignment for equivalence checking
PLDI 2019: Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and ImplementationJune 2019, Pages 1027–1040https://doi.org/10.1145/3314221.3314596We introduce a robust semantics-driven technique for program equivalence checking. Given two functions we find a trace alignment over a set of concrete executions of both programs and construct a product program particularly amenable to checking ...
-
- research-articleJune 2018
Active learning of points-to specifications
PLDI 2018: Proceedings of the 39th ACM SIGPLAN Conference on Programming Language Design and ImplementationJune 2018, Pages 678–692https://doi.org/10.1145/3192366.3192383When analyzing programs, large libraries pose significant challenges to static points-to analysis. A popular solution is to have a human analyst provide points-to specifications that summarize relevant behaviors of library code, which can substantially ...
Also Published in:
ACM SIGPLAN Notices: Volume 53 Issue 4, April 2018 - research-articleJune 2017
Synthesizing program input grammars
PLDI 2017: Proceedings of the 38th ACM SIGPLAN Conference on Programming Language Design and ImplementationJune 2017, Pages 95–110https://doi.org/10.1145/3062341.3062349We present an algorithm for synthesizing a context-free grammar encoding the language of valid program inputs from a set of input examples and blackbox access to the program. Our algorithm addresses shortcomings of existing grammar inference algorithms,...
Also Published in:
ACM SIGPLAN Notices: Volume 52 Issue 6, June 2017 - research-articleJune 2016
Stratified synthesis: automatically learning the x86-64 instruction set
PLDI '16: Proceedings of the 37th ACM SIGPLAN Conference on Programming Language Design and ImplementationJune 2016, Pages 237–250https://doi.org/10.1145/2908080.2908121The x86-64 ISA sits at the bottom of the software stack of most desktop and server software. Because of its importance, many software analysis and verification tools depend, either explicitly or implicitly, on correct modeling of the semantics of x86-...
Also Published in:
ACM SIGPLAN Notices: Volume 51 Issue 6, June 2016 - research-articleJune 2016
Verifying bit-manipulations of floating-point
PLDI '16: Proceedings of the 37th ACM SIGPLAN Conference on Programming Language Design and ImplementationJune 2016, Pages 70–84https://doi.org/10.1145/2908080.2908107Reasoning about floating-point is difficult and becomes only more so if there is an interplay between floating-point and bit-level operations. Even though real-world floating-point libraries use implementations that have such mixed computations, no ...
Also Published in:
ACM SIGPLAN Notices: Volume 51 Issue 6, June 2016 - research-articleJune 2015
Composing concurrency control
PLDI '15: Proceedings of the 36th ACM SIGPLAN Conference on Programming Language Design and ImplementationJune 2015, Pages 240–249https://doi.org/10.1145/2737924.2737970Concurrency control poses significant challenges when composing computations over multiple data-structures (objects) with different concurrency-control implementations. We formalize the usually desired requirements (serializability, abort-safety, ...
Also Published in:
ACM SIGPLAN Notices: Volume 50 Issue 6, June 2015 - research-articleJune 2015
Verification of producer-consumer synchronization in GPU programs
PLDI '15: Proceedings of the 36th ACM SIGPLAN Conference on Programming Language Design and ImplementationJune 2015, Pages 88–98https://doi.org/10.1145/2737924.2737962Previous efforts to formally verify code written for GPUs have focused solely on kernels written within the traditional data-parallel GPU programming model. No previous work has considered the higher performance, but more complex, warp-specialized ...
Also Published in:
ACM SIGPLAN Notices: Volume 50 Issue 6, June 2015 - research-articleJune 2014
First-class runtime generation of high-performance types using exotypes
PLDI '14: Proceedings of the 35th ACM SIGPLAN Conference on Programming Language Design and ImplementationJune 2014, Pages 77–88https://doi.org/10.1145/2594291.2594307We introduce exotypes, user-defined types that combine the flexibility of meta-object protocols in dynamically-typed languages with the performance control of low-level languages. Like objects in dynamic languages, exotypes are defined programmatically ...
Also Published in:
ACM SIGPLAN Notices: Volume 49 Issue 6, June 2014 - research-articleJune 2014
Stochastic optimization of floating-point programs with tunable precision
PLDI '14: Proceedings of the 35th ACM SIGPLAN Conference on Programming Language Design and ImplementationJune 2014, Pages 53–64https://doi.org/10.1145/2594291.2594302The aggressive optimization of floating-point computations is an important problem in high-performance computing. Unfortunately, floating-point instruction sets have complicated semantics that often force compilers to preserve programs as written. We ...
Also Published in:
ACM SIGPLAN Notices: Volume 49 Issue 6, June 2014 - research-articleJune 2013
Terra: a multi-stage language for high-performance computing
PLDI '13: Proceedings of the 34th ACM SIGPLAN Conference on Programming Language Design and ImplementationJune 2013, Pages 105–116https://doi.org/10.1145/2491956.2462166High-performance computing applications, such as auto-tuners and domain-specific languages, rely on generative programming techniques to achieve high performance and portability. However, these systems are often implemented in multiple disparate ...
Also Published in:
ACM SIGPLAN Notices: Volume 48 Issue 6, June 2013 - research-articleJune 2012
Concurrent data representation synthesis
PLDI '12: Proceedings of the 33rd ACM SIGPLAN Conference on Programming Language Design and ImplementationJune 2012, Pages 417–428https://doi.org/10.1145/2254064.2254114We describe an approach for synthesizing data representations for concurrent programs. Our compiler takes as input a program written using concurrent relations and synthesizes a representation of the relations as sets of cooperating data structures as ...
Also Published in:
ACM SIGPLAN Notices: Volume 47 Issue 6, June 2012 - research-articleJune 2012
Automated error diagnosis using abductive inference
PLDI '12: Proceedings of the 33rd ACM SIGPLAN Conference on Programming Language Design and ImplementationJune 2012, Pages 181–192https://doi.org/10.1145/2254064.2254087When program verification tools fail to verify a program, either the program is buggy or the report is a false alarm. In this situation, the burden is on the user to manually classify the report, but this task is time-consuming, error-prone, and does ...
Also Published in:
ACM SIGPLAN Notices: Volume 47 Issue 6, June 2012 - research-articleJune 2011
Precise and compact modular procedure summaries for heap manipulating programs
PLDI '11: Proceedings of the 32nd ACM SIGPLAN Conference on Programming Language Design and ImplementationJune 2011, Pages 567–577https://doi.org/10.1145/1993498.1993565We present a strictly bottom-up, summary-based, and precise heap analysis targeted for program verification that performs strong updates to heap locations at call sites. We first present a theory of heap decompositions that forms the basis of our ...
Also Published in:
ACM SIGPLAN Notices: Volume 46 Issue 6, June 2011 - research-articleJune 2011
Data representation synthesis
PLDI '11: Proceedings of the 32nd ACM SIGPLAN Conference on Programming Language Design and ImplementationJune 2011, Pages 38–49https://doi.org/10.1145/1993498.1993504We consider the problem of specifying combinations of data structures with complex sharing in a manner that is both declarative and results in provably correct code. In our approach, abstract data types are specified using relational algebra and ...
Also Published in:
ACM SIGPLAN Notices: Volume 46 Issue 6, June 2011 - proceedingJune 2010
PLDI '10: Proceedings of the 31st ACM SIGPLAN Conference on Programming Language Design and Implementation
We are pleased to present the proceedings of the ACM SIGPLAN 2010 Conference on Programming Language Design and Implementation. PLDI addresses all issues relevant to the design of programming languages, the theory and practice of associated software ...