1,205 papers · page 14 of 61
Loop tiling is a widely used program optimization that improves data locality and enables coarse-grained parallelism. Parameterized tiled loops, where the tile sizes remain symbolic parameters until runtime, are quite useful for iterative compilers and autotuners that produce hig…
An important, challenging problem in the verification of imperative programs with shared, mutable state is the frame problem in the presence of data abstraction. That is, one must be able to specify and verify upper bounds on the set of memory locations a method can read and writ…
Designers often apply manual or semi-automatic loop and data transformations on array- and loop-intensive programs to improve performance. It is crucial that such transformations preserve the functionality of the program. This article presents an automatic method for constructing…
Performance modeling for scientific applications is important for assessing potential application performance and systems procurement in high-performance computing (HPC). Recent progress on communication tracing opens up novel opportunities for communication modeling due to its l…
Software Transactional Memory (STM) is an attractive basis for the development of language features for concurrent programming. However, the semantics of these features can be delicate and problematic. In this article we explore the trade-offs semantic simplicity, the viability o…
While model checking of pushdown systems is by now an established technique in software verification, temporal logics and automata traditionally used in this area are unattractive on two counts. First, logics and automata traditionally used in model checking cannot express requir…
Since its introduction by Joseph A. Fisher in 1979, trace scheduling has influenced much of the work on compile-time ILP (Instruction Level Parallelism) transformations. Initially developed for use in microcode compaction, it quickly became the main technique for machine-level co…
A certificate is a mathematical object that can be used to establish that a piece of mobile code satisfies some security policy. In general, certificates cannot be generated automatically. There is thus an interest in developing methods to reuse certificates generated for source …
We present the design and implementation of a typechecker for verifying security properties of the source code of cryptographic protocols and access control mechanisms. The underlying type theory is a λ-calculus equipped with refinement types for expressing pre- and post-conditio…
Concurrent objects are inherently complex to verify. In the late 80s and early 90s, Herlihy and Wing proposed linearizability as a correctness condition for concurrent objects, which, once proven, allows us to reason about concurrent objects using pre- and postconditions only. A …
Ownership is a powerful concept to structure the object store and to control aliasing and modifications of objects. This article presents an ownership type system for a Java-like programming language with generic types. Like our earlier Universe type system, Generic Universe Type…
Behavioral software contracts have become a popular mechanism for specifying and ensuring logical claims about a program's flow of values. While contracts for first-order functions come with a natural interpretation and are well understood, the various incarnations of higher-orde…
In this article we provide an interprocedural analysis of linear two-variable equalities. The novel algorithm has a worst-case complexity of 𝒪( n ⋅ k 4 ), where k is the number of variables and n is the program size. Thus, it saves a factor of k 4 in comparison to a related algor…
We present practical algorithms for computing exact least solutions of equation systems over the reals with addition, multiplication by positive constants, minimum and maximum. The algorithms are based on strategy iteration. Our algorithms can, for instance, be used for the analy…
There are many powerful techniques for automated termination analysis of term rewriting. However, up to now they have hardly been used for real programming languages. We present a new approach which permits the application of existing techniques from term rewriting to prove termi…
In this article, we present a new shape analysis algorithm. The key distinguishing aspect of our algorithm is that it is completely compositional, bottom-up and noniterative. We present our algorithm as an inference system for computing Hoare triples summarizing heap manipulating…
We present MorphJ: a language for specifying general classes whose members are produced by iterating over members of other classes. We call this technique “class morphing” or just “morphing.” Morphing extends the notion of genericity so that not only types of methods and fields, …
No abstract available.
No abstract available.
Locksmith is a static analysis tool for automatically detecting data races in C programs. In this article, we describe each of Locksmith's component analyses precisely, and present systematic measurements that isolate interesting trade-offs between precision and efficiency in eac…