Write a Blog >>
POPL 2016
Wed 20 - Sat 23 January 2016 St. Petersburg, Florida, United States
POPL 2016 (series) / Hilton St. Petersburg Bayfront /

Room information: Grand Bay North

VenueHilton St. Petersburg Bayfront
Room nameGrand Bay North
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 20 Jan

Displayed time zone: Guadalajara, Mexico City, Monterrey change

10:30 - 12:10
Track 1: Algorithmic VerificationResearch Papers at Grand Bay North
Chair(s): Arie Gurfinkel Carnegie Mellon University
10:30
25m
Talk
Temporal Verification of Higher-order Functional Programs
Research Papers
Akihiro Murase , Tachio Terauchi JAIST, Naoki Kobayashi University of Tokyo, Ryosuke Sato University of Tokyo, Hiroshi Unno University of Tsukuba
10:55
25m
Talk
Scaling Network Verification using Symmetry and Surgery
Research Papers
Gordon Plotkin , Nikolaj Bjørner Microsoft Research, Nuno P. Lopes Microsoft Research, Andrey Rybalchenko Microsoft Research, George Varghese Microsoft Research
Pre-print
11:20
25m
Talk
Model Checking for Symbolic-Heap Separation Logic with Inductive Predicates
Research Papers
James Brotherston , Nikos Gorogiannis , Max Kanovich , Reuben Rowe
11:45
25m
Talk
Reducing Crash Recoverability to Reachability
Research Papers
Eric Koskinen Yale University, Junfeng Yang Columbia University
14:20 - 16:00
Track 1: Decision ProceduresResearch Papers at Grand Bay North
Chair(s): Loris D'Antoni University of Pennsylvania
14:20
25m
Talk
Query-Guided Maximum Satisfiability
Research Papers
Xin Zhang Georgia Tech, Ravi Mangal Georgia Institute of Technology, Aditya Nori Microsoft Research, UK, Mayur Naik Georgia Tech
File Attached
14:45
25m
Talk
String Solving with Word Equations and Transducers: Decidability and Applications to Detecting Mutation XSS
Research Papers
Anthony Widjaja Lin Yale-NUS College, Singapore, Pablo Barcelo University of Chile, Chile
Media Attached
15:10
25m
Talk
Symbolic Computation of Differential Equivalences
Research Papers
Luca Cardelli Microsoft Research and University of Oxford, Mirco Tribastone IMT Institute for Advanced Studies Lucca, Italy, Max Tschaikowski IMT Institute for Advanced Studies Lucca, Italy, Andrea Vandin IMT Institute for Advanced Studies Lucca, Italy
Media Attached
15:35
25m
Talk
Unboundedness and Downward Closures of Higher-Order Pushdown Automata
Research Papers
Matthew Hague Royal Holloway University of London, UK, Jonathan Kochems Department of Computer Science, University of Oxford, C.-H. Luke Ong University of Oxford, UK
Media Attached
16:30 - 17:45
Track 1: Language DesignResearch Papers at Grand Bay North
Chair(s): David Walker Princeton University
16:30
25m
Talk
Dependent Types and Multi-Monadic Effects in F*
Research Papers
Nikhil Swamy Microsoft Research, Cătălin Hriţcu INRIA Paris, Chantal Keller MSR-INRIA, Aseem Rastogi University of Maryland, College Park, Antoine Delignat-Lavaud INRIA, Simon Forest ENS, Karthikeyan Bhargavan INRIA, Cédric Fournet Microsoft Research, Pierre-Yves Strub IMDEA Software Institute, Markulf Kohlweiss Microsoft Research, Jean-Karim Zinzindohoué INRIA, Santiago Zanella-Béguelin Microsoft Research
Pre-print Media Attached
16:55
25m
Talk
Fabular: Regression Formulas as Probabilistic Programming
Research Papers
Johannes Borgström Uppsala University, Andrew D. Gordon Microsoft Research and University of Edinburgh, Long Ouyang Stanford University, Claudio Russo Microsoft Research, Adam Ścibior University of Cambridge, Marcin Szymczak University of Edinburgh
Media Attached
17:20
25m
Talk
Kleenex: Compiling Nondeterministic Transducers to Deterministic Streaming Transducers
Research Papers
Bjørn Bugge Grathwohl DIKU, University of Copenhagen, Fritz Henglein DIKU, Denmark, Ulrik Terp Rasmussen DIKU, University of Copenhagen, Kristoffer Aalund Søholm Jobindex, Denmark, Sebastian Paaske Tørholm Jobindex, Denmark
Media Attached

