Filter Program
Dates
Rooms
Tracks
Badges
Your Program
Mon 18 JunDisplayed time zone: Eastern Time (US & Canada) change
Mon 18 Jun
Displayed time zone: Eastern Time (US & Canada) change
08:00 - 09:00 | |||
08:00 60mOther | Breakfast Catering | ||
09:00 - 10:30 | |||
09:00 60mTalk | The Science of Deep Specification DeepSpec Andrew W. Appel Princeton | ||
10:00 30mTalk | CakeML: from functions to machine code with proof all the way DeepSpec Magnus O. Myreen Chalmers University of Technology, Sweden | ||
09:00 - 09:15 | |||
09:00 15mDay opening | Message from the Chairs ISMM | ||
09:00 - 10:30 | |||
09:15 75mTalk | Designing hardware to be free of covert channels by construction FMS Andrew Myers Cornell University | ||
09:00 - 10:30 | |||
09:00 90mOther | Debugging and Profiling Task Parallel Programs with TASKPROF PLDI Tutorials | ||
09:15 - 09:30 | IntroductionMAPL at Columbus Ballroom A Chair(s): Alvin Cheung University of Washington, Justin Gottschlich Intel Labs | ||
09:15 - 10:15 | |||
09:15 60mTalk | Getting to Go ISMM Richard L. Hudson Google | ||
09:30 - 10:30 | |||
09:30 30mTalk | Ariadne: Analysis for Machine Learning Programs MAPL Julian Dolby IBM Thomas J. Watson Research Center, Avraham Shinnar IBM Research, Allison Allain IBM Research, Jenna Reinen IBM Research | ||
10:00 30mTalk | Clone-Hunter: Accelerated Bound Checks Elimination via Binary Code Clone Detection MAPL Hongfa Xue George Washington University, Guru Venkataramani George Washington University, Tian Lan George Washington University | ||
10:30 - 11:00 | |||
10:30 30mCoffee break | Break Catering | ||
10:45 - 12:15 | Reference Counting and Techniques for C-family LanguagesISMM at Discovery AB Chair(s): Emery D. Berger University of Massachusetts, Amherst | ||
10:45 30mTalk | Detailed Heap Profiling ISMM | ||
11:15 30mTalk | FRC: A High-Performance Concurrent Parallel Deferred Reference Counter for C++ ISMM Charles Tripp Terrain Data, USA, David Hyde Stanford University, USA, Benjamin Grossman-Ponemon Terrain Data, USA | ||
11:45 30mTalk | Distributed Garbage Collection for General Graphs ISMM Steven R. Brandt Louisiana State University, Hari Krishnan Facebook, n.n., Costas Busch Louisiana State University, USA, Gokarna Sharma Kent State University, USA | ||
11:00 - 12:00 | |||
11:00 30mTalk | Obfuscation Resilient Search through Executable Classification MAPL Fang-Hsiang Su Columbia University, New York, Jonathan Bell George Mason University, Gail Kaiser Columbia University, New York, Baishakhi Ray Columbia University, New York | ||
11:30 30mTalk | Retrieval on source code: a neural code search MAPL Saksham Sachdev Facebook, Hongyu Li Rice University, Sifei Luan Facebook, Seohyun Kim Facebook, Koushik Sen University of California, Berkeley, Satish Chandra Facebook | ||
11:00 - 12:15 | |||
11:00 30mTalk | Vellvm - Modular Semantics via Interaction Trees DeepSpec Steve Zdancewic University of Pennsylvania | ||
11:30 30mTalk | Crellvm DeepSpec Chung-Kil Hur Seoul National University | ||
11:00 - 12:15 | |||
11:00 75mTalk | Everest: Verifying and Deploying Secure Components in the HTTPS Ecosystem FMS Nikhil Swamy Microsoft Research | ||
11:00 - 12:15 | |||
11:00 75mOther | Debugging and Profiling Task Parallel Programs with TASKPROF PLDI Tutorials | ||
12:15 - 14:00 | |||
12:15 1h45mLunch | Lunch Catering | ||
14:00 - 15:30 | |||
14:00 30mTalk | Relay: A New IR for Machine Learning Frameworks MAPL Jared Roesch University of Washington, USA, Steven Lyubomirsky University of Washington, USA, Logan Weber University of Washington, Josh Pollock University of Washington, Marisa Kirisame , Tianqi Chen , Zachary Tatlock University of Washington, Seattle | ||
14:30 30mTalk | Diesel - DSL for Linear Algebra and Neural Net Computations on GPUs MAPL Venmugil Elango NVIDIA, Norm Rubin NVIDIA, Mahesh Ravishankar , Hari Sandanagobalane NVIDIA, Vinod Grover | ||
15:00 30mTalk | Gen: probabilistic programming with fast custom inference via code generation MAPL File Attached | ||
14:00 - 15:40 | |||
14:00 30mTalk | Verifiable C, a logic and system for proving C programs correct DeepSpec | ||
14:30 30mTalk | Progress Report on the DeepSpec Web Server DeepSpec Benjamin C. Pierce University of Pennsylvania | ||
15:00 30mTalk | QuickChick: Random Testing in Coq DeepSpec Leonidas Lampropoulos University of Pennsylvania | ||
14:00 - 15:30 | |||
14:00 30mTalk | Hardware-Software Co-optimization of Memory Management in Dynamic Languages ISMM | ||
14:30 30mTalk | Dynamic Vertical Memory Scalability for OpenJDK Cloud Applications ISMM Rodrigo Bruno INESC-ID / Instituto Superior Técnico, University of Lisbon, Paulo Ferreira INESC-ID / Instituto Superior Técnico, University of Lisbon, Ruslan Synytsky Jelastic, n.n., Tetiana Fydorenchyk Jelastic, n.n., Jia Rao University of Texas at Arlington, USA, Hang Huang Huazhong University of Science and Technology, China, Song Wu Huazhong University of Science and Technology, China | ||
15:00 30mTalk | OMR: Out-of-Core MapReduce for Large Data Sets ISMM Gurneet Kaur , Keval Vora University of California, Riverside, Sai Charan Koduru University of California, Riverside, Rajiv Gupta UC Riverside | ||
14:00 - 15:40 | |||
14:00 70mTalk | Modular Verification of Deep Specifications of Security-Critical Components FMS Andrew W. Appel Princeton | ||
15:10 30mResearch paper | A Recursive Strategy for Symbolic Execution to Find Exploits in Hardware Designs FMS | ||
14:00 - 15:40 | |||
14:00 1h40mOther | Bayou: Deep Learning over “Big Code” for Program Analysis and Synthesis PLDI Tutorials Swarat Chaudhuri Rice University, Vijayaraghavan Murali Rice University, USA, Chris Jermaine Rice University | ||
15:40 - 16:10 | |||
15:40 30mCoffee break | Break Catering | ||
16:00 - 17:30 | Analyzing the Cache and SchedulingISMM at Discovery AB Chair(s): Michael D. Bond Ohio State University | ||
16:00 30mTalk | mPart: Miss-Ratio Curve Guided Partitioning in Key-Value Stores ISMM Daniel Byrne Michigan Technological University, USA, Nilufer Onder Michigan Technological University, USA, Zhenlin Wang Michigan Technological University | ||
16:30 30mTalk | Prediction and Bounds on Shared Cache Demand from Memory Access Interleaving ISMM Jacob Brock University of Rochester, Chen Ding University of Rochester, Rahman Lavaee , Fangzhou Liu , Liang Yuan Institute of Computing Technology at Chinese Academy of Sciences, China | ||
17:00 30mTalk | Balanced Double Queues for GC Work-Stealing on Weak Memory Models ISMM Michihiro Horie IBM Research - Tokyo, Hiroshi Horii IBM Research, Japan, Kazunori Ogata IBM Research, Japan, Tamiya Onodera IBM, Japan | ||
16:10 - 16:40 | |||
16:10 30mTalk | The Three Pillars of Machine Programming MAPL Justin Gottschlich Intel Labs, Armando Solar-Lezama MIT CSAIL, Nesime Tatbul Intel Labs and MIT, Michael Carbin MIT, Martin C. Rinard Massachusetts Institute of Technology, Regina Barzilay MIT, Saman Amarasinghe MIT, Joshua B. Tenenbaum MIT, Tim Mattson Intel, USA | ||
16:10 - 17:35 | |||
16:10 30mTalk | Real-Time CertiKOS: A Step Toward Resource Adaptive Certified OS Kernels DeepSpec Zhong Shao Yale University | ||
16:40 30mTalk | Verification Around the Hardware-Software Interface: Instruction Set, Processors, and Side Channels DeepSpec Adam Chlipala Massachusetts Institute of Technology, USA | ||
17:10 25mTalk | Using Kami in the field - experiences integrating Kami into SiFive's Chisel/Scala-based design flow DeepSpec Muralidaran Vijayaraghavan SiFive | ||
16:10 - 17:25 | |||
16:10 60mMeeting | Breakout sessions / Discussion FMS | ||
17:10 15mMeeting | Wrapup FMS | ||
16:10 - 17:35 | |||
16:10 85mOther | Bayou: Deep Learning over “Big Code” for Program Analysis and Synthesis PLDI Tutorials Swarat Chaudhuri Rice University, Vijayaraghavan Murali Rice University, USA, Chris Jermaine Rice University | ||
16:40 - 17:00 | Closing RemarksMAPL at Columbus Ballroom A Chair(s): Alvin Cheung University of Washington, Justin Gottschlich Intel Labs | ||
17:00 - 18:00 | |||
18:00 - 19:00 | |||
Tue 19 JunDisplayed time zone: Eastern Time (US & Canada) change
Tue 19 Jun
Displayed time zone: Eastern Time (US & Canada) change
08:00 - 09:00 | |||
08:00 60mOther | Breakfast Catering | ||
08:45 - 10:30 | |||
08:45 10mDay opening | Introduction and Welcome PLMW @ PLDI | ||
08:55 20mSocial Event | Icebreaker PLMW @ PLDI Michelle Strout University of Arizona | ||
09:15 45mTalk | What Programming Language Researchers Do and How to Become One PLMW @ PLDI Kathryn S McKinley Google | ||
10:00 30mTalk | Intermittent Computing Systems PLMW @ PLDI Brandon Lucia Carnegie Mellon University | ||
09:00 - 10:30 | |||
09:00 90mOther | Static Analysis for C++ with Phasar PLDI Tutorials Eric Bodden Heinz Nixdorf Institut, Paderborn University and Fraunhofer IEM, Philipp Dominik Schubert Heinz Nixdorf Institut, Paderborn University, Ben Hermann University of Paderborn | ||
09:00 - 10:30 | |||
09:00 60mTalk | Modularity for Decidability: Implementing and Semi-Automatically Verifying Distributed Systems DeepSpec Mooly Sagiv Tel Aviv University | ||
10:00 30mTalk | Automation for High-Assurance Cryptography, for Primitives and Protocols DeepSpec | ||
09:00 - 10:30 | |||
09:00 15mDay opening | Welcome LCTES | ||
09:15 75mTalk | Keynote: Blockchain and Embedded Systems LCTES | ||
09:00 - 10:30 | |||
09:00 90mOther | Declarative Program Analysis with QL PLDI Tutorials | ||
09:00 - 10:00 | |||
09:00 60mTalk | Tensor Comprehensions: deep learning as a polyhedral compiler's killer app ARRAY Pre-print | ||
10:00 - 10:35 | |||
10:00 35mTalk | A Rosetta Stone for Array Languages ARRAY Artjoms Šinkarovs Heriot-Watt University, UK, Robert Bernecky Snake Island Research, Hans-Nikolai Vießmann Heriot-Watt University, UK, Sven-Bodo Scholz Heriot-Watt University | ||
10:30 - 11:00 | |||
10:30 30mCoffee break | Break Catering | ||
11:00 - 12:15 | |||
11:00 75mOther | Static Analysis for C++ with Phasar PLDI Tutorials Eric Bodden Heinz Nixdorf Institut, Paderborn University and Fraunhofer IEM, Philipp Dominik Schubert Heinz Nixdorf Institut, Paderborn University, Ben Hermann University of Paderborn | ||
11:00 - 12:15 | |||
11:00 45mTalk | Crossing the Divide: Becoming a (Programming Languages) Researcher PLMW @ PLDI Alex Aiken Stanford University | ||
11:45 30mTalk | Program verification using abductive reasoning PLMW @ PLDI Işıl Dillig UT Austin | ||
11:00 - 12:15 | |||
11:00 30mTalk | Towards a formal semantics for GHC Core DeepSpec Stephanie Weirich University of Pennsylvania, USA | ||
11:30 30mTalk | Debugging Debug Information and Beyond DeepSpec Francesco Zappa Nardelli Inria | ||
11:00 - 12:15 | |||
11:00 25mFull-paper | MakeCode and CODAL: Intuitive and Efficient Embedded Systems Programming for Education LCTES James Devine Lancaster University, Joe Finney , Peli de Halleux Microsoft Research, Michał Moskal Microsoft Research, Thomas Ball Microsoft Research, Steve Hodges Microsoft | ||
11:25 25mFull-paper | Compositionality in Scenario-aware Dataflow: A Rendezvous Perspective LCTES | ||
11:50 25mFull-paper | A Memory-Bounded, Deterministic and Terminating Semantics for the Synchronous Programming Language Céu LCTES Guilherme F. Lima PUC-Rio, Rodrigo C. M. Santos PUC-Rio, Edward Hermann Haeusler PUC-Rio, Roberto Ierusalimschy PUC-Rio, Francisco Sant'Anna Rio de Janeiro State University | ||
11:00 - 12:15 | |||
11:00 75mOther | Declarative Program Analysis with QL PLDI Tutorials | ||
11:00 - 12:10 | |||
11:00 35mTalk | Petalisp: Run Time Code Generation for Operations on Strided Arrays ARRAY File Attached | ||
11:35 35mTalk | Profile-Based Vectorization for MATLAB ARRAY Patryk Kiepas MINES ParisTech, France, Jaroslaw Kozlak AGH University of Science and Technology, Poland, Claude Tadonki MINES ParisTech, France, Corinne Ancourt MINES ParisTech, France | ||
12:15 - 14:00 | |||
12:15 1h45mLunch | Lunch Catering | ||
12:50 - 13:50 | |||
12:50 60mLunch | Poster Session & Lunch LCTES | ||
13:15 - 15:30 | |||
13:15 75mOther | Panel: "Charting your Path" PLMW @ PLDI Sara Achour MIT, Shoaib Kamil Adobe, Jennifer B. Sartor Vrije Universiteit Brussel, Zachary Tatlock University of Washington, Seattle | ||
14:30 30mTalk | Evaluating Evaluations PLMW @ PLDI Milind Kulkarni Purdue University | ||
15:00 30mTalk | The Importance of Communication PLMW @ PLDI Michael Carbin MIT | ||
14:00 - 15:40 | |||
14:00 1h40mOther | Static Analysis for C++ with Phasar PLDI Tutorials Eric Bodden Heinz Nixdorf Institut, Paderborn University and Fraunhofer IEM, Philipp Dominik Schubert Heinz Nixdorf Institut, Paderborn University, Ben Hermann University of Paderborn | ||
14:00 - 15:40 | |||
14:00 30mTalk | Multicore and Multithreaded Linking for Concurrent CertiKOS DeepSpec Jieung Kim Yale University, USA | ||
14:30 30mTalk | Verifying seL4 towards Concurrency DeepSpec Thomas Sewell UNSW, Australia | ||
15:00 30mTalk | Specifying and Verifying Concurrent Programs with Ghost State DeepSpec William Mansky Princeton University | ||
14:00 - 15:40 | |||
14:00 25mFull-paper | Adaptive Deep Learning Model Selection on Embedded Systems LCTES Ben Taylor Lancaster University, UK, Vicent Sanz Marco Lancaster University, Willy Wolff Lancaster University, Yehia Elkhatib Lancaster University, Zheng Wang Lancaster University | ||
14:25 25mFull-paper | Optimizing RAID/SSD Controllers with Lifetime Extension for Flash-based SSD Array LCTES Lei Han , Zhaoyan Shen The Hong Kong Polytechnic University, Zili Shao The Hong Kong Polytechnic University, Tao Li University of Florida | ||
14:50 25mFull-paper | Verification of Coarse-Grained Reconfigurable Arrays through Random Test Programs LCTES Bernhard Egger Seoul National University, Eunjin Song Seoul National University, Hochan Lee Seoul National University, Daeyoung Shin Seoul National University | ||
15:15 25mFull-paper | Decoupling Address Generation from Loads and Stores to Improve Data Access Energy Efficiency LCTES Michael Stokes Florida State University, Ryan Baird Florida State University, Zhaoxiang Jin Michigan Technological University, David B. Whalley , Soner Onder Michigan Technological University | ||
14:00 - 15:40 | |||
14:00 1h40mOther | Verified Low-Level Programming in F* PLDI Tutorials Jonathan Protzenko Microsoft Research, Redmond, Nikhil Swamy Microsoft Research, Tahina Ramananandro Microsoft Research, n.n. | ||
14:00 - 15:45 | |||
14:00 35mTalk | Parallel Programming with Arrays in Kappa ARRAY Beatrice Åkerblom Stockholm University, Elias Castegren Uppsala University, Tobias Wrigstad Uppsala University | ||
14:35 35mTalk | Rank Polymorphism Viewed as a Constraint Problem ARRAY Justin Slepak Northeastern University, Panagiotis Manolios Northeastern University, Olin Shivers Northeastern University, USA | ||
15:10 35mTalk | Proving a Core Code for FDM Correct by 2 + dw Tests ARRAY Magne Haveraaen University of Bergen, Norway | ||
15:40 - 16:10 | |||
15:40 30mCoffee break | Break Catering | ||
16:00 - 17:15 | |||
16:00 60mPoster | Poster Session PLMW @ PLDI Milind Kulkarni Purdue University, James Larus EPFL, Adrian Sampson Cornell University, Santosh Nagarakatte Rutgers University, USA, Eva Darulova MPI-SWS, Osbert Bastani Stanford University, Emery D. Berger University of Massachusetts, Amherst, Mayur Naik University of Pennsylvania, Joseph Devietti University of Pennsylvania, Sasa Misailovic University of Illinois at Urbana-Champaign, USA, John Wickerson Imperial College London, Xin Zhang Massachusetts Institute of Technology, USA, Sara Achour MIT, Michael Carbin MIT, Michelle Strout University of Arizona | ||
17:00 15mDay closing | Wrap up PLMW @ PLDI | ||
16:10 - 17:35 | |||
16:10 85mOther | Static Analysis for C++ with Phasar PLDI Tutorials Eric Bodden Heinz Nixdorf Institut, Paderborn University and Fraunhofer IEM, Philipp Dominik Schubert Heinz Nixdorf Institut, Paderborn University, Ben Hermann University of Paderborn | ||
16:10 - 17:35 | |||
16:10 5mTalk | 5-minute Lightning Talks DeepSpec | ||
16:15 5mTalk | Simplicity for Smart Contracts DeepSpec | ||
16:20 5mTalk | Machine-Verified Machine Learning DeepSpec Gordon Stewart Ohio University | ||
16:25 5mTalk | Verification of Union-Find in C DeepSpec | ||
16:30 5mTalk | Narcissus: Deriving Correct-By-Construction Decoders and Encoders from Binary Formats DeepSpec Clément Pit-Claudel MIT CSAIL | ||
16:35 5mTalk | LLVM's IR and Call-By-Push-Value Lambda Calculus DeepSpec | ||
16:40 5mTalk | A Formal Equational Theory for Call-By-Push-Value DeepSpec Christine Rizkallah The University of Melbourne | ||
16:45 5mTalk | Serializability for Distributed Protocols DeepSpec Joonwon Choi Massachusetts Institute of Technology, USA | ||
16:50 5mTalk | A Quick Hack to ask any SMT Solver if my Coq Goal is True DeepSpec Samuel Gruetter Massachusetts Institute of Technology | ||
16:10 - 17:25 | |||
16:25 15mShort-paper | WIP: Deep Neural Networks compiler for a trace-based accelerator LCTES Andre Xian Ming Chang FWDNXT and Purdue, Aliasger Zaidy FWDNXT and Purdue, Lukasz Burzawa FWDNXT and Purdue, Eugenio Culurciello FWDNXT and Purdue | ||
16:40 15mShort-paper | WIP: Statically Relating Program Properties for Efficient Verification LCTES | ||
16:55 15mShort-paper | WIP: Transparent Standby for Low-Power, Resource-Constrained Embedded Systems: A Programming Language-Based Approach LCTES Francisco Sant'Anna Rio de Janeiro State University, Alexandre Sztajnberg Rio de Janeiro State University, Noemi Rodriguez PUC-Rio, Ana Lúcia de Moura | ||
17:10 15mShort-paper | WIP: An open-source realtime computational platform LCTES Pavan Mehrotra Stanford University, Sabar Dasgupta Stanford University, Samantha Robertson Stanford University, Paul Nuyujukian Stanford University Link to publication DOI Pre-print Media Attached | ||
16:10 - 17:35 | |||
16:10 85mOther | Verified Low-Level Programming in F* PLDI Tutorials Jonathan Protzenko Microsoft Research, Redmond, Nikhil Swamy Microsoft Research, Tahina Ramananandro Microsoft Research, n.n. | ||
16:10 - 17:20 | |||
16:10 35mTalk | Inner Array Inlining for Structure of Arrays Layout ARRAY Matthias Springer Tokyo Institute of Technology, Yaozhu Sun Tokyo Institute of Technology, Hidehiko Masuhara Tokyo Institute of Technology Pre-print | ||
16:45 35mTalk | An Array API for Finite Difference Methods ARRAY Eva Burrows University of Bergen, Norway, Helmer André Friis IRIS, Norway, Magne Haveraaen University of Bergen, Norway | ||
17:30 - 18:30 | |||
Wed 20 JunDisplayed time zone: Eastern Time (US & Canada) change
Wed 20 Jun
Displayed time zone: Eastern Time (US & Canada) change
08:00 - 08:45 | |||
08:00 45mOther | Breakfast Catering | ||
08:45 - 09:00 | WelcomePLDI Invited Speakers at Grand Ballroom Chair(s): Jeffrey S. Foster University of Maryland, College Park / Tufts University, Dan Grossman University of Washington | ||
09:00 - 10:00 | KeynotePLDI Invited Speakers at Grand Ballroom Chair(s): Michael Hicks University of Maryland, College Park | ||
09:00 60mTalk | Language-Integrated Verification PLDI Invited Speakers Ranjit Jhala University of California, San Diego Media Attached | ||
10:00 - 10:30 | Lightning Overview - Day 1PLDI Research Papers at Grand Ballroom Chair(s): Dan Grossman University of Washington | ||
10:30 - 11:00 | |||
10:30 30mCoffee break | Break Catering | ||
11:00 - 12:15 | |||
11:00 25mTalk | Verifying That Web Pages Have Accessible Layout PLDI Research Papers Pavel Panchekha University of Washington, Adam T. Geller University of Washington, USA, Michael D. Ernst University of Washington, USA, Zachary Tatlock University of Washington, Seattle, Shoaib Kamil Adobe Media Attached | ||
11:25 25mTalk | BLeak: Automatically Debugging Memory Leaks in Web Applications PLDI Research Papers John Vilk University of Massachusetts, Amherst, Emery D. Berger University of Massachusetts, Amherst Media Attached | ||
11:50 25mTalk | Putting in All the Stops: Execution Control for JavaScript PLDI Research Papers Samuel Baxter University of Massachusetts at Amherst, USA, Rachit Nigam , Joe Gibbs Politz University of California, San Diego, Shriram Krishnamurthi Brown University, USA, Arjun Guha University of Massachusetts, Amherst Media Attached | ||
11:00 - 12:15 | Emerging HardwarePLDI Research Papers at Grand Ballroom CD Chair(s): Ryan R. Newton Indiana University | ||
11:00 25mTalk | Persistency for Synchronization-Free Regions PLDI Research Papers Vaibhav Gogte University of Michigan, USA, Stephan Diestelhorst ARM Research, UK, William Wang Arm Research, UK, Satish Narayanasamy University of Michigan, Peter M. Chen University of Michigan, USA, Thomas F. Wenisch University of Michigan, USA Media Attached | ||
11:25 25mTalk | Write-Rationing Garbage Collection for Hybrid Memories PLDI Research Papers Shoaib Akram Ghent University, Jennifer B. Sartor Vrije Universiteit Brussel, Kathryn S McKinley Google, Lieven Eeckhout Ghent University, Belgium Media Attached | ||
11:50 25mTalk | Mapping Spiking Neural Networks onto a Manycore Neuromorphic Architecture PLDI Research Papers Chit-Kwan Lin Intel Labs, n.n., Andreas Wild Intel Labs, n.n., Tsung-Han Lin Intel Labs, n.n., Gautham N. Chinya Intel Labs, n.n., Mike Davies Intel Labs, n.n., Hong Wang Intel Labs, n.n. Media Attached | ||
12:15 - 14:00 | |||
12:15 1h45mLunch | Lunch Catering | ||
14:00 - 15:40 | Concurrency and TerminationPLDI Research Papers at Grand Ballroom AB Chair(s): Iulian Neamtiu New Jersey Institute of Technology | ||
14:00 25mTalk | Static Serializability Analysis for Causal Consistency PLDI Research Papers Lucas Brutschy ETH Zurich, Dimitar Dimitrov ETH Zurich, Switzerland, Peter Müller ETH Zurich, Martin Vechev ETH Zürich | ||
14:25 25mTalk | CUBA: Interprocedural Context-UnBounded Analysis of Concurrent Programs PLDI Research Papers Media Attached | ||
14:50 25mTalk | Symbolic Reasoning for Automatic Signal Placement PLDI Research Papers Kostas Ferles UT Austin, Jacob Van Geffen UT Austin, Işıl Dillig UT Austin, Yannis Smaragdakis University of Athens Media Attached | ||
15:15 25mTalk | Advanced Automata-Based Algorithms for Program Termination Checking PLDI Research Papers Yu-Fang Chen , Matthias Heizmann University of Freiburg, Germany, Ondřej Lengál Brno University of Technology , Yong Li Institute of Software, Chinese Academy of Sciences, Ming-Hsien Tsai Academia Sinica, Taiwan, Andrea Turrini State Key Laboratory of Computer Science, Institute of Software, Chinese Academy of Sciences, Lijun Zhang Institute of Software, Chinese Academy of Sciences Media Attached | ||
14:00 - 15:40 | Dynamic TechniquesPLDI Research Papers at Grand Ballroom CD Chair(s): Sorin Lerner University of California, San Diego | ||
14:00 25mTalk | HHVM JIT: A Profile-Guided, Region-Based Compiler for PHP and Hack PLDI Research Papers Guilherme Ottoni Facebook Media Attached | ||
14:25 25mTalk | On-Stack Replacement, Distilled PLDI Research Papers Media Attached | ||
14:50 25mTalk | EffectiveSan: Type and Memory Error Detection using Dynamically Typed C/C++ PLDI Research Papers Gregory J. Duck National University of Singapore, Singapore, Roland H. C. Yap National University of Singapore, Singapore Media Attached | ||
15:15 25mTalk | Calling-to-Reference Context Translation via Constraint-Guided CFL-Reachability PLDI Research Papers Cheng Cai University of California, Irvine, Qirun Zhang University of California, Davis, Zhiqiang Zuo Nanjing University, China, Khanh Nguyen University of California, Irvine, Harry Xu University of California, Los Angeles (UCLA), Zhendong Su University of California, Davis Media Attached | ||
15:40 - 16:10 | |||
15:40 30mCoffee break | Break Catering | ||
16:10 - 17:25 | Transactions and RacesPLDI Research Papers at Grand Ballroom AB Chair(s): Tatiana Shpeisman Google Brain | ||
16:10 25mTalk | The Semantics of Transactions and Weak Memory in x86, Power, ARM, and C++ PLDI Research Papers Nathan Chong ARM Ltd., Tyler Sorensen Imperial College London, John Wickerson Imperial College London Media Attached | ||
16:35 25mTalk | MixT: A Language for Mixing Consistency in Geodistributed Transactions PLDI Research Papers Media Attached | ||
17:00 25mTalk | Bounding Data Races in Space and Time PLDI Research Papers Stephen Dolan University of Cambridge, KC Sivaramakrishnan University of Cambridge, Anil Madhavapeddy OCaml Labs Media Attached | ||
16:10 - 17:25 | |||
16:10 25mTalk | Finding Root Causes of Floating Point Error PLDI Research Papers Alex Sanchez-Stern University of California, San Diego, Pavel Panchekha University of Washington, Sorin Lerner University of California, San Diego, Zachary Tatlock University of Washington, Seattle Media Attached | ||
16:35 25mTalk | Ryū: Fast Float-to-String Conversion PLDI Research Papers Ulf Adams Google, Germany Media Attached | ||
17:00 25mTalk | To-Many or To-One? All-in-One! Efficient Purely Functional Multi-maps with Type-Heterogeneous Hash-Tries PLDI Research Papers Michael J. Steindorfer Delft University of Technology, Jurgen Vinju Centrum Wiskunde & Informatica / Technische Universiteit Eindhoven / SWAT.engineering BV Media Attached | ||
17:30 - 18:30 | Program Chair's Report and SIGPLAN Town Hall MeetingPLDI Invited Speakers at Grand Ballroom AB Chair(s): Dan Grossman University of Washington, Michael Hicks University of Maryland, College Park | ||
17:30 30mTalk | PLDI Program Chair's Report PLDI Invited Speakers Dan Grossman University of Washington Media Attached | ||
18:00 30mTalk | SIGPLAN Town Hall Meeting PLDI Invited Speakers Michael Hicks University of Maryland, College Park, Benjamin C. Pierce University of Pennsylvania, Steve Blackburn Australian National University Media Attached | ||
18:00 - 21:00 | |||
Thu 21 JunDisplayed time zone: Eastern Time (US & Canada) change
Thu 21 Jun
Displayed time zone: Eastern Time (US & Canada) change
08:00 - 09:00 | |||
08:00 45mOther | Breakfast Catering | ||
08:45 - 09:00 | PLDI 2019 IntroductionPLDI Invited Speakers at Grand Ballroom Chair(s): Kathleen Fisher Tufts University, Kathryn S McKinley Google | ||
08:45 15mTalk | PLDI 2019 Introduction PLDI Invited Speakers Media Attached | ||
09:00 - 10:00 | KeynotePLDI Invited Speakers at Grand Ballroom Chair(s): Cormac Flanagan University of California, Santa Cruz | ||
09:00 60mTalk | Machine Learning: Alchemy for the Modern Computer Scientist PLDI Invited Speakers Media Attached | ||
10:00 - 10:30 | Lightning Overview - Day 2PLDI Research Papers at Grand Ballroom Chair(s): Dan Grossman University of Washington | ||
10:30 - 11:00 | |||
10:30 30mCoffee break | Break Catering | ||
11:00 - 12:15 | Multicore and MorePLDI Research Papers at Grand Ballroom AB Chair(s): Yannis Smaragdakis University of Athens | ||
11:00 25mTalk | Spatial: A Language and Compiler for Application Accelerators PLDI Research Papers David Koeplinger Stanford University, USA, Matthew Feldman Stanford University, USA, Raghu Prabhakar Stanford University, USA, Yaqi Zhang Stanford University, USA, Stefan Hadjis Stanford University, USA, Ruben Fiszel EPFL, Switzerland, Tian Zhao Stanford University, Luigi Nardi Stanford University, Ardavan Pedram Stanford University, USA, Christos Kozyrakis Stanford University, USA, Kunle Olukotun Stanford University Media Attached | ||
11:25 25mTalk | Enhancing Computation-to-Core Assignment with Physical Location Information PLDI Research Papers Orhan Kislal Pennsylvania State University, USA, Jagadish Kotra Pennsylvania State University, USA, Xulong Tang Penn State, Mahmut Taylan Kandemir University of Pennsylvania, Myoungsoo Jung Yonsei University, South Korea Media Attached | ||
11:50 25mTalk | SWOOP: Software-Hardware Co-design for Non-speculative, Execute-Ahead, In-Order Cores PLDI Research Papers Kim-Anh Tran Uppsala University, Sweden, Alexandra Jimborean Uppsala University, Trevor E. Carlson National University of Singapore, Konstantinos Koukos Uppsala University, Sweden, Magnus Själander Norwegian University of Science and Technology (NTNU), Stefanos Kaxiras Uppsala University, Sweden Media Attached | ||
11:00 - 12:30 | |||
12:30 - 14:00 | |||
12:30 90mLunch | Lunch Catering | ||
14:00 - 15:40 | Concurrency DebuggingPLDI Research Papers at Grand Ballroom AB Chair(s): Tony Hosking Australian National University / Data61 | ||
14:00 25mTalk | iReplayer: In-situ and Identical Record-and-Replay for Multithreaded Applications PLDI Research Papers Hongyu Liu University of Texas at San Antonio, USA, Sam Silvestro University of Texas at San Antonio, USA, Wei Wang University of Texas at San Antonio, USA, Chen Tian Huawei Lab, USA, Tongping Liu Media Attached | ||
14:25 25mTalk | D4: Fast Concurrency Debugging with Parallel Differential Analysis PLDI Research Papers Media Attached | ||
14:50 25mTalk | High-Coverage, Unbounded Sound Predictive Race Detection PLDI Research Papers Jake Roemer Ohio State University, Kaan Genç Ohio State University, USA, Michael D. Bond Ohio State University Media Attached | ||
15:15 25mTalk | CURD: A Dynamic CUDA Race Detector PLDI Research Papers Media Attached | ||
14:00 - 15:40 | Synthesis and LearningPLDI Research Papers at Grand Ballroom CD Chair(s): Xin Zhang Massachusetts Institute of Technology, USA | ||
14:00 25mTalk | A General Path-Based Representation for Predicting Program Properties PLDI Research Papers Uri Alon Technion, Meital Zilberstein Technion, Omer Levy University of Washington, USA, Eran Yahav Technion Media Attached | ||
14:25 25mTalk | Program Synthesis using Conflict-Driven Learning PLDI Research Papers Yu Feng University of Texas at Austin, USA, Ruben Martins Carnegie Mellon University, Osbert Bastani Stanford University, Işıl Dillig UT Austin Media Attached | ||
14:50 25mTalk | Accelerating Search-Based Program Synthesis using Learned Probabilistic Models PLDI Research Papers Woosuk Lee University of Pennsylvania, USA, Kihong Heo University of Pennsylvania, USA, Rajeev Alur University of Pennsylvania, Mayur Naik University of Pennsylvania Media Attached | ||
15:15 25mTalk | Inferring Crypto API Rules from Code Changes PLDI Research Papers Rumen Atanasov Paletov , Petar Tsankov ETH Zurich, Veselin Raychev ETH Zurich, Martin Vechev ETH Zürich Media Attached | ||
15:40 - 16:10 | |||
15:40 30mCoffee break | Break Catering | ||
16:10 - 17:00 | Programming-Student FeedbackPLDI Research Papers at Grand Ballroom AB Chair(s): Dan Grossman University of Washington | ||
16:10 25mTalk | Automated Clustering and Program Repair for Introductory Programming Assignments PLDI Research Papers Sumit Gulwani Microsoft Research, Ivan Radiček Vienna University of Technology, Austria, Florian Zuleger TU Vienna Media Attached | ||
16:35 25mTalk | Search, Align, and Repair: Data-Driven Feedback Generation for Introductory Programming Exercises PLDI Research Papers Ke Wang University of California at Davis, USA, Rishabh Singh Google Brain, Zhendong Su University of California, Davis Media Attached | ||
16:10 - 17:00 | Analyzing Probabilistic ProgramsPLDI Research Papers at Grand Ballroom CD Chair(s): Eva Darulova MPI-SWS | ||
16:10 25mTalk | Bounded Expectations: Resource Analysis for Probabilistic Programs PLDI Research Papers Van Chan Ngo Carnegie Mellon University, Quentin Carbonneaux Yale University, Jan Hoffmann Carnegie Mellon University Media Attached | ||
16:35 25mTalk | PMAF: An Algebraic Framework for Static Analysis of Probabilistic Programs PLDI Research Papers Di Wang Carnegie Mellon University, Jan Hoffmann Carnegie Mellon University, Thomas Reps University of Wisconsin - Madison and GrammaTech, Inc. Media Attached | ||
17:00 - 18:00 | |||
17:30 - 18:30 | SIGPLAN and SRC AwardsPLDI Invited Speakers at Grand Ballroom Chair(s): Maria Christakis MPI-SWS, Satnam Singh X, the moonshot factory | ||
Fri 22 JunDisplayed time zone: Eastern Time (US & Canada) change
Fri 22 Jun
Displayed time zone: Eastern Time (US & Canada) change
08:00 - 09:00 | |||
08:00 60mOther | Breakfast Catering | ||
09:00 - 10:00 | KeynotePLDI Invited Speakers at Grand Ballroom Chair(s): Emery D. Berger University of Massachusetts, Amherst | ||
09:00 60mTalk | A “Post-ISA” Era in Computer Systems: Challenges and Opportunities PLDI Invited Speakers Media Attached | ||
10:00 - 10:30 | Lightning Overview - Day 3PLDI Research Papers at Grand Ballroom Chair(s): Dan Grossman University of Washington | ||
10:30 - 11:00 | |||
10:30 30mCoffee break | Break Catering | ||
11:00 - 12:15 | Optimization and LocalityPLDI Research Papers at Grand Ballroom AB Chair(s): Milind Kulkarni Purdue University | ||
11:00 25mTalk | Polyhedral Auto-transformation with No Integer Linear Programming PLDI Research Papers Aravind Acharya Indian Institute of Science, Bangalore, Uday Bondhugula Indian Institute of Science, Albert Cohen Inria, France / ENS, France Media Attached | ||
11:25 25mTalk | Partial Control-Flow Linearization PLDI Research Papers Media Attached | ||
11:50 25mTalk | Locality Analysis through Static Parallel Sampling PLDI Research Papers Dong Chen University of Rochester, Fangzhou Liu University of Rochester, Chen Ding University of Rochester, Sreepathi Pai University of Rochester Media Attached | ||
11:00 - 12:15 | Inference for Probabilistic ProgramsPLDI Research Papers at Grand Ballroom CD Chair(s): Arjun Guha University of Massachusetts, Amherst | ||
11:00 25mTalk | Incremental Inference for Probabilistic Programs PLDI Research Papers Marco Cusumano-Towner MIT-CSAIL, Benjamin Bichsel ETH Zurich, Switzerland, Timon Gehr , Martin Vechev ETH Zürich, Vikash K. Mansinghka MIT Media Attached | ||
11:25 25mTalk | Bayonet: Probabilistic Inference for Networks PLDI Research Papers Timon Gehr , Sasa Misailovic University of Illinois at Urbana-Champaign, USA, Petar Tsankov ETH Zurich, Laurent Vanbever ETH Zürich, Pascal Wiesmann ETH Zurich, Switzerland, Martin Vechev ETH Zürich Media Attached | ||
11:50 25mTalk | Probabilistic Programming with Programmable Inference PLDI Research Papers Vikash K. Mansinghka MIT, Ulrich Schaechtle Massachusetts Institute of Technology, USA, Shivam Handa , Alexey Radul , Yutian Chen Google Deepmind, n.n., Martin C. Rinard Massachusetts Institute of Technology Media Attached | ||
12:15 - 14:00 | |||
12:15 1h45mLunch | Lunch Catering | ||
14:00 - 15:40 | VerificationPLDI Research Papers at Grand Ballroom AB Chair(s): Adam Chlipala Massachusetts Institute of Technology, USA | ||
14:00 25mTalk | VeriPhy: Verified Controller Executables from Verified Cyber-Physical System Models PLDI Research Papers Brandon Bohrer , Yong Kiam Tan Carnegie Mellon University, USA, Stefan Mitsch Carnegie Mellon University, USA, Magnus O. Myreen Chalmers University of Technology, Sweden, André Platzer Carnegie Mellon University Media Attached | ||
14:25 25mTalk | Crellvm: Verified Credible Compilation for LLVM PLDI Research Papers Jeehoon Kang Seoul National University, Yoonseung Kim Seoul National University (South Korea), Youngju Song Seoul National University, Juneyoung Lee Seoul National University, Sanghoon Park Seoul National University, South Korea, Mark Dongyeon Shin Seoul National University, South Korea, Yonghyun Kim Seoul National University, South Korea, Sungkeun Cho Seoul National University, South Korea, Joonwon Choi Massachusetts Institute of Technology, USA, Chung-Kil Hur Seoul National University, Kwangkeun Yi Seoul National University Media Attached | ||
14:50 25mTalk | Certified Concurrent Abstraction Layers PLDI Research Papers Ronghui Gu Columbia University, Zhong Shao Yale University, Jieung Kim Yale University, USA, Xiongnan (Newman) Wu Yale University, Jérémie Koenig , Vilhelm Sjöberg Yale University, Hao Chen Yale University, David Costanzo Yale University, Tahina Ramananandro Microsoft Research, n.n. Media Attached | ||
15:15 25mTalk | Modularity for Decidability of Deductive Verification with Applications to Distributed Systems PLDI Research Papers Marcelo Taube Tel Aviv University, Israel, Giuliano Losa University of California at Los Angeles, USA, Kenneth L. McMillan Microsoft Research, Oded Padon Tel Aviv University, Mooly Sagiv Tel Aviv University, Sharon Shoham Tel Aviv university, James R. Wilcox University of Washington, Doug Woos University of Washington Media Attached | ||
14:00 - 15:40 | |||
14:00 25mTalk | Active Learning of Points-To Specifications PLDI Research Papers Osbert Bastani Stanford University, Rahul Sharma Microsoft Research, Alex Aiken Stanford University, Percy Liang Stanford University Media Attached | ||
14:25 25mTalk | Pinpoint: Fast and Precise Sparse Value Flow Analysis for Million Lines of Code PLDI Research Papers Qingkai Shi Hong Kong University of Science and Technology, China, Xiao Xiao SourceBrella Inc., Rongxin Wu Department of Computer Science and Engineering, The Hong Kong University of Science and Technology, Jinguo Zhou Sourcebrella Inc., Gang Fan , Charles Zhang Media Attached | ||
14:50 25mTalk | A Data-Driven CHC Solver PLDI Research Papers Media Attached | ||
15:15 25mTalk | User-Guided Program Reasoning using Bayesian Inference PLDI Research Papers Mukund Raghothaman University of Pennsylvania, Sulekha Kulkarni Georgia Tech, Kihong Heo University of Pennsylvania, USA, Mayur Naik University of Pennsylvania Media Attached | ||
15:40 - 16:10 | |||
15:40 30mCoffee break | Break Catering | ||
16:10 - 17:25 | ParallelismPLDI Research Papers at Grand Ballroom AB Chair(s): Julian Dolby IBM Thomas J. Watson Research Center | ||
16:10 25mTalk | GPU Code Optimization using Abstract Kernel Emulation and Sensitivity Analysis PLDI Research Papers Changwan Hong , Aravind Sukumaran-Rajam Ohio State University, USA, Jinsung Kim Ohio State University, USA, Prashant Singh Rawat , Sriram Krishnamoorthy Pacific Northwest National Laboratories, Louis-Noël Pouchet Colorado State University, Fabrice Rastello INRIA, P. Sadayappan Ohio State University Media Attached | ||
16:35 25mTalk | Gluon: A Communication-Optimizing Substrate for Distributed Heterogeneous Graph Analytics PLDI Research Papers Roshan Dathathri University of Texas at Austin, USA, Gurbinder Gill University of Texas at Austin, USA, Loc Hoang University of Texas at Austin, USA, Hoang-Vu Dang University of Illinois at Urbana-Champaign, USA, Alex Brooks University of Illinois at Urbana-Champaign, USA, Nikoli Dryden University of Illinois at Urbana-Champaign, USA, Marc Snir UIUC, Keshav Pingali University of Texas at Austin, USA Media Attached | ||
17:00 25mTalk | Heartbeat Scheduling: Provable Efficiency for Nested Parallelism PLDI Research Papers Umut A. Acar Carnegie Mellon University, Arthur Charguéraud Inria, Adrien Guatto , Mike Rainey , Filip Sieczkowski University of Wrocław Media Attached | ||
16:10 - 17:25 | |||
16:10 25mTalk | Guarded Impredicative Polymorphism PLDI Research Papers Alejandro Serrano Utrecht University, Jurriaan Hage Utrecht University, Dimitrios Vytiniotis Microsoft Research, Cambridge, Simon Peyton Jones Microsoft Research Media Attached | ||
16:35 25mTalk | Typed Closure Conversion for the Calculus of Constructions PLDI Research Papers Media Attached | ||
17:00 25mTalk | Inferring Type Rules for Syntactic Sugar PLDI Research Papers Media Attached | ||