PLDI 2012 List of Accepted Papers

二 042012

List of Accepted Papers 论文收录

* The acceptance of a few additional papers is still pending

Compiling a High-Level Language for GPUs (via Language Support for Architectures and Compilers)

Christophe Dubach¹², Perry Cheng¹, Rodric Rabbah¹, David F. Bacon¹, Stephen Fink¹
¹IBM, ²University of Edinburgh

Synchronising C/C++ and POWER

Susmit Sarkar¹, Mark Batty¹, Scott Owens¹, Kayvan Memarian¹, Peter Sewell¹, Luc Maranget², Jade Alglave³, Derek Williams⁴
¹University of Cambridge, ²INRIA, ³University of Oxford, ⁴IBM

Static Analysis and Compiler Implementation of Idempotent Processing

Marc Kruijf, Karthikeyan Sankaralingam, Somesh Jha
University of Wisconsin – Madison

Adaptive Input-aware Compilation for Graphics Engines

Mehrzad Samadi¹, Amir Hormati², Mojtaba Mehrara¹, Scott Mahlke¹
¹University of Michigan, ²Microsoft Corporation

Automated Error Diagnosis Using Abductive Inference

Isil Dillig¹, Thomas Dillig¹, Alex Aiken²
¹College of William & Mary, ²Stanford University

Multicore Acceleration of Priority-Based Schedulers for Concurrency Bug Detection

Santosh Nagarakatte¹, Sebastian Burckhardt², Milo M K Martin¹, Madanlal Musuvathi²
¹University of Pennsylvania, ²Microsoft Research

RockSalt: Better, Faster, Stronger SFI for the x86

Greg Morrisett¹, Gang Tan², Joseph Tassarotti¹, Jean-Baptiste Tristan¹, Edward Gan¹
¹Harvard University, ²Lehigh University

Fast and Precise Hybrid Type Inference for JavaScript

Brian Hackett¹, Shu-yu Guo²
¹Mozilla Corporation, ²University of California, Los Angeles

Fully Automatic and Precise Detection of Thread Safety Violations

Michael Pradel, Thomas Gross
ETH Zurich

The Implicit Calculus: A New Foundation for Generic Programming

Bruno Oliveira¹, Tom Schrijvers², Wontae Choi¹, Wonchan Lee¹, Kwangkeun Yi¹
¹Seoul National University, ²Universiteit Gent

Sound and Precise Analysis of Multithreaded Programs through Schedule Specialization

Jingyue Wu, Yang Tang, Gang Hu, Heming Cui, Junfeng Yang
Columbia University

Effective Parallelization of Loops in the Presence of I/O Operations

Min Feng, Rajiv Gupta, Iulian Neamtiu
University of California, Riverside

Input-Sensitive Profiling

Emilio Coppa, Camil Demetrescu, Irene Finocchi
Sapienza University of Rome

Type-Directed Completion of Partial Expressions

Daniel Perelman¹, Sumit Gulwani², Tom Ball², Dan Grossman¹
¹University of Washington, ²Microsoft Research Redmond

Synthesising graphics card programs from DSLs

Luke Cartey, Rune LyngsÃ¸, Oege Moor
University of Oxford

Reasoning about Relaxed Programs

Michael Carbin, Deokhwan Kim, Sasa Misailovic, Martin C. Rinard
MIT Computer Science and Artificial Intelligence Laboratory

Parallelizing Top-Down Interprocedural Analyses

Aws Albarghouthi¹, Rahul Kumar², Aditya Nori³, Sriram Rajamani³
¹University of Toronto, ²Microsoft Corporation, ³Microsoft Research India

Concurrent Data Representation Synthesis

Peter Hawkins¹, Alex Aiken¹, Kathleen Fisher², Martin Rinard³, Mooly Sagiv⁴
¹Stanford University, ²Tufts University, ³MIT Computer Science and Artificial Intelligence Laboratory, ⁴Tel-Aviv University

Diderot: A Parallel DSL for Image Analysis and Visualization