Thu 21 Jan

Displayed time zone: Guadalajara, Mexico City, Monterrey change

10:30 - 12:10
Track 1: Foundations of distributed systemsResearch Papers at Grand Bay North
Chair(s): Mooly Sagiv Tel Aviv University
10:30
25m
Talk
Certified Causally Consistent Distributed Key-Value Stores
Research Papers
Mohsen Lesani MIT, Christian J. Bell MIT CSAIL, Adam Chlipala MIT
Media Attached
10:55
25m
Talk
'Cause I'm Strong Enough: Reasoning about Consistency Choices in Distributed Systems
Research Papers
Alexey Gotsman IMDEA, Hongseok Yang University of Oxford, UK, Carla Ferreira Universidade Nova Lisboa, Mahsa Najafzadeh UPMC & INRIA, Marc Shapiro Inria & LIP6
Media Attached
11:20
25m
Talk
A Program Logic for Concurrent Objects under Fair Scheduling
Research Papers
Hongjin Liang University of Science and Technology of China, Xinyu Feng University of Science and Technology of China
Media Attached
11:45
25m
Talk
PSync: a partially synchronous language for fault-tolerant distributed algorithms
Research Papers
Cezara Drăgoi INRIA, ENS, CNRS, Thomas A. Henzinger IST Austria, Damien Zufferey MIT
Link to publication DOI Pre-print Media Attached File Attached
14:20 - 16:00
Track 1: Learning and verificationResearch Papers at Grand Bay North
Chair(s): David Monniaux CNRS, VERIMAG
14:20
25m
Talk
Combining Static Analysis with Probabilistic Models to Enable Market-Scale Analysis
Research Papers
Damien Octeau University of Wisconsin and Pennsylvania State University, Somesh Jha University of Wisconsin, Madison, Matthew Dering Pennsylvania State University, Patrick McDaniel Pennsylvania State University, Alexandre Bartel Technical University Darmstadt, Hongyu Li Rice University, Jacques Klein University of Luxembourg, Yves Le Traon University of Luxembourg
Media Attached
14:45
25m
Talk
Abstraction Refinement Guided by a Learnt Probabilistic Model
Research Papers
Radu Grigore University of Oxford, Hongseok Yang University of Oxford, UK
Media Attached
15:10
25m
Talk
Learning Invariants using Decision Trees and Implication Counterexamples
Research Papers
Pranav Garg University of Illinois at Urbana-Champaign, Daniel Neider University of Illinois at Urbana-Champaign, P. Madhusudan University of Illinois at Urbana-Champaign, Dan Roth University of Illinois at Urbana-Champaign
Media Attached
15:35
25m
Talk
Symbolic Abstract Data Type Inference
Research Papers
Michael Emmi IMDEA Software Institute, Constantin Enea LIAFA, Université Paris Diderot
Media Attached
16:30 - 17:45
Track 1: OptimizationResearch Papers at Grand Bay North
Chair(s): Mayur Naik Georgia Tech
16:30
25m
Talk
SMO: An Integrated Approach to Intra-Array and Inter-Array Storage Optimization
Research Papers
Somashekaracharya G Bhaskaracharya Indian Institute of Science and National Instruments, Uday Bondhugula Indian Institute of Science, Albert Cohen INRIA
Media Attached File Attached
16:55
25m
Talk
PolyCheck: Dynamic Verification of Iteration Space Transformations on Affine Programs
Research Papers
Wenlei Bao , Sriram Krishnamoorthy Pacific Northwest National Laboratories, Louis-Noël Pouchet Ohio State University, Fabrice Rastello INRIA, France, P. Sadayappan Ohio State University
Media Attached
17:20
25m
Talk
Printing Floating-Point Numbers: A Faster, Always Correct Method
Research Papers
Marc Andrysco University of California, San Diego, Ranjit Jhala University of California, San Diego, Sorin Lerner University of California, San Diego
Media Attached
18:00 - 19:00
SIGPLAN Awards; Program Chair's Report; and SIGPLAN Business MeetingResearch Papers at Grand Bay North
Chair(s): Michael Hicks University of Maryland at College Park, USA

