PLDI 2015
59 papers
- A formal C memory model supporting integer-pointer casts
- A simpler, safer programming and execution model for intermittent systems
- Algorithmic debugging of real-world haskell programs: deriving dependencies from the cost centre stack
- Asynchronous programming, analysis and testing with state machines
- Automatic error elimination by horizontal code transfer across multiple applications
- Automatic induction proofs of data-structures in imperative programs
- Automatically improving accuracy for floating point expressions
- Autotuning algorithmic choice for input sensitivity
- Blame and coercion: together again for the first time
- Celebrating diversity: a mixture of experts approach for runtime mapping in dynamic environments
- Composing concurrency control
- Compositional certified resource bounds
- Concurrency debugging with differential schedule projections
- DAG inlining: a decision procedure for reachability-modulo-theories in hierarchical programs
- Declarative programming over eventually consistent data stores
- Defining the undefinedness of C
- Diagnosing type errors with class
- Dynamic partial order reduction for relaxed memory models
- Efficient execution of recursive programs on commodity vector hardware
- Efficient synthesis of network updates
- Efficient synthesis of probabilistic programs
- Exploring and enforcing security guarantees via program dependence graphs
- Finding counterexamples from parsing conflicts
- FlashRelate: extracting relational data from semi-structured spreadsheets using examples
- Helium: lifting high-performance stencil kernels from stripped x86 binaries to halide DSL code
- Improving compiler scalability: optimizing large programs at small price
- Interactive parser synthesis by example
- KJS: a complete formal semantics of JavaScript
- LaminarIR: compile-time queues for structured streams
- Light: replay via tightly bounded recording
- Lightweight, flexible object-oriented generics
- Loop and data transformations for sparse matrix code
- Making numerical program analysis fast
- Many-core compiler fuzzing
- Mechanized verification of fine-grained concurrent programs
- Monitoring refinement via symbolic reasoning
- Optimizing off-chip accesses in multicores
- Peer-to-peer affine commitment using bitcoin
- Preventing glitches and short circuits in high-level self-timed chip specifications
- Profile-guided meta-programming
- Provably correct peephole optimizations with alive
- Relatively complete counterexamples for higher-order programs
- Relaxing safely: verified on-the-fly garbage collection for x86-TSO
- Stateless model checking concurrent programs with maximal causality reduction
- Static detection of asymptotic performance bugs in collection traversals
- Synthesis of machine code from semantics
- Synthesis of ranking functions using extremal counterexamples
- Synthesizing data structure transformations from input-output examples
- Synthesizing parallel graph programs via automated planning
- Synthesizing racy tests
- Termination and non-termination specification inference
- The Push/Pull model of transactions
- Tree dependence analysis
- Type-and-example-directed program synthesis
- Verdi: a framework for implementing and formally verifying distributed systems
- Verification of a cryptographic primitive: SHA-256 (abstract)
- Verification of producer-consumer synchronization in GPU programs
- Verifying read-copy-update in a logic for weak memory
- Zero-overhead metaprogramming: reflection and metaobject protocols fast and without compromises