Charisee Chiw, Gordon Kindlmann, John Reppy, Lamont Samuels, Nick Seltzer
University of Chicago

A Dynamic Program Analysis to find Floating-Point Accuracy Problems

Florian Benz¹, Sebastian Hack¹, Andreas Hildebrandt²
¹Saarland University, ²Johannes-Gutenberg UniversitÄt Mainz

Self-Stabilizing Java

Yong hun Eom, Brian Demsky
University of California, Irvine

Race Detection for Web Applications

Boris Petrov¹, Martin Vechev², Manu Sridharan³, Julian Dolby³
¹Sofia University, ²ETH Zurich, ³IBM T.J. Watson Research Center

Engage: A Deployment Management System

Jeffrey Fischer¹, Rupak Majumdar², Shahram Esmaeilsabzali²
¹Genforma Corp., ²MPI-SWS

Understanding and Detecting Real-World Performance Bugs

Guoliang Jin¹, Linhai Song¹, Xiaoming Shi¹, Joel Scherpelz², Shan Lu¹
¹University of Wisconsin, Madison, ²Nvidia

And Then There Were None: A Stall-Free Real-Time Garbage Collector for Reconfigurable Hardware

David F. Bacon, Perry Cheng, Sunil Shukla
IBM Research

Polyhedra Scanning Revisited

Chun Chen
University of Utah

Dynamic Trace-Based Analysis of Vectorization Potential of Applications

Justin Holewinski, Ragavendar Ramamurthi, Naznin Fauzia, Mahesh Ravishankar, Louis-Noel Pouchet, Atanas Rountev, P. Sadayappan
Ohio State University

Automated Synthesis of Symbolic Instruction Encodings from I/O Samples

Patrice Godefroid¹, Ankur Taly²
¹Microsoft Research, ²Stanford University

Parcae: A System for Flexible Parallel Execution

Arun Raman¹, Ayal Zaks², Jae W. Lee ³, David I. August¹
¹Princeton University, ²IBM Research, ³Sungkyunkwan University

Dynamic Synthesis for Relaxed Memory Models

Feng Liu¹, Nayden Nedev¹, Nedyalko Prisadnikov², Martin Vechev³, Eran Yahav⁴
¹Princeton University, ²Sofia University, ³ETH Zurich, ⁴Technion

Language-Based Control and Mitigation of Timing Channels

Danfeng Zhang, Aslan Askarov, Andrew Myers
Cornell University

A Compiler Framework for Extracting Superword Level Parallelism

Jun Liu, Yuanrui Zhang, Ohyoung Jang, Wei Ding, Mahmut Kandemir
The Pennsylvania State University

Algorithmic Profiling

Dmitrijs Zaparanuks, Matthias Hauswirth
University of Lugano

Reagents: Expressing and Composing Fine-grained Concurrency

Aaron Turon
Northeastern University

Janus: Exploiting Parallelism via Hindsight

Omer Tripp¹, Roman Manevich², John Field³, Mooly Sagiv¹
¹Tel Aviv University, ²The University of Texas at Austin, ³Google

Deterministic Parallelism via Liquid Effects

Ming Kawaguchi, Patrick Rondon, Alexander Bakst, Ranjit Jhala
UC San Diego

Chimera: Hybrid Program Analysis for Determinism

Dongyoon Lee, Peter Chen, Jason Flinn, Satish Narayanasamy
University of Michigan, Ann Arbor

Scalable and Precise Dynamic Datarace Detection for Structured Parallelism

Raghavan Raman¹, Jisheng Zhao¹, Vivek Sarkar¹, Martin Vechev², Eran Yahav³
¹Rice University, ²ETH Zurich, ³Technion

Synthesizing Software Verifiers from Proof Rules

Sergey Grebenshchikov¹, Nuno Lopes², Corneliu Popeea¹, Andrey Rybalchenko¹
¹Technical University Munich, ²INESC-ID / IST – TU Lisbon

Speculative Separation for Privatization and Reductions

