1,205 papers · page 14 of 61
Lakshminarayanan Renganarayanan, DaeGon Kim, Michelle Mills Strout, Sanjay V. Rajopadhye
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…
Jan Smans, Bart Jacobs, Frank Piessens
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…
Sven Verdoolaege, Gerda Janssens, Maurice Bruynooghe
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…
Xing Wu, Frank Mueller
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…
Martín Abadi, Andrew Birrell, Tim Harris, Michael Isard
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…
Rajeev Alur, Swarat Chaudhuri, P. Madhusudan
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…
Utpal Banerjee
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…
Gilles Barthe, César Kunz
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 …
Jesper Bengtson, Karthikeyan Bhargavan, Cédric Fournet, Andrew D. Gordon, Sergio Maffeis
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…
John Derrick, Gerhard Schellhorn, Heike Wehrheim
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 …
Werner Dietl, Sophia Drossopoulou, Peter Müller
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…
Christos Dimoulas, Matthias Felleisen
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…
Andrea Flexeder, Markus Müller-Olm, Michael Petter, Helmut Seidl
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…
Thomas Martin Gawlitza, Helmut Seidl
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…
Jürgen Giesl, Matthias Raffelsieper, Peter Schneider-Kamp, Stephan Swiderski, René Thiemann
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…
Bhargav S. Gulavani, Supratik Chakraborty, G. Ramalingam, Aditya V. Nori
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…
Shan Shan Huang, Yannis Smaragdakis
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, …
Jens Palsberg
No abstract available.
Jens Palsberg
No abstract available.
Polyvios Pratikakis, Jeffrey S. Foster, Michael Hicks
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…