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-articleApril 2022
What’s Decidable About Causally Consistent Shared Memory?
ACM Transactions on Programming Languages and Systems (TOPLAS), Volume 44, Issue 2Article No.: 8, Pages 1–55https://doi.org/10.1145/3505273While causal consistency is one of the most fundamental consistency models weaker than sequential consistency, the decidability of safety verification for (finite-state) concurrent programs running under causally consistent shared memories is still ...
- research-articleJune 2021
A Programming Language for Data Privacy with Accuracy Estimations
ACM Transactions on Programming Languages and Systems (TOPLAS), Volume 43, Issue 2Article No.: 6, Pages 1–42https://doi.org/10.1145/3452096Differential privacy offers a formal framework for reasoning about the privacy and accuracy of computations on private data. It also offers a rich set of building blocks for constructing private data analyses. When carefully calibrated, these analyses ...
- research-articleMay 2017
From Clarity to Efficiency for Distributed Algorithms
ACM Transactions on Programming Languages and Systems (TOPLAS), Volume 39, Issue 3Article No.: 12, Pages 1–41https://doi.org/10.1145/2994595This article describes a very high-level language for clear description of distributed algorithms and optimizations necessary for generating efficient implementations. The language supports high-level control flows in which complex synchronization ...
- research-articleMarch 2017
Limitations of Partial Compaction: Towards Practical Bounds
ACM Transactions on Programming Languages and Systems (TOPLAS), Volume 39, Issue 1Article No.: 2, Pages 1–44https://doi.org/10.1145/2994597Compaction of a managed heap is a costly operation to be avoided as much as possible in commercial runtimes. Instead, partial compaction is often used to defragment parts of the heap and avoid space blowup. Previous study of compaction limitation ...
- research-articleApril 2015
Verification of a Cryptographic Primitive: SHA-256
ACM Transactions on Programming Languages and Systems (TOPLAS), Volume 37, Issue 2Article No.: 7, Pages 1–31https://doi.org/10.1145/2701415This article presents a full formal machine-checked verification of a C program: the OpenSSL implementation of SHA-256. This is an interactive proof of functional correctness in the Coq proof assistant, using the Verifiable C program logic. Verifiable C ...
-
- research-articleJuly 2013
Efficient Identification of Linchpin Vertices in Dependence Clusters
ACM Transactions on Programming Languages and Systems (TOPLAS), Volume 35, Issue 2Article No.: 7, Pages 1–35https://doi.org/10.1145/2491522.2491524Several authors have found evidence of large dependence clusters in the source code of a diverse range of systems, domains, and programming languages. This raises the question of how we might efficiently locate the fragments of code that give rise to ...
- research-articleNovember 2012
Space overhead bounds for dynamic memory management with partial compaction
ACM Transactions on Programming Languages and Systems (TOPLAS), Volume 34, Issue 3Article No.: 13, Pages 1–43https://doi.org/10.1145/2362389.2362392Dynamic memory allocation is ubiquitous in today's runtime environments. Allocation and deallocation of objects during program execution may cause fragmentation and foil the program's ability to allocate objects. Robson [1971] has shown that a worst-...
- research-articleAugust 2010
Finite differencing of logical formulas for static analysis
ACM Transactions on Programming Languages and Systems (TOPLAS), Volume 32, Issue 6Article No.: 24, Pages 1–55https://doi.org/10.1145/1749608.1749613This article concerns mechanisms for maintaining the value of an instrumentation relation (also known as a derived relation or view), defined via a logical formula over core relations, in response to changes in the values of the core relations. It ...
- research-articleAugust 2010
WYSINWYX: What you see is not what you eXecute
ACM Transactions on Programming Languages and Systems (TOPLAS), Volume 32, Issue 6Article No.: 23, Pages 1–84https://doi.org/10.1145/1749608.1749612Over the last seven years, we have developed static-analysis methods to recover a good approximation to the variables and dynamically allocated memory objects of a stripped executable, and to track the flow of values through them. The article presents ...
- research-articleApril 2010
Santa Claus: Formal analysis of a process-oriented solution
ACM Transactions on Programming Languages and Systems (TOPLAS), Volume 32, Issue 4Article No.: 14, Pages 1–37https://doi.org/10.1145/1734206.1734211With the commercial development of multicore processors, the challenges of writing multithreaded programs to take advantage of these new hardware architectures are becoming more and more pertinent. Concurrent programming is necessary to achieve the ...
- research-articleFebruary 2010
A relational approach to interprocedural shape analysis
ACM Transactions on Programming Languages and Systems (TOPLAS), Volume 32, Issue 2Article No.: 5, Pages 1–52https://doi.org/10.1145/1667048.1667050This article addresses the verification of properties of imperative programs with recursive procedure calls, heap-allocated storage, and destructive updating of pointer-valued fields, that is, interprocedural shape analysis. The article makes three ...
- research-articleAugust 2009
From datalog rules to efficient programs with time and space guarantees
ACM Transactions on Programming Languages and Systems (TOPLAS), Volume 31, Issue 6Article No.: 21, Pages 1–38https://doi.org/10.1145/1552309.1552311This article describes a method for transforming any given set of Datalog rules into an efficient specialized implementation with guaranteed worst-case time and space complexities, and for computing the complexities from the rules. The running time is ...
- research-articleJuly 2009
A theory of contracts for Web services
ACM Transactions on Programming Languages and Systems (TOPLAS), Volume 31, Issue 5Article No.: 19, Pages 1–61https://doi.org/10.1145/1538917.1538920Contracts are behavioral descriptions of Web services. We devise a theory of contracts that formalizes the compatibility of a client with a service, and the safe replacement of a service with another service. The use of contracts statically ensures the ...
- research-articleOctober 2008
Perfect hashing as an almost perfect subtype test
ACM Transactions on Programming Languages and Systems (TOPLAS), Volume 30, Issue 6Article No.: 33, Pages 1–56https://doi.org/10.1145/1391956.1391960Subtype tests are an important issue in the implementation of object-oriented programming languages. Many techniques have been proposed, but none of them perfectly fulfills the five requirements that we have identified: constant-time, linear-space, ...
- research-articleAugust 2008
Relations as an abstraction for BDD-based program analysis
ACM Transactions on Programming Languages and Systems (TOPLAS), Volume 30, Issue 4Article No.: 19, Pages 1–63https://doi.org/10.1145/1377492.1377494In this article we present Jedd, a language extension to Java that supports a convenient way of programming with Binary Decision Diagrams (BDDs). The Jedd language abstracts BDDs as database-style relations and operations on relations, and provides ...
- research-articleMay 2008
Verifying safety properties of concurrent heap-manipulating programs
ACM Transactions on Programming Languages and Systems (TOPLAS), Volume 32, Issue 5Article No.: 18, Pages 1–50https://doi.org/10.1145/1745312.1745315We provide a parametric framework for verifying safety properties of concurrent heap-manipulating programs. The framework combines thread-scheduling information with information about the shape of the heap. This leads to verification algorithms that are ...
- articleNovember 2007
Empirical study of optimization techniques for massive slicing
ACM Transactions on Programming Languages and Systems (TOPLAS), Volume 30, Issue 1Pages 3–eshttps://doi.org/10.1145/1290520.1290523This article presents results from a study of techniques that improve the performance of graph-based interprocedural slicing of the System Dependence Graph (SDG). This is useful in “massive slicing” where slices are required for many or all of the ...
- articleNovember 2007
Forma: A framework for safe automatic array reshaping
ACM Transactions on Programming Languages and Systems (TOPLAS), Volume 30, Issue 1Pages 2–eshttps://doi.org/10.1145/1290520.1290522This article presents Forma, a practical, safe, and automatic data reshaping framework that reorganizes arrays to improve data locality. Forma splits large aggregated data-types into smaller ones to improve data locality. Arrays of these large data ...
- articleAugust 2007
Static validation of XSL transformations
ACM Transactions on Programming Languages and Systems (TOPLAS), Volume 29, Issue 4Pages 21–eshttps://doi.org/10.1145/1255450.1255454XSL Transformations (XSLT) is a programming language for defining transformations among XML languages. The structure of these languages is formally described by schemas, for example using DTD or XML Schema, which allows individual documents to be ...
- articleJanuary 2007
PPMexe: Program compression
ACM Transactions on Programming Languages and Systems (TOPLAS), Volume 29, Issue 1Pages 3–eshttps://doi.org/10.1145/1180475.1180478With the emergence of software delivery platforms, code compression has become an important system component that strongly affects performance. This article presents PPMexe, a compression mechanism for program binaries that analyzes their syntax and ...