POPL 2018
Sun 7 - Sat 13 January 2018 Los Angeles, California, United States
POPL 2018 (series) / Omni Hotel /

Room information: Bunker Hill

VenueOmni Hotel
Room nameBunker Hill
Floor0
Room InformationNo extra information available
Program

You're viewing the program in a time zone which is different from your device's time zone change time zone

Wed 10 Jan

Displayed time zone: Tijuana, Baja California change

10:30 - 12:10
StringsResearch Papers at Bunker Hill
Chair(s): Zachary Tatlock University of Washington, Seattle
10:30
25m
Talk
Synthesizing Bijective Lenses
Research Papers
Anders Miltner Princeton University, Kathleen Fisher Tufts University, Benjamin C. Pierce University of Pennsylvania, David Walker Princeton University, Steve Zdancewic University of Pennsylvania
10:55
25m
Talk
WebRelate: Integrating Web Data with Spreadsheets using Examples
Research Papers
Jeevana Priya Inala MIT, Rishabh Singh Microsoft Research
11:20
25m
Talk
What's Decidable About String Constraints with ReplaceAll Function?
Research Papers
Taolue Chen Birkbeck, University of London, Yan Chen State Key Laboratory of Computer Science, Institute of Software, Chinese Academy of Sciences & University of Chinese Academy of Sciences, Matthew Hague Royal Holloway, University of London, Anthony Widjaja Lin Oxford University, Zhilin Wu State Key Laboratory of Computer Science, Institute of Software, Chinese Academy of Sciences
11:45
25m
Talk
String Constraints with Concatenation and Transducers Solved Efficiently
Research Papers
Lukáš Holík Brno University of Technology, Anthony Widjaja Lin Oxford University, Petr Janků Brno University of Technology, Philipp Ruemmer Uppsala University, Tomáš Vojnar Brno University of Technology
13:40 - 15:20
Verification IResearch Papers at Bunker Hill
Chair(s): Zhong Shao Yale University
13:40
25m
Talk
Automated Lemma Synthesis in Symbolic-Heap Separation Logic
Research Papers
Quang-Trung Ta National University of Singapore, Ton Chanh Le National University of Singapore, Siau-Cheng Khoo National University of Singapore, Wei-Ngan Chin National University of Singapore
14:05
25m
Talk
Foundations for Natural Proofs and Quantifier Instantiation
Research Papers
Christof Löding RWTH Aachen University, P. Madhusudan University of Illinois at Urbana-Champaign, Lucas Peña University of Illinois at Urbana-Champaign
14:30
25m
Talk
Higher-Order Constrained Horn Clauses for Verification
Research Papers
Toby Cathcart Burn University of Oxford, C.-H. Luke Ong University of Oxford, Steven Ramsay University of Bristol
14:55
25m
Talk
Relatively Complete Refinement Type System for Verification of Higher-Order Non-Deterministic Programs
Research Papers
Hiroshi Unno University of Tsukuba, Yuki Satake University of Tsukuba, Tachio Terauchi Waseda University
15:50 - 17:30
Memory and ConcurrencyResearch Papers at Bunker Hill
Chair(s): Azadeh Farzan University of Toronto
15:50
25m
Talk
Effective Stateless Model Checking for C/C++ Concurrency
Research Papers
Michalis Kokologiannakis National Technical University of Athens, Greece, Ori Lahav Tel Aviv University, Israel, Konstantinos (Kostis) Sagonas , Viktor Vafeiadis MPI-SWS, Germany
16:15
25m
Talk
Transactions in Relaxed Memory Architectures
Research Papers
Brijesh Dongol Brunel University London, Radha Jagadeesan DePaul University, James Riely DePaul University
Link to publication DOI Pre-print Media Attached
16:40
25m
Talk
Simplifying ARM Concurrency: Multicopy-Atomic Axiomatic and Operational Models for ARMv8
Research Papers
Christopher Pulte University of Cambridge, Shaked Flur University of Cambridge, Will Deacon ARM Ltd., Jon French University of Cambridge, Susmit Sarkar University of St. Andrews, Peter Sewell University of Cambridge
17:05
25m
Talk
Progress of Concurrent Objects with Partial Methods
Research Papers
Hongjin Liang University of Science and Technology of China, Xinyu Feng University of Science and Technology of China

