Export Citations
Save this search
Please login to be able to save your searches and receive alerts for new content matching your search criteria.
- proceedingJune 2022
PLDI 2022: Proceedings of the 43rd ACM SIGPLAN International Conference on Programming Language Design and Implementation
Welcome to PLDI 2022, the 43rd ACM SIGPLAN Conference on Programming Language Design and Implementation to be held in San Diego (and online) June 13-17. PLDI is a premier forum for programming language research, broadly interpreted, including design, ...
Type error feedback via analytic program repair
PLDI 2020: Proceedings of the 41st ACM SIGPLAN Conference on Programming Language Design and ImplementationJune 2020, Pages 16–30https://doi.org/10.1145/3385412.3386005We introduce Analytic Program Repair, a data-driven strategy for providing feedback for type-errors via repairs for the erroneous program. Our strategy is based on insight that similar errors have similar repairs. Thus, we show how to use a training ...
Lazy counterfactual symbolic execution
PLDI 2019: Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and ImplementationJune 2019, Pages 411–424https://doi.org/10.1145/3314221.3314618We present counterfactual symbolic execution, a new approach that produces counterexamples that localize the causes of failure of static verification. First, we develop a notion of symbolic weak head normal form and use it to define lazy symbolic ...
FaCT: a DSL for timing-sensitive computation
- Sunjay Cauligi,
- Gary Soeller,
- Brian Johannesmeyer,
- Fraser Brown,
- Riad S. Wahby,
- John Renner,
- Benjamin Grégoire,
- Gilles Barthe,
- Ranjit Jhala,
- Deian Stefan
PLDI 2019: Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and ImplementationJune 2019, Pages 174–189https://doi.org/10.1145/3314221.3314605Real-world cryptographic code is often written in a subset of C intended to execute in constant-time, thereby avoiding timing side channel vulnerabilities. This C subset eschews structured programming as we know it: if-statements, looping constructs, ...
- research-articleJune 2016
Refinement types for TypeScript
PLDI '16: Proceedings of the 37th ACM SIGPLAN Conference on Programming Language Design and ImplementationJune 2016, Pages 310–325https://doi.org/10.1145/2908080.2908110We present Refined TypeScript (RSC), a lightweight refinement type system for TypeScript, that enables static verification of higher-order, imperative programs. We develop a formal system for RSC that delineates the interaction between refinement types ...
Also Published in:
ACM SIGPLAN Notices: Volume 51 Issue 6, June 2016 - research-articleJune 2012
Verifying GPU kernels by test amplification
PLDI '12: Proceedings of the 33rd ACM SIGPLAN Conference on Programming Language Design and ImplementationJune 2012, Pages 383–394https://doi.org/10.1145/2254064.2254110We present a novel technique for verifying properties of data parallel GPU programs via test amplification. The key insight behind our work is that we can use the technique of static information flow to amplify the result of a single test execution over ...
Also Published in:
ACM SIGPLAN Notices: Volume 47 Issue 6, June 2012 - research-articleJune 2012
Deterministic parallelism via liquid effects
PLDI '12: Proceedings of the 33rd ACM SIGPLAN Conference on Programming Language Design and ImplementationJune 2012, Pages 45–54https://doi.org/10.1145/2254064.2254071Shared memory multithreading is a popular approach to parallel programming, but also fiendishly hard to get right. We present Liquid Effects, a type-and-effect system based on refinement types which allows for fine-grained, low-level, shared memory ...
Also Published in:
ACM SIGPLAN Notices: Volume 47 Issue 6, June 2012 - research-articleJune 2009
Type-based data structure verification
PLDI '09: Proceedings of the 30th ACM SIGPLAN Conference on Programming Language Design and ImplementationJune 2009, Pages 304–315https://doi.org/10.1145/1542476.1542510We present a refinement type-based approach for the static verification of complex data structure invariants. Our approach is based on the observation that complex data structures are typically fashioned from two elements: recursion (e.g., lists and ...
Also Published in:
ACM SIGPLAN Notices: Volume 44 Issue 6, June 2009 - research-articleJune 2009
Staged information flow for javascript
PLDI '09: Proceedings of the 30th ACM SIGPLAN Conference on Programming Language Design and ImplementationJune 2009, Pages 50–62https://doi.org/10.1145/1542476.1542483Modern websites are powered by JavaScript, a flexible dynamic scripting language that executes in client browsers. A common paradigm in such websites is to include third-party JavaScript code in the form of libraries or advertisements. If this code were ...
Also Published in:
ACM SIGPLAN Notices: Volume 44 Issue 6, June 2009 - research-articleJune 2008
Dataflow analysis for concurrent programs using datarace detection
PLDI '08: Proceedings of the 29th ACM SIGPLAN Conference on Programming Language Design and ImplementationJune 2008, Pages 316–326https://doi.org/10.1145/1375581.1375620Dataflow analyses for concurrent programs differ from their single-threaded counterparts in that they must account for shared memory locations being overwritten by concurrent threads. Existing dataflow analysis techniques for concurrent programs ...
Also Published in:
ACM SIGPLAN Notices: Volume 43 Issue 6, June 2008 - research-articleJune 2008
Liquid types
PLDI '08: Proceedings of the 29th ACM SIGPLAN Conference on Programming Language Design and ImplementationJune 2008, Pages 159–169https://doi.org/10.1145/1375581.1375602We present Logically Qualified Data Types, abbreviated to Liquid Types, a system that combines Hindley-Milner type inference with Predicate Abstraction to automatically infer dependent types precise enough to prove a variety of safety properties. Liquid ...
Also Published in:
ACM SIGPLAN Notices: Volume 43 Issue 6, June 2008 - ArticleJune 2007
Mace: language support for building distributed systems
PLDI '07: Proceedings of the 28th ACM SIGPLAN Conference on Programming Language Design and ImplementationJune 2007, Pages 179–188https://doi.org/10.1145/1250734.1250755Building distributed systems is particularly difficult because of the asynchronous, heterogeneous, and failure-prone environment where these systemsmust run. Tools for building distributed systems must strike a compromise between reducing programmer ...
Also Published in:
ACM SIGPLAN Notices: Volume 42 Issue 6, June 2007 - ArticleJune 2005
Path slicing
PLDI '05: Proceedings of the 2005 ACM SIGPLAN conference on Programming language design and implementationJune 2005, Pages 38–47https://doi.org/10.1145/1065010.1065016We present a new technique, path slicing, that takes as input a possibly infeasible path to a target location, and eliminates all the operations that are irrelevant towards the reachability of the target location. A path slice is a subsequence of the ...
Also Published in:
ACM SIGPLAN Notices: Volume 40 Issue 6, June 2005 - ArticleJune 2004
Race checking by context inference
PLDI '04: Proceedings of the ACM SIGPLAN 2004 conference on Programming language design and implementationJune 2004, Pages 1–13https://doi.org/10.1145/996841.996844Software model checking has been successful for sequential programs, where predicate abstraction offers suitable models, and counterexample-guided abstraction refinement permits the automatic inference of models. When checking concurrent programs, we ...
Also Published in:
ACM SIGPLAN Notices: Volume 39 Issue 6, May 2004