Nick P. Johnson¹, Hanjun Kim¹, Prakash Prabhu¹, Ayal Zaks ², David I. August¹
¹Princeton University, ²IBM Haifa Research Lab

SuperC: Parsing All of C by Taming the Preprocessor

Paul Gazzillo, Robert Grimm
New York University

Type-Directed Automatic Incrementalization

Yan Chen, Joshua Dunfield, Umut A. Acar
Max Planck Institute for Software Systems

Efficient State Merging in Symbolic Execution

Volodymyr Kuznetsov, Johannes Kinder, Stefan Bucur, George Candea
EPFL

Design and Implementation of Sparse Global Analyses for C-like Languages

Hakjoo Oh, Kihong Heo, Wonchan Lee, Woosuk Lee, Kwangkeun Yi
Seoul National University

大软件的烦恼与编译技术

IT产业, 前端和程序分析, 系统软件及库, 编程技术, 编译前沿, 编译技术, 编译理论实践和应用 1 Response »

一 302012

现在虽说卖硬件的比不上卖软件的，卖软件的比不上卖服务的。但软件仍然是服务的基石。
而且不管是软件、硬件、还是服务，背后都是一行行的代码，以及基于这些代码所形成的软件功能、硬件系统、技术人员的经验等等。
这些代码有的用C/C++、Java、C#写，有的用PHP、JavaScript、Ruby写，有的用Verilog写。 Continue reading »

List of accepted papers