Thu 11 Jan

Displayed time zone: Tijuana, Baja California change

10:30 - 12:10
ConsistencyResearch Papers at Bunker Hill
Chair(s): Xinyu Feng University of Science and Technology of China
10:30
25m
Talk
Sound, Complete, and Tractable Linearizability Monitoring for Concurrent Collections
Research Papers
Michael Emmi Nokia Bell Labs, Constantin Enea Université Paris Diderot
10:55
25m
Talk
Reducing Liveness to Safety in First-Order Logic
Research Papers
Oded Padon Tel Aviv University, Jochen Hoenicke Universität Freiburg, Giuliano Losa University of California at Los Angeles, USA, Andreas Podelski University of Freiburg, Germany, Mooly Sagiv Tel Aviv University, Sharon Shoham Tel Aviv university
11:20
25m
Talk
Alone Together: Compositional Reasoning and Inference for Weak Isolation
Research Papers
Gowtham Kaki Purdue University, Kartik Nagar Purdue University, Mahsa Najafzadeh Purdue University, Suresh Jagannathan Purdue University
11:45
25m
Talk
Programming and Proving with Distributed Protocols
Research Papers
Ilya Sergey University College London, James R. Wilcox University of Washington, Zachary Tatlock University of Washington, Seattle
DOI Pre-print
13:40 - 15:20
TerminationResearch Papers at Bunker Hill
Chair(s): Constantin Enea Université Paris Diderot
13:40
25m
Talk
A new proof rule for almost-sure termination
Research Papers
Annabelle McIver Macquarie University, Carroll Morgan University of New South Wales; Data 61, Benjamin Lucien Kaminski RWTH Aachen University; University College London, Joost-Pieter Katoen RWTH Aachen University
14:05
25m
Talk
Lexicographic Ranking Supermartingales: An Efficient Approach to Termination of Probabilistic Programs
Research Papers
Sheshansh Agrawal IIT Bombay, Krishnendu Chatterjee IST Austria, Petr Novotný IST Austria
14:30
25m
Talk
Algorithmic Analysis of Termination Problems for Quantum Programs
Research Papers
Yangjia Li Institute of Software, Chinese Academy of Sciences, Mingsheng Ying University of Technology Sydney
14:55
25m
Talk
Monadic refinements for relational cost analysis
Research Papers
Ivan Radicek TU Vienna, Gilles Barthe IMDEA Software Institute, Marco Gaboardi University at Buffalo, SUNY, Deepak Garg Max Planck Institute for Software Systems, Florian Zuleger TU Vienna
15:50 - 16:40
Language DesignResearch Papers at Bunker Hill
Chair(s): Zachary Tatlock University of Washington, Seattle
15:50
25m
Talk
An Axiomatic Basis for Bidirectional Programming
Research Papers
Hsiang-Shang ‘Josh’ Ko National Institute of Informatics, Japan, Zhenjiang Hu National Institute of Informatics
Link to publication DOI Pre-print Media Attached File Attached
16:15
25m
Talk
Simplicitly: Foundations and Applications of Implicit Function Types
Research Papers
Martin Odersky EPFL, Switzerland, Olivier Blanvillain EPFL, Fengyun Liu EPFL, Switzerland, Aggelos Biboudis Ecole Polytechnique Federale de Lausanne, Heather Miller Ecole Polytechnique Federale de Lausanne, Sandro Stucki EPFL

Fri 12 Jan

Displayed time zone: Tijuana, Baja California change

