1,205 papers · page 9 of 61
Building a cost-effective static analyzer for real-world programs is still regarded an art. One key contributor to this grim reputation is the difficulty in balancing the cost and the precision of an analyzer. An ideal analyzer should be adaptive to a given analysis task and avoi…
We propose an approach for the modular specification and verification of total correctness properties of object-oriented programs. The core of our approach is a specification style that prescribes a way to assign a level expression to each method such that each callee’s level is …
Program analyses often utilize various forms of sensitivity such as context sensitivity, call-site sensitivity, and object sensitivity. These techniques all allow for more precise program analyses, that are able to compute more precise program invariants, and to verify stronger p…
Modern systems are increasingly susceptible to soft errors that manifest themselves as bit flips and possibly alter the semantics of an application. We would like to measure the quality degradation on semantics due to such bit flips, and thus we introduce a Hyperball abstract dom…
No abstract available.
This article investigates the semantic intricacies of conditioning, a main feature in probabilistic programming. Our study is based on an extension of the imperative probabilistic guarded command language pGCL with conditioning. We provide a weakest precondition (wp) semantics an…
Constraint-based refactoring generalizes constraint-based type refactoring as introduced by Tip et al. [61] by extending the coverage of change from types to names, locations, accessibilities, and other properties of program elements. Starting with a generic specification of refa…
In multiparty session types, interconnection networks identify which roles in a session engage in communication (i.e., two roles are connected if they exchange a message). In session-based interpretations of linear logic the analogue notion corresponds to determining which proces…
In security-typed programming languages, types statically enforce noninterference between potentially conspiring values, such as the arguments and results of functions. But to adopt static security types, like other advanced type disciplines, programmers face a steep wholesale tr…
Constructing a high-performance garbage collector is hard. Constructing a fully concurrent ‘on-the-fly’ compacting collector is much more so. We describe our experience of implementing the Sapphire algorithm as the first on-the-fly, parallel, replication copying, garbage collecto…
editorial Free Access Share on Corrigendum to “Cross-Language Interoperability in a Multi-Language Runtime”, by Grimmer et al., ACM Transactions on Programming Languages and Systems (TOPLAS) Volume 40, Issue 2, Article No. 8ACM Transactions on Programming Languages and SystemsVol…
Modern architectures rely on memory fences to prevent undesired weakenings of memory consistency. As the fences’ semantics may be subtle, the automation of their placement is highly desirable. But precise methods for restoring consistency do not scale to deployed systems’ code. W…
JavaScript is the source of many security problems, including cross-site scripting attacks and malicious advertising code. Central to these problems is the fact that code from untrusted sources runs with full privileges. Information flow controls help prevent violations of data c…
Compaction 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 provided some initial asymptotic …
We introduce a novel approach to typestate-oriented programming based on the chemical metaphor: state and operations on objects are molecules of messages, and state transformations are chemical reactions. This approach allows us to investigate typestate in an inherently concurren…
Numerical software, common in scientific computing or embedded systems, inevitably uses a finite-precision approximation of the real arithmetic in which most algorithms are designed. In many applications, the roundoff errors introduced by finite-precision arithmetic are not the o…
The Message Passing Interface (MPI) is the standard API for parallelization in high-performance and scientific computing. Communication deadlocks are a frequent problem in MPI programs, and this article addresses the problem of discovering such deadlocks. We begin by showing that…
Verifying invariants of fine-grained concurrent data structures is challenging, because interference from other threads may occur at any time. We propose a new way of proving invariants of fine-grained concurrent data structures: applying rely-guarantee reasoning to references in…
Big data is revolutionizing how all sectors of our economy do business, including telecommunication, transportation, medical, and finance. Big data comes in two flavors: data at rest and data in motion. Processing data in motion is stream processing . Stream processing for big da…
Today, software is traded worldwide on global markets, with apps being downloaded to smartphones within minutes or seconds. This poses, more than ever, the challenge of ensuring safety of software in the face of (1) unknown or untrusted software providers together with (2) resour…