Multiple Facets for Dynamic Information Flow. Authors:
Thomas Austin and Cormac Flanagan (UC Santa Cruz)
A Unified Approach to Fully Lazy Sharing.
Authors:
Thibaut Balabonski (PPS, Université Paris-Diderot)
An Executable Formal Semantics of C with Applications.
Authors:
Chucky Ellison and Grigore Rosu (University of Illinois)
Defining Code-injection Attacks.Authors:
Donald Ray and Jay Ligatti (University of South Florida)
The Marriage of Bisimulations and Kripke Logical Relations.
Authors:
Chung-Kil Hur, Derek Dreyer, Georg Neis, and Viktor Vafeiadis (MPI-SWS)
Recursive Proofs for Inductive Tree Data-Structures.
Authors:
P. Madhusudan, Xiaokang Qiu, and Andrei Stefanescu (Univ of Illinois at Urbana-Champaign)
An Abstract Interpretation Framework for Termination. Authors:
Patrick Cousot (CNRS ENS INRIA NYU) and Radhia Cousot (CNRS ENS INRIA)
Algebraic Foundations for Effect-Dependent Optimisations. Authors:
Ohad Kammar and Gordon Plotkin (University of Edinburgh)
Higher-Order Functional Reactive Programming in Bounded Space.Authors:
Neelakantan R. Krishnaswami and Nick Benton (Microsoft Research) and Jan Hoffmann (LMU Munich)
Optimal Randomized Transformation of Approximate Computations. Authors:
Zeyuan Allen Zhu, Sasa Misailovic, Jonathan Kelner, and Martin Rinard (MIT)
Clarifying and compiling C/C++ concurrency: from C++0x to POWER.
Authors:
Mark Batty (University of Cambridge), Kayvan Memarian (INRIA), and Scott Owens, Susmit Sarkar, and Peter Sewell (University of Cambridge)
A Compiler and Run-time System for Network Programming Languages.
Authors:
Christopher Monsanto (Princeton University), Nate Foster (Cornell University), Rob Harrison (United States Military Academy), and David Walker (Princeton University)
Information Effects.
Authors:
Roshan James and Amr Sabry (Indiana University)
A Language for Automatically Enforcing Privacy Policies. Authors:
Jean Yang, Kuat Yessenov, and Armando Solar-Lezama (MIT CSAIL)
Static and User-Extensible Proof Checking. Authors:
Antonis Stampoulis and Zhong Shao (Yale University)
A Rely-Guarantee-Based Simulation for Verifying Concurrent Program Transformations. Authors:
Hongjin Liang, Xinyu Feng, and Ming Fu (School of Computer Science and Technology, University of Science and Technology of China)
A Type Theory for Probability Density Functions.Authors: Sooraj Bhat (College of Computing, Georgia Institute of Technology), Ashish Agarwal (Courant Institute of Mathematical Sciences, New York University), and Richard Vuduc and Alexander Gray (College of Computing, Georgia Institute of Technology)
Abstractions From Tests. Authors:
Mayur Naik (Georgia Tech), Hongseok Yang (Oxford University), and Ghila Castelnuovo and Mooly Sagiv (Tel-Aviv University)
A mechanized semantics for C++ object construction and destruction, with applications to resource management.Authors:
Tahina Ramananandro (INRIA Paris-Rocquencourt), Gabriel Dos Reis (Texas A&M University), and Xavier Leroy (INRIA Paris-Rocquencourt)
Programming with Binders and Indexed Data-Types.
Authors:
Andrew Cave and Brigitte Pientka (McGill University)
Analysis of Recursively Parallel Programs. Authors:
Ahmed Bouajjani and Michael Emmi (LIAFA, Université Paris Diderot, France)
Access Permission Contracts for Scripting Languages. Authors:
Phillip Heidegger, Annette Bieniusa, and Peter Thiemann (University of Freiburg)
Canonicity for 2-Dimensional Type Theory.Authors:
Daniel R. Licata and Robert Harper (Carnegie Mellon University)
Freefinement. Authors:
Stephan van Staden (ETH Zurich), Cristiano Calcagno (ETH Zurich, Imperial College London and Monoidics Ltd), and Bertrand Meyer (ETH Zurich)
Towards Nominal Computation.
Authors:
Mikolaj Bojanczyk, Laurent Braud, Bartek Klin, and Slawomir Lasota (University of Warsaw)
Resource-Sensitive Synchronization Inference by Abduction. Authors:
Matko Botincan and Mike Dodds (University of Cambridge) and Suresh Jagannathan (Purdue University)
Underspecified harnesses and interleaved bugs.
Authors:
Saurabh Joshi (IIT Kanpur), Shuvendu Lahiri (Microsoft Research, Redmond), and Akash Lal (Microsoft Research, Bangalore)
Constraints as Control.
Authors:
Ali Sinan Köksal, Viktor Kuncak, and Philippe Suter (EPFL)
Edit Lenses. Authors:
Martin Hofmann (Ludwig Maximilians Universität) and Benjamin C. Pierce and Daniel Wagner (University of Pennsylvania)
Sound Predictive Race Detection in Polynomial Time.
Authors:
Yannis Smaragdakis (University of Athens and UMass Amherst), Jacob M. Evans (University of Massachusetts at Amherst), and Caitlin Sadowski, Jaeheon Yi, and Cormac Flanagan (University of California at Santa Cruz)
Symbolic Finite State Transducers, Algorithms and Applications. Authors:
Nikolaj Bjorner (Microsoft Research), Pieter Hooimeijer (U. Virginia), and Benjamin Livshits, David Molnar, and Margus Veanes (Microsoft Research)
Run Your Research: On the Effectiveness of Lightweight Mechanization. Authors:
Casey Klein (Northwestern University), John Clements (California Polytechnic State University), Christos Dimoulas, Carl Eastlund, and Matthias Felleisen (Northeastern University), Matthew Flatt (University of Utah), Jay McCarthy (Brigham Young University), Jon Rafkind (University of Utah), Sam Tobin-Hochstadt (Northeastern University), and Robert Bruce Findler (Northwestern University)
Extending System F-eta with Abstraction over Erasable Coercions.
Authors:
Didier Remy and Julien Cretin (INRIA Paris-Rocquencourt)
A Program Logic for JavaScript.
Authors:
Philippa Gardner, Sergio Maffeis, and Gareth Smith (Imperial College London)
Deciding Choreography Realizability.
Authors:
Samik Basu (Iowa State University), Tevfik Bultan (University of California at Santa Barbara), and Meriem Ouederni (University of Malagna)
Nested Refinements for Dynamic Languages.
Authors:
Ravi Chugh, Patrick M. Rondon, and Ranjit Jhala (UC San Diego)
The Ins and Outs of Gradual Type Inference.Authors:
Aseem Rastogi (SUNY Stony Brook) and Avik Chaudhuri and Basil Hosmer (Adobe Advanced Technology Labs)
A Type System for Borrowing Without Fractions.
Authors:
Karl Naden, Robert L. Bocchino Jr., and Jonathan Aldrich (Carnegie Mellon University)
Formalizing the LLVM Intermediate Representation for Verified Program Transformation.
Authors:
Jianzhou Zhao, Steve Zdancewic, Santosh Nagarakatte, and Milo M. K. Martin (University of Pennsylvania)
Self-Certification: Bootstrapping Typecheckers in F* with Coq.
Authors:
Pierre-Yves Strub (MSR INRIA) and Nikhil Swamy, Cedric Fournet, and Juan Chen (Microsoft Research)
Verification of Parameterized Concurrent Programs By Modular Reasoning about Data and Control. Authors:
Azadeh Farzan and Zachary Kincaid (University of Toronto)
Probabilistic Relational Reasoning for Differential Privacy.
Authors:
Gilles Barthe, Boris Köpf, Federico Olmedo, and Santiago Zanella Beguelin (IMDEA Software Institute)
Playing in the Grey Area of Proofs.
Authors:
Krystof Hoder (University of Manchester), Laura Kovacs (TU Vienna), and Andrei Voronkov (University of Manchester)
Syntactic Control of Interference for Separation Logic.
Authors:
Uday S. Reddy (University of Birmingham) and John C. Reynolds (Carnegie-Mellon)