10:30 - 12:10
Testing and VerificationResearch Papers at Bunker Hill
Chair(s): Santosh Nagarakatte Rutgers University, USA
10:30
25m
Talk
Generating Good Generators for Inductive Relations
Research Papers
Leonidas Lampropoulos University of Pennsylvania, Zoe Paraskevopoulou Princeton University, Benjamin C. Pierce University of Pennsylvania
10:55
25m
Talk
Why is Random Testing Effective for Partition Tolerance Bugs?
Research Papers
Rupak Majumdar MPI-SWS, Filip Niksic MPI-SWS
11:20
25m
Talk
On Automatically Proving the Correctness of math.h Implementations
Research Papers
Wonyeol Lee Stanford University, Rahul Sharma Microsoft Research, Alex Aiken Stanford University
11:45
25m
Talk
Online Detection of Effectively Callback Free Objects with Applications to Smart Contracts
Research Papers
Shelly Grossman Tel Aviv University, Ittai Abraham VMWare Research, Guy Gueta VMWare Research, Yan Michalevsky Stanford University, Noam Rinetzky Tel Aviv University, Mooly Sagiv Tel Aviv University, Yoni Zohar Tel Aviv University
13:30 - 15:20
Program Analysis IIResearch Papers at Bunker Hill
Chair(s): Işıl Dillig UT Austin
13:30
10m
Awards
SRC Awards
Research Papers
Benjamin Delaware Purdue University
13:30
22m
Talk
Refinement Reflection: Complete Verification with SMT
Research Papers
Niki Vazou University of Maryland, Anish Tondwalkar UCSD, Vikraman Choudhury , Ryan Scott Indiana University, Ryan R. Newton Indiana University, Philip Wadler University of Edinburgh, UK, Ranjit Jhala University of California, San Diego
14:05
25m
Talk
Non-Linear Reasoning For Invariant Synthesis
Research Papers
Zachary Kincaid Princeton University, John Cyphert University of Wisconsin - Madison, Jason Breck University of Wisconsin - Madison, Thomas Reps University of Wisconsin - Madison and GrammaTech, Inc.
14:30
25m
Talk
A Practical Construction for Decomposing Numerical Abstract Domains
Research Papers
Gagandeep Singh , Markus Püschel ETH Zürich, Martin Vechev ETH Zürich
14:55
25m
Talk
Verifying Equivalence of Database-Driven Applications
Research Papers
Yuepeng Wang University of Texas at Austin, Işıl Dillig UT Austin, Shuvendu K. Lahiri Microsoft Research, William Cook University of Texas at Austin
15:50 - 17:05
SynthesisResearch Papers at Bunker Hill
Chair(s): Nadia Polikarpova University of California, San Diego
15:50
25m
Talk
Strategy Synthesis for Linear Arithmetic Games
Research Papers
Azadeh Farzan University of Toronto, Zachary Kincaid Princeton University
16:15
25m
Talk
Bonsai: Synthesis-Based Reasoning for Type Systems
Research Papers
Kartik Chandra Stanford University, Rastislav Bodík University of Washington
16:40
25m
Talk
Program Synthesis using Abstraction Refinement
Research Papers
Xinyu Wang UT Austin, Işıl Dillig UT Austin, Rishabh Singh Microsoft Research

Wed 10 Jan

Displayed time zone: Tijuana, Baja California change

Room10:003011:003012:003013:003014:003015:003016:003017:0030
Bunker Hill

Research Papers

Strings

Research Papers

Verification I

Research Papers

Memory and Concurrency

Thu 11 Jan

Displayed time zone: Tijuana, Baja California change

Room10:003011:003012:003013:003014:003015:003016:0030
Bunker Hill

Research Papers

Consistency

Research Papers

Termination

Research Papers

Language Design

Fri 12 Jan

Displayed time zone: Tijuana, Baja California change

Room10:003011:003012:003013:003014:003015:003016:003017:0030
Bunker Hill

Research Papers

Testing and Verification

Research Papers

Program Analysis II

Research Papers

Synthesis

Wed 10 Jan

Displayed time zone: Tijuana, Baja California change

Room10:0015304511:0015304512:0015304513:0015304514:0015304515:0015304516:0015304517:00153045
Bunker Hill
POPL Research Papers
Synthesizing Bijective Lenses
10:30 - 10:55
POPL Research Papers
WebRelate: Integrating Web Data with Spreadsheets using Examples
10:55 - 11:20
POPL Research Papers
What's Decidable About String Constraints with ReplaceAll Function?
11:20 - 11:45
POPL Research Papers
String Constraints with Concatenation and Transducers Solved Efficiently
11:45 - 12:10
POPL Research Papers
Automated Lemma Synthesis in Symbolic-Heap Separation Logic
13:40 - 14:05
POPL Research Papers
Foundations for Natural Proofs and Quantifier Instantiation
14:05 - 14:30
POPL Research Papers
Higher-Order Constrained Horn Clauses for Verification
14:30 - 14:55
POPL Research Papers
Relatively Complete Refinement Type System for Verification of Higher-O ...
14:55 - 15:20
POPL Research Papers
Effective Stateless Model Checking for C/C++ Concurrency
15:50 - 16:15
POPL Research Papers
Transactions in Relaxed Memory Architectures
16:15 - 16:40
POPL Research Papers
Simplifying ARM Concurrency: Multicopy-Atomic Axiomatic and Operational ...
16:40 - 17:05
POPL Research Papers
Progress of Concurrent Objects with Partial Methods
17:05 - 17:30

Thu 11 Jan

Displayed time zone: Tijuana, Baja California change

Room10:0015304511:0015304512:0015304513:0015304514:0015304515:0015304516:00153045
Bunker Hill
POPL Research Papers
Sound, Complete, and Tractable Linearizability Monitoring for Concurren ...
10:30 - 10:55
POPL Research Papers
Reducing Liveness to Safety in First-Order Logic
10:55 - 11:20
POPL Research Papers
Alone Together: Compositional Reasoning and Inference for Weak Isolation
11:20 - 11:45
POPL Research Papers
Programming and Proving with Distributed Protocols
11:45 - 12:10
POPL Research Papers
A new proof rule for almost-sure termination
13:40 - 14:05
POPL Research Papers
Lexicographic Ranking Supermartingales: An Efficient Approach to Termin ...
14:05 - 14:30
POPL Research Papers
Algorithmic Analysis of Termination Problems for Quantum Programs
14:30 - 14:55
POPL Research Papers
Monadic refinements for relational cost analysis
14:55 - 15:20
POPL Research Papers
An Axiomatic Basis for Bidirectional Programming
15:50 - 16:15
POPL Research Papers
Simplicitly: Foundations and Applications of Implicit Function Types
16:15 - 16:40

Fri 12 Jan

Displayed time zone: Tijuana, Baja California change

Room10:0015304511:0015304512:0015304513:0015304514:0015304515:0015304516:0015304517:00153045
Bunker Hill
POPL Research Papers
Generating Good Generators for Inductive Relations
10:30 - 10:55
POPL Research Papers
Why is Random Testing Effective for Partition Tolerance Bugs?
10:55 - 11:20
POPL Research Papers
On Automatically Proving the Correctness of math.h Implementations
11:20 - 11:45
POPL Research Papers
Online Detection of Effectively Callback Free Objects with Applications ...
11:45 - 12:10
POPL Research Papers
SRC Awards
13:30 - 13:40
Refinement Reflection: Complete Verification with SMT
13:30 - 13:52
POPL Research Papers
Non-Linear Reasoning For Invariant Synthesis
14:05 - 14:30
POPL Research Papers
A Practical Construction for Decomposing Numerical Abstract Domains
14:30 - 14:55
POPL Research Papers
Verifying Equivalence of Database-Driven Applications
14:55 - 15:20
POPL Research Papers
Strategy Synthesis for Linear Arithmetic Games
15:50 - 16:15
POPL Research Papers
Bonsai: Synthesis-Based Reasoning for Type Systems
16:15 - 16:40
POPL Research Papers
Program Synthesis using Abstraction Refinement
16:40 - 17:05