Fri 22 Jan

Displayed time zone: Guadalajara, Mexico City, Monterrey change

10:30 - 12:10
Track 1: Program Design and AnalysisResearch Papers at Grand Bay North
Chair(s): Manu Sridharan Samsung Research America
10:30
25m
Talk
Newtonian Program Analysis via Tensor Product
Research Papers
Thomas Reps University of Wisconsin - Madison and Grammatech Inc., Emma Turetsky CS Dept., Univ. of Wisconsin-Madison, Prathmesh Prabhu Google
Media Attached
10:55
25m
Talk
Casper: An Efficient Approach to Call Trace Collection
Research Papers
Rongxin Wu Department of Computer Science and Engineering, The Hong Kong University of Science and Technology, Xiao Xiao The Hong Kong University of Science and Technology, Shing-Chi Cheung Department of Computer Science and Engineering, The Hong Kong University of Science and Technology, Hongyu Zhang Microsoft Research, Charles Zhang HKUST
Media Attached
11:20
25m
Talk
Pushdown Control-flow Analysis for Free
Research Papers
Thomas Gilray University of Utah, Steven Lyde , Michael D. Adams University of Utah, Matthew Might University of Utah, USA, David Van Horn University of Maryland, College Park
Pre-print Media Attached
11:45
25m
Talk
Binding as Sets of Scopes
Research Papers
Matthew Flatt University of Utah
Pre-print Media Attached
14:20 - 16:00
Track 1: SynthesisResearch Papers at Grand Bay North
Chair(s): Roberto Giacobazzi University of Verona, Italy
14:20
25m
Talk
Learning Programs from Noisy Data
Research Papers
Veselin Raychev ETH Zurich, Pavol Bielik ETH Zurich, Switzerland, Martin Vechev ETH Zurich, Andreas Krause ETH Zurich
Link to publication DOI Pre-print Media Attached File Attached
14:45
25m
Talk
Optimizing Synthesis with Metasketches
Research Papers
James Bornholt University of Washington, Emina Torlak University of Washington, Dan Grossman University of Washington, USA, Luis Ceze University of Washington, USA
Pre-print Media Attached
15:10
25m
Talk
Maximal Specification Synthesis
Research Papers
Aws Albarghouthi University of Wisconsin–Madison, Işıl Dillig University of Texas, Austin, Arie Gurfinkel Carnegie Mellon University
Pre-print Media Attached
15:35
25m
Talk
Example-Directed Synthesis: A Type-Theoretic Interpretation
Research Papers
Jonathan Frankle Princeton University, Peter-Michael Osera Grinnell College, David Walker Princeton University, Steve Zdancewic University of Pennsylvania
Pre-print Media Attached File Attached

Wed 20 Jan

Displayed time zone: Guadalajara, Mexico City, Monterrey change

Room10:003011:003012:003013:003014:003015:003016:003017:0030
Grand Bay North

Research Papers

Track 1: Algorithmic Verification

Research Papers

Track 1: Decision Procedures

Research Papers

Track 1: Language Design

Thu 21 Jan

Displayed time zone: Guadalajara, Mexico City, Monterrey change

Room10:003011:003012:003013:003014:003015:003016:003017:003018:0030
Grand Bay North

Research Papers

Track 1: Foundations of distributed systems

Research Papers

Track 1: Learning and verification

Research Papers

Track 1: Optimization

Research Papers

SIGPLAN Awards; Program Chair's Report; and SIGPLAN Business Meeting

Fri 22 Jan

Displayed time zone: Guadalajara, Mexico City, Monterrey change

Room10:003011:003012:003013:003014:003015:0030
Grand Bay North

Research Papers

Track 1: Program Design and Analysis

Research Papers

Track 1: Synthesis

Wed 20 Jan

Displayed time zone: Guadalajara, Mexico City, Monterrey change

Room10:0015304511:0015304512:0015304513:0015304514:0015304515:0015304516:0015304517:00153045
Grand Bay North
POPL Research Papers
Temporal Verification of Higher-order Functional Programs
10:30 - 10:55
POPL Research Papers
Scaling Network Verification using Symmetry and Surgery
10:55 - 11:20
POPL Research Papers
Model Checking for Symbolic-Heap Separation Logic with Inductive Predicates
11:20 - 11:45
POPL Research Papers
Reducing Crash Recoverability to Reachability
11:45 - 12:10
POPL Research Papers
Query-Guided Maximum Satisfiability
14:20 - 14:45
POPL Research Papers
String Solving with Word Equations and Transducers: Decidability and Ap ...
14:45 - 15:10
POPL Research Papers
Symbolic Computation of Differential Equivalences
15:10 - 15:35
POPL Research Papers
Unboundedness and Downward Closures of Higher-Order Pushdown Automata
15:35 - 16:00
POPL Research Papers
Dependent Types and Multi-Monadic Effects in F*
16:30 - 16:55
POPL Research Papers
Fabular: Regression Formulas as Probabilistic Programming
16:55 - 17:20
POPL Research Papers
Kleenex: Compiling Nondeterministic Transducers to Deterministic Stream ...
17:20 - 17:45

Thu 21 Jan

Displayed time zone: Guadalajara, Mexico City, Monterrey change

Room10:0015304511:0015304512:0015304513:0015304514:0015304515:0015304516:0015304517:00153045
Grand Bay North
POPL Research Papers
Certified Causally Consistent Distributed Key-Value Stores
10:30 - 10:55
POPL Research Papers
'Cause I'm Strong Enough: Reasoning about Consistency Choices in Distri ...
10:55 - 11:20
POPL Research Papers
A Program Logic for Concurrent Objects under Fair Scheduling
11:20 - 11:45
POPL Research Papers
PSync: a partially synchronous language for fault-tolerant distributed ...
11:45 - 12:10
POPL Research Papers
Combining Static Analysis with Probabilistic Models to Enable Market-Sc ...
14:20 - 14:45
POPL Research Papers
Abstraction Refinement Guided by a Learnt Probabilistic Model
14:45 - 15:10
POPL Research Papers
Learning Invariants using Decision Trees and Implication Counterexamples
15:10 - 15:35
POPL Research Papers
Symbolic Abstract Data Type Inference
15:35 - 16:00
POPL Research Papers
SMO: An Integrated Approach to Intra-Array and Inter-Array Storage Opti ...
16:30 - 16:55
POPL Research Papers
PolyCheck: Dynamic Verification of Iteration Space Transformations on A ...
16:55 - 17:20
POPL Research Papers
Printing Floating-Point Numbers: A Faster, Always Correct Method
17:20 - 17:45

Fri 22 Jan

Displayed time zone: Guadalajara, Mexico City, Monterrey change

Room10:0015304511:0015304512:0015304513:0015304514:0015304515:00153045
Grand Bay North
POPL Research Papers
Newtonian Program Analysis via Tensor Product
10:30 - 10:55
POPL Research Papers
Casper: An Efficient Approach to Call Trace Collection
10:55 - 11:20
POPL Research Papers
Pushdown Control-flow Analysis for Free
11:20 - 11:45
POPL Research Papers
Binding as Sets of Scopes
11:45 - 12:10
POPL Research Papers
Learning Programs from Noisy Data
14:20 - 14:45
POPL Research Papers
Optimizing Synthesis with Metasketches
14:45 - 15:10
POPL Research Papers
Maximal Specification Synthesis
15:10 - 15:35
POPL Research Papers
Example-Directed Synthesis: A Type-Theoretic Interpretation
15:35 - 16:00