YY一下量子计算机的编译器

编译前沿 3 Responses »

十二 232010

没错，是量子计算机。既然是计算机，就需要程序员，需要程序员就需要编译器。今天就来聊聊量子计算机的编译器，因为量子计算机还遥遥无期，所以就叫YY了。

这篇文章源自龙书第一作者，现在在哥伦比亚大学教书的Alfred V. Aho在 2008年PLDI上的一篇邀请讲座的PPT，能读懂英文的，请无视本文，原因嘛，我是中国人，你懂的，哈。 Continue reading »

好消息：PLDI 2012极有可能在中国召开

编译前沿, 编译技术 5 Responses »

十一 182010

据十分可靠的小道消息透露：2012年的PLDI会议极其有可能会在中国召开。

PLDI(Programming Language Design and Implementation)是全球最有影响力的有关编程语言设计和编译器实现方面的会议。每年一届，平均每篇文章的被引用次数达到38次，在所有体系结构相关会议中排名第四，前三依次是OSDI(Usenix Symposium on Operating Systems Design and Implementation)， SOSP(ACM SIGOPS Symp on OS Principles)， ASPLOS(Architectural Support for Programming Languages and Operating Systems).PLDI每年的通过率仅有20%+,基本是4：1的比例。

中国地区，迄今为止，共发表过5篇论文，分别是2010年计算所、2008和2007年清华、2005和2004年Intel中国、1992年中国台湾。2011年的PLDI，本博听说已经有两个小团伙在冲刺，文章初稿的提交截止日期是后天(美国时间：11月19号)，目前他们几乎都在加班加点，拼命丰富。祝他们好运！

PLDI， Welcome to China!

多面体模型是编译器循环优化的未来吗？

编译前沿, 编译技术 13 Responses »

七 162010

相信很多人都听说过：程序80%的运行时间用来执行20%的代码。循环几乎占一般应用程序运行时间的绝大部分。优化程序中有关循环尤其是关键循环的代码将会给程序的性能带来很大的提升。而且这种循环优化是目标机器无关的，任何对循环的一点点优化都会在所有编译器支持的目标机上带来性能提升。所以编译器上的循环优化一直是研究的热点。 Continue reading »