Implementation of the memory-safe full ANSI-C compiler
This paper describes a completely memory-safe compiler for C language programs that is fully compatible with the ANSI C specification.
1,971 papers · page 59 of 99
Progress guarantee for parallel programs via bounded lock-freedom
Parallel platforms are becoming ubiquitous with modern computing systems. Many parallel applications attempt to avoid locks in order to achieve high responsiveness, aid scalability, and avoid deadlocks and livelocks. However, avoiding the use of system locks does not guarantee th…
Sharing classes between families
Class sharing is a new language mechanism for building extensible software systems. Recent work has separately explored two different kinds of extensibility: first, family inheritance, in which an entire family of related classes can be inherited, and second, adaptation, in which…
Automatic generation of library bindings using static analysis
High-level languages are growing in popularity. However, decades of C software development have produced large libraries of fast, time-tested, meritorious code that are impractical to recreate from scratch. Cross-language bindings can expose low-level C code to high-level languag…
Typed self-representation
Self-representation -- the ability to represent programs in their own language -- has important applications in reflective languages and many other domains of programming language design. Although approaches to designing typed program representations for sublanguages of some base…
Laminar: practical fine-grained decentralized information flow control
Decentralized information flow control (DIFC) is a promising model for writing programs with powerful, end-to-end security guarantees. Current DIFC systems that run on commodity hardware can be broadly categorized into two types: language-level and operating system-level DIFC. La…
Error propagation analysis for file systems
Unchecked errors are especially pernicious in operating system file management code. Transient or permanent hardware failures are inevitable, and error-management bugs at the file system layer can cause silent, unrecoverable data corruption. We propose an interprocedural static a…
Programming model for a heterogeneous x86 platform
The client computing platform is moving towards a heterogeneous architecture consisting of a combination of cores focused on scalar performance, and a set of throughput-oriented cores. The throughput oriented cores (e.g. a GPU) may be connected over both coherent and non-coherent…
Verifiable composition of deterministic grammars
There is an increasing interest in extensible languages,
Chameleon: adaptive selection of collections
Languages such as Java and C#, as well as scripting languages like Python, and Ruby, make extensive use of Collection classes. A collection implementation represents a fixed choice in the dimensions of operation time, space utilization, and synchronization. Using the collection i…
Program verification using templates over predicate abstraction
We address the problem of automatically generating invariants with quantified and boolean structure for proving the validity of given assertions or generating pre-conditions under which the assertions are valid. We present three novel algorithms, having different strengths, that …
Dynamic software updates: a VM-centric approach
Software evolves to fix bugs and add features. Stopping and restarting programs to apply changes is inconvenient and often costly. Dynamic software updating (DSU) addresses this problem by updating programs while they execute, but existing DSU systems for managed languages do not…
Binary analysis for measurement and attribution of program performance
Modern programs frequently employ sophisticated modular designs. As a result, performance problems cannot be identified from costs attributed to routines in isolation; understanding code performance requires information about a routine's calling context. Existing performance tool…
Analyzing recursive programs using a fixed-point calculus
We show that recursive programs where variables range over finite domains can be effectively and efficiently analyzed by describing the analysis algorithm using a formula in a fixed-point calculus. In contrast with programming in traditional languages, a fixed-point calculus serv…
Towards a holistic approach to auto-parallelization: integrating profile-driven parallelism detection and machine-learning based mapping
Compiler-based auto-parallelization is a much studied area, yet has still not found wide-spread application. This is largely due to the poor exploitation of application parallelism, subsequently resulting in performance levels far below those which a skilled expert programmer cou…
TAJ: effective taint analysis of web applications
Taint analysis, a form of information-flow analysis, establishes whether values from untrusted methods and parameters may flow into security-sensitive operations. Taint analysis can detect many common vulnerabilities in Web applications, and so has attracted much attention from b…
Verified validation of lazy code motion
Translation validation establishes a posteriori the correctness of a run of a compilation pass or other program transformation. In this paper, we develop an efficient translation validation algorithm for the Lazy Code Motion (LCM) optimization. LCM is an interesting challenge for…
Go with the flow: profiling copies to find runtime bloat
Many large-scale Java applications suffer from runtime bloat. They execute large volumes of methods, and create many temporary objects, all to execute relatively simple operations. There are large opportunities for performance optimizations in these applications, but most are bei…
An integrated proof language for imperative programs
We present an integrated proof language for guiding the actions of multiple reasoning systems as they work together to prove complex correctness properties of imperative programs. The language operates in the context of a program verification system that uses multiple reasoning s…
Automatic volume management for programmable microfluidics
Microfluidics has enabled lab-on-a-chip technology to miniaturize and integrate biological and chemical analyses to a single chip comprising channels, valves, mixers, heaters, separators, and sensors. Recent papers have proposed programmable labs-on-a-chip as an alternative to tr…