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

Sun 7 Jan

Displayed time zone: Tijuana, Baja California change

09:00 - 10:00
Invited Talk by Ranjit JhalaVMCAI at Watercourt
Chair(s): Işıl Dillig UT Austin
09:00
60m
Talk
Reasoning about Functions
VMCAI
Ranjit Jhala University of California, San Diego
10:30 - 12:00
SynthesisVMCAI at Watercourt
Chair(s): K. Rustan M. Leino Amazon
10:30
30m
Talk
Abstraction-Based Interaction Model for Synthesis
VMCAI
Hila Peleg , Shachar Itzhaky Technion, Israel, Sharon Shoham Tel Aviv university
11:00
30m
Talk
A Framework for Computer-Aided Design of Educational Domain Models
VMCAI
Eric Butler University of Washington, Emina Torlak University of Washington, Zoran Popovic University of Washington
11:30
30m
Talk
Generating Tests by Example
VMCAI
Hila Peleg , Dan Rasin Technion – Israel Institute of Technology, Eran Yahav Technion
14:00 - 15:30
VerificationVMCAI at Watercourt
Chair(s): Jeffrey S. Foster University of Maryland, College Park
14:00
30m
Talk
Gradual Program Verification
VMCAI
Johannes Bader Microsoft, Jonathan Aldrich Carnegie Mellon University, Éric Tanter University of Chile
14:30
30m
Talk
A Logical System for Modular Information Flow Verification
VMCAI
Adi Prabawa National University of Singapore, Mahmudul Faisal Al Ameen National University of Singapore, Benedict Lee National University of Singapore, Wei-Ngan Chin National University of Singapore
15:00
30m
Talk
P5: Planner-less Proofs of Probabilistic Parameterized Protocols
VMCAI
Lenore Zuck , Kenneth L. McMillan Microsoft Research, Jordan Torf UIC
16:00 - 17:30
SecurityVMCAI at Watercourt
Chair(s): Francesco Ranzato University of Padova
16:00
30m
Talk
Code Obfuscation Against Abstract Model Checking Attacks
VMCAI
Roberto Bruni Dipartimento di Informatica, Universita' di Pisa, Roberto Giacobazzi University of Verona and IMDEA Software Institute, Roberta Gori Dipartimento di Informatica, Universita' di Pisa
16:30
30m
Talk
Scalable Approximation of Quantitative Information Flow in Programs
VMCAI
Fabrizio Biondi CentraleSupelec Rennes, Mike Enescu INRIA, Annelie Heuser CNRS/IRISA, Axel Legay , Kuldeep S. Meel National University of Singapore, Jean Quilbeuf INRIA
17:00
30m
Talk
Abstract Code Injection - A Semantic Approach Based on Abstract Non-Interference
VMCAI
Samuele Buro Università degli Studi di Verona, Isabella Mastroeni University of Verona, Italy

Mon 8 Jan

Displayed time zone: Tijuana, Baja California change

09:00 - 10:30
Equational reasoning for probabilistic programmingTutorialFest at Bradbury
09:00
90m
Talk
Equational reasoning for probabilistic programming.
TutorialFest
A: Chung-chieh Shan Indiana University, USA
Media Attached
09:00 - 10:30
Programming and Reasoning with Infinite Data in IsabelleTutorialFest at Hershey
09:00
90m
Talk
Programming and Reasoning with Infinite Data in Isabelle/HOL.
TutorialFest
A: Mathias Fleury MPI-INF, A: Andreas Lochbihler , A: Andrei Popescu Middlesex University, London
Media Attached
09:00 - 10:00
Invited Talk by René ThiemannCPP at Museum A
Chair(s): June Andronick Data61,CSIRO (formerly NICTA) and UNSW
09:00
60m
Talk
Efficient Certification of Complexity Proofs: Formalizing the Perron–Frobenius Theorem (Invited Talk Paper)
CPP
Jose Divasón , Sebastiaan Joosten , Ondřej Kunčar Technische Universität München, Germany, René Thiemann University of Innsbruck, Akihisa Yamada
DOI
09:00 - 10:30
Message-Passing Concurrency and Substructural LogicsTutorialFest at Museum B
09:00
90m
Talk
Message-Passing Concurrency and Substructural Logics
TutorialFest
Frank Pfenning Carnegie Mellon University, USA
Media Attached
09:00 - 10:00
Invited Talk by Kenneth L. McMillanVMCAI at Watercourt
Chair(s): Lenore Zuck
09:00
60m
Talk
How to Stay Decidable
VMCAI
Kenneth L. McMillan Microsoft Research
09:00 - 10:30
Code ObfuscationTutorialFest at Widney
09:00
90m
Talk
Code Obfuscation - A Hacking view on program analysis and understanding.
TutorialFest
A: Roberto Giacobazzi University of Verona and IMDEA Software Institute
Media Attached
10:30 - 12:00
Session 1-1PEPM at Crocker
Chair(s): Hsiang-Shang ‘Josh’ Ko National Institute of Informatics, Japan
10:30
60m
Talk
Developments in Property-Based Testing (Invited Talk)
PEPM
Jan Midtgaard University of Southern Denmark
DOI
11:30
30m
Talk
Selective CPS Transformation for Shift and Reset
PEPM
Kenichi Asai Ochanomizu University, Chihiro Uehara Ochanomizu University
DOI
10:30 - 12:00
Verifying Programs and SystemsCPP at Museum A
Chair(s): Natarajan Shankar SRI International, USA
10:30
30m
Talk
Total Haskell is Reasonable Coq
CPP
Antal Spector-Zabusky , Joachim Breitner University of Pennsylvania, Christine Rizkallah University of Pennsylvania, USA, Stephanie Weirich University of Pennsylvania, USA
DOI
11:00
30m
Talk
A Formal Proof in Coq of a Control Function for the Inverted Pendulum
CPP
Damien Rouhling University of Côte d'Azur, France
DOI
11:30
30m
Talk
Completeness and Decidability of Converse PDL in the Constructive Type Theory of Coq
CPP
Christian Doczkal CNRS, France, Joachim Bard Saarland University, Germany
DOI
10:30 - 12:00
Abstract InterpretationVMCAI at Watercourt
Chair(s): Patrick Cousot
10:30
30m
Talk
On Constructivity of Galois Connections
VMCAI
Francesco Ranzato University of Padova
11:00
30m
Talk
An Abstract Interpretation Framework for the Round-Off Error Analysis of Floating-Point Programs
VMCAI
Laura Titolo National Institute of Aerospace, USA, Marco A. Feliu National Institute of Aerospace, Mariano Moscato National Institute of Aerospace, Cesar Munoz NASA
11:30
30m
Talk
Modular Analysis of Executables using On-Demand Heyting Completion
VMCAI
Julian Kranz Technical University of Munich, Axel Simon Google
11:00 - 12:00
Equational reasoning for probabilistic programmingTutorialFest at Bradbury
11:00
60m
Talk
Equational reasoning for probabilistic programming.
TutorialFest
A: Chung-chieh Shan Indiana University, USA
Media Attached
11:00 - 12:00
Programming and Reasoning with Infinite Data in IsabelleTutorialFest at Hershey
11:00
60m
Talk
Programming and Reasoning with Infinite Data in Isabelle/HOL.
TutorialFest
A: Mathias Fleury MPI-INF, A: Andreas Lochbihler , A: Andrei Popescu Middlesex University, London
Media Attached
11:00 - 12:00
Message-Passing Concurrency and Substructural LogicsTutorialFest at Museum B
11:00
60m
Talk
Message-Passing Concurrency and Substructural Logics
TutorialFest
Frank Pfenning Carnegie Mellon University, USA
Media Attached
11:00 - 12:00
Code ObfuscationTutorialFest at Widney
11:00
60m
Talk
Code Obfuscation - A Hacking view on program analysis and understanding.
TutorialFest
A: Roberto Giacobazzi University of Verona and IMDEA Software Institute
Media Attached
13:30 - 15:30
Verified ApplicationsCPP at Museum A
Chair(s): K. Rustan M. Leino Amazon
13:30
30m
Talk
Mechanising and Verifying the WebAssembly Specification
CPP
Conrad Watt University of Cambridge, UK
DOI
14:00
30m
Talk
Towards Verifying Ethereum Smart Contract Bytecode in Isabelle/HOL
CPP
Sidney Amani UNSW, Australia, Myriam Bégel ENS Paris-Saclay, France, Maksym Bortin , Mark Staples CSIRO, Australia
DOI
14:30
30m
Talk
Mechanising Blockchain Consensus
CPP
George Pîrlea University College London, Ilya Sergey University College London
DOI Pre-print
15:00
30m
Talk
Formal Microeconomic Foundations and the First Welfare Theorem
CPP
Cezary Kaliszyk University of Innsbruck, Julian Parsert University of Innsbruck, Austria
13:30 - 14:30
Opening & Invited Talk IPADL at Rose
13:30
30m
Day opening
Opening
PADL

14:00
30m
Talk
INVITED TALK: ``Safe'' Languages Require Sequential Consistency
PADL
I: Todd Millstein University of California, Los Angeles
14:00 - 15:30
Computational Higher Type TheoryTutorialFest at Bradbury
14:00
90m
Talk
Computational Higher Type Theory
TutorialFest
A: Robert Harper Carnegie Mellon University, A: Carlo Angiuli Carnegie Mellon University
Media Attached
14:00 - 15:30
Session 1-2PEPM at Crocker
Chair(s): Kenichi Asai Ochanomizu University
14:00
30m
Talk
A Guess-and-Assume Approach to Loop Fusion for Program Verification
PEPM
Akifumi Imanishi Kyoto University, Kohei Suenaga Graduate School of Informatics, Kyoto University, Atsushi Igarashi Kyoto University, Japan
DOI
14:30
30m
Talk
Gradually Typed Symbolic Expressions
PEPM
David Broman KTH Royal Institute of Technology, Jeremy G. Siek Indiana University, USA
DOI
15:00
30m
Talk
On the Cost of Type-Tag Soundness
PEPM
Ben Greenman Northeastern University, Zeina Migeed University of California, Los Angeles
DOI
14:00 - 15:30
Introduction to Algebraic Program analysisTutorialFest at Hershey
14:00
90m
Talk
Introduction to Algebraic Program analysis.
TutorialFest
Zachary Kincaid Princeton University, Thomas Reps University of Wisconsin - Madison and GrammaTech, Inc.
Media Attached
14:00 - 15:30
Iris - A Higher-Order Concurrent Separation LogicTutorialFest at Museum B
14:00
90m
Talk
Iris - A Modular Foundation for Higher-Order Concurrent Separation Logic.
TutorialFest
Jacques-Henri Jourdan CNRS, LRI, Université Paris-Sud, A: Robbert Krebbers Delft University of Technology
Media Attached
14:00 - 15:30
PotpourriVMCAI at Watercourt
Chair(s): Wei-Ngan Chin National University of Singapore
14:00
30m
Talk
Revisiting MITL to Fix Decision Procedures
VMCAI
Nima Roohi University of Pennsylvania, Mahesh Viswanathan University of Illinois at Urbana-Champaign
14:30
30m
Talk
On abstraction and compositionality for weak-memory linearisability
VMCAI
Brijesh Dongol Brunel University London, Radha Jagadeesan DePaul University, James Riely DePaul University, Alasdair Armstrong Brunel University
15:00
30m
Talk
Automatic Verification of RMA Programs via Abstraction Extrapolation
VMCAI
Cedric Baumann ETH Zurich, Andrei Marian Dan ETH Zurich, Yuri Meshman IMDEA, Torsten Hoefler ETH Zurich, Martin Vechev ETH Zürich
14:00 - 15:30
One Weird Trick: Relational Interpreters for Program SynthesisTutorialFest at Widney
14:00
90m
Talk
One Weird Trick: Relational Interpreters for Program Synthesis.
TutorialFest
A: William E. Byrd University of Alabama at Birmingham, USA, Gregory Rosenblatt n.n., n.n.
Media Attached
14:30 - 15:30
Prolog and OptimizationsPADL at Rose
14:30
30m
Talk
Exploiting Term Hiding to Reduce Run-time Checking Overhead
PADL
A: Nataliia Stulova IMDEA Software Institute and T.U. of Madrid (UPM), A: José Morales IMDEA Software Institute, A: Manuel Hermenegildo IMDEA Software Institute and T.U. of Madrid (UPM)
15:00
30m
Talk
On k-colored Lambda Terms and their Skeletons
PADL
I: Paul Tarau University of North Texas
16:00 - 17:00
Computational Higher Type TheoryTutorialFest at Bradbury
16:00
60m
Talk
Computational Higher Type Theory
TutorialFest
A: Robert Harper Carnegie Mellon University, A: Carlo Angiuli Carnegie Mellon University
Media Attached
16:00 - 17:30
Session 1-3PEPM at Crocker
Chair(s): Frank Pfenning Carnegie Mellon University, USA
16:00
60m
Talk
The Simple Essence of Automatic Differentiation (Invited Talk)
PEPM
Conal Elliott Target, USA
Pre-print
16:00 - 17:00
Introduction to Algebraic Program analysisTutorialFest at Hershey
16:00
60m
Talk
Introduction to Algebraic Program analysis.
TutorialFest
Zachary Kincaid Princeton University, Thomas Reps University of Wisconsin - Madison and GrammaTech, Inc.
Media Attached
16:00 - 18:00
Proof Methods and LibrariesCPP at Museum A
Chair(s): René Thiemann University of Innsbruck
16:00
30m
Talk
Triangulating Context Lemmas
CPP
Craig McLaughlin The University of Edinburgh, James McKinna , Ian Stark The University of Edinburgh
DOI
16:30
30m
Talk
Adapting Proof Automation to Adapt Proofs
CPP
Talia Ringer University of Washington, Nathaniel Yazdani University of Washington, Seattle, John Leo Halfaya Research, Dan Grossman University of Washington
DOI
17:00
30m
Talk
A Monadic Framework for Relational Verification: Applied to Information Security, Program Equivalence, and Optimizations
CPP
Niklas Grimm Vienna University of Technology, Austria, Kenji Maillard Inria Paris and ENS Paris, Cédric Fournet Microsoft Research, Cătălin Hriţcu Inria Paris, Matteo Maffei Saarland University, Jonathan Protzenko Microsoft Research, n.n., Tahina Ramananandro Microsoft Research, n.n., Aseem Rastogi Microsoft Research, Nikhil Swamy Microsoft Research, Santiago Zanella-Béguelin Microsoft Research, n.n.
DOI
17:30
30m
Talk
Formal Proof of Polynomial-Time Complexity with Quasi-Interpretations
CPP
Hugo Férée University of Kent, UK, Samuel Hym University of Lille, France, Micaela Mayero , Jean-Yves Moyen University of Copenhagen, Denmark, David Nowak CNRS, France
DOI
16:00 - 17:00
Iris - A Higher-Order Concurrent Separation LogicTutorialFest at Museum B
16:00
60m
Talk
Iris - A Modular Foundation for Higher-Order Concurrent Separation Logic.
TutorialFest
Jacques-Henri Jourdan CNRS, LRI, Université Paris-Sud, A: Robbert Krebbers Delft University of Technology
Media Attached
16:00 - 17:30
Invited Tutorial by Mayur NaikVMCAI at Watercourt
Chair(s): Jens Palsberg University of California, Los Angeles (UCLA)
16:00
90m
Talk
Maximum Satisfiability in Program Analysis: Applications and Techniques
VMCAI
Mayur Naik University of Pennsylvania, Xujie Si University of Pennsylvania, Xin Zhang Massachusetts Institute of Technology, USA, Radu Grigore University of Kent
16:00 - 17:00
One Weird Trick: Relational Interpreters for Program SynthesisTutorialFest at Widney
16:00
60m
Talk
One Weird Trick: Relational Interpreters for Program Synthesis.
TutorialFest
A: William E. Byrd University of Alabama at Birmingham, USA, Gregory Rosenblatt n.n., n.n.
Media Attached
18:00 - 22:00
VMCAI BanquetVMCAI at Watercourt
18:00
4h
Dinner
Banquet
VMCAI

18:15 - 20:15
CPP ReceptionCPP at Museum A
18:15
2h
Social Event
CPP Reception
CPP

Tue 9 Jan

Displayed time zone: Tijuana, Baja California change

09:00 - 10:00
SESSION I (invited talk) PPS at Bradbury
Chair(s): Andrew D. Gordon Microsoft Research and University of Edinburgh
09:00
60m
Talk
Software is eating the world, but ML is going to eat software
PPS
09:00 - 10:00
Invited Talk by Brigitte PientkaCPP at Museum A
Chair(s): Amy Felty University of Ottawa
09:00
60m
Talk
POPLMark Reloaded: Mechanizing Logical Relations Proofs (Invited Talk)
CPP
Brigitte Pientka McGill University
DOI
09:00 - 10:00
Invited Talk by Azadeh FarzanVMCAI at Watercourt
Chair(s): Işıl Dillig UT Austin
09:00
60m
Talk
Rethinking Compositionality for Concurrent Program Proofs
VMCAI
Azadeh Farzan University of Toronto
10:00 - 10:30
POSTER SESSION (14 posters - not talks) PPS at Bradbury
10:00
2m
Talk
Probabilistic Programming for Robotics
PPS
Nils Napp SUNY at Buffalo, Marco Gaboardi University at Buffalo, SUNY
10:02
2m
Talk
Game Semantics for Probabilistic Programs
PPS
C.-H. Luke Ong University of Oxford, Matthijs Vákár University of Oxford
10:04
2m
Talk
Interactive Writing and Debugging of Bayesian Probabilistic Programs
PPS
Javier Burroni , Arjun Guha University of Massachusetts, Amherst, David Jensen University of Massachusetts Amherst
Pre-print
10:06
2m
Talk
Deep Amortized Inference for Probabilistic Programs using Adversarial Compilation
PPS
10:08
2m
Talk
Comparing the speed of probabilistic processes
PPS
Mathias Ruggaard Pedersen Aalborg University, Nathanaël Fijalkow Alan Turing Institute, Giorgio Bacci Aalborg University, Kim Larsen Aalborg University, Radu Mardare Aalborg University
10:10
2m
Talk
Using Reinforcement Learning for Probabilistic Program Inference
PPS
Avi Pfeffer Charles River Analytics
10:12
2m
Talk
TensorFlow Distributions
PPS
Link to publication Pre-print
10:15
2m
Talk
Constructive probabilistic semantics with non-spatial locales
PPS
Benjamin Sherman Massachusetts Institute of Technology, USA, Jared Tramontano Massachusetts Institute of Technology, Michael Carbin MIT
Pre-print
10:17
2m
Talk
Using probabilistic programs as proposals
PPS
Marco Cusumano-Towner MIT-CSAIL, Vikash Mansinghka Massachusetts Institute of Technology
10:19
2m
Talk
Probabilistic Program Equivalence for NetKAT
PPS
Steffen Smolka Cornell University, David Kahn Cornell University, Praveen Kumar Cornell University, Nate Foster Cornell University, Dexter Kozen , Alexandra Silva University College London
Link to publication File Attached
10:21
2m
Talk
Reasoning about Divergences via Span-liftings
PPS
Tetsuya Sato University at Buffalo, SUNY, USA
10:23
2m
Talk
Probabilistic Models for Assured Position, Navigation and Timing
PPS
Andres Molina-Markham The MITRE Corporation
10:25
2m
Talk
The Support Method of Computing Expectations
PPS
Avi Pfeffer Charles River Analytics
10:27
2m
Talk
Combining static and dynamic optimizations using closed-form solutions
PPS
Daniel Lundén KTH Royal Institute of Technology, David Broman KTH Royal Institute of Technology, Lawrence M. Murray Uppsala University
10:30 - 12:00
SESSION II (3 talks) PPS at Bradbury
Chair(s): Erik Meijer
10:30
30m
Talk
The semantic structure of quasi-Borel spaces: algebra, logic, and recursion
PPS
Chris Heunen University of Edinburgh, Ohad Kammar University of Oxford, Sean Moss University of Oxford, Adam Ścibior University of Cambridge and MPI Tuebingen, Sam Staton University of Oxford, Matthijs Vákár University of Oxford, Hongseok Yang University of Oxford
11:00
30m
Talk
Stable, measurable functions and probabilistic programs
PPS
Michele Pagani University Paris Diderot, Thomas Ehrhard CNRS and University Paris Diderot, Christine Tasson University Paris Diderot
11:30
30m
Talk
Formal Methods For Probabilistic Programming
PPS
Daniel Selsam Stanford University
10:30 - 12:00
Session 2-1PEPM at Crocker
Chair(s): Fritz Henglein DIKU, Denmark
10:30
60m
Talk
Challenges in the Design and Compilation of Programming Languages for Exascale Machines (Invited Talk)
PEPM
Alex Aiken Stanford University
11:30
30m
Talk
Checking Cryptographic API Usage with Composable Annotations (Short Paper)
PEPM
Duncan Mitchell Royal Holloway, University of London, L. Thomas van Binsbergen Royal Holloway University of London, Blake Loring , Johannes Kinder Royal Holloway, University of London
DOI
10:30 - 12:00
Morning Session 2NetPL at Hershey
10:30
30m
Talk
Very Large Scale Network Verification
NetPL
Andrey Rybalchenko Microsoft Research
11:00
60m
Other
Working Groups
NetPL

10:30 - 12:00
Trusted Verification Frameworks and SystemsCPP at Museum A
Chair(s): Zhong Shao Yale University
10:30
30m
Talk
A Verified SAT Solver with Watched Literals Using Imperative HOL
CPP
Mathias Fleury MPI-INF, Jasmin Blanchette Vrije Universiteit Amsterdam, Peter Lammich Technische Universität München
DOI
11:00
30m
Talk
Œuf: Minimizing the Coq Extraction TCB
CPP
Eric Mullen University of Washington, Stuart Pernsteiner University of Washington, USA, James R. Wilcox University of Washington, Zachary Tatlock University of Washington, Seattle, Dan Grossman University of Washington
DOI
11:30
30m
Talk
Proofs in Conflict-Driven Theory Combination
CPP
Maria Paola Bonacina University of Verona, Italy, Stéphane Graham-Lengrand CNRS, France, Natarajan Shankar SRI International, USA
DOI
10:30 - 12:00
Panel IPLMW at Museum B
10:30
90m
Talk
Panel I: Technical Trends in Programming Languages Research
PLMW
Aws Albarghouthi University of Wisconsin-Madison, Constantin Enea Université Paris Diderot, David Walker Princeton University, Andrew Myers Cornell University
10:30 - 12:00
Functional ProgrammingPADL at Rose
10:30
30m
Talk
Hygienic Source-Code Generation Using Functors
PADL
A: Karl Crary Carnegie Mellon University
11:00
30m
Talk
Snaarkl: Somewhat Practical, Pretty Much Declarative Verifiable Computing in Haskell
PADL
A: Gordon Stewart Ohio University, A: Samuel Merten , A: Logan Leland
11:30
30m
Talk
Rewriting High-Level Spreadsheet Structures into Higher-Order Functional Programs
PADL
A: Florian Biermann IT University of Copenhagen, Wensheng Dou Institute of Software, Chinese Academy of Sciences, China, A: Peter Sestoft IT University of Copenhagen
10:30 - 12:00
Verifying Protocols and SystemsVMCAI at Watercourt
Chair(s): James Riely DePaul University
10:30
30m
Talk
Analyzing Guarded Protocols: Better Cutoffs, More Systems, More Expressivity
VMCAI
Swen Jacobs , Mouhammad Sakr Saarland University
11:00
30m
Talk
Automatic Verification of Intermittent Systems
VMCAI
11:30
30m
Talk
Co-Design and Verification of an Available File System
VMCAI
Mahsa Najafzadeh Purdue University, Marc Shapiro LIP6, Patrick Eugster Purdue University
13:30 - 15:30
Afternoon Session 1NetPL at Hershey
14:00
30m
Other
Working Groups Debrief
NetPL

14:30
30m
Talk
Safety Verification of Stateful Networks
NetPL
Sharon Shoham Tel Aviv university
15:00
30m
Talk
Understand and verify your network using Header Space Analysis
NetPL
Peyman Kazemian Forward Networks
13:30 - 15:30
Type Theory, Set Theory, and Formalized MathematicsCPP at Museum A
Chair(s): Thorsten Altenkirch University of Nottingham
13:30
30m
Talk
Finite Sets in Homotopy Type Theory
CPP
Dan Frumin Radboud University, Herman Geuvers Radboud University Nijmegen, Netherlands, Léon Gondelman LRI, Université Paris-Sud, Niels van der Weide Radboud University Nijmegen, Netherlands
DOI
14:00
30m
Talk
Generic Derivation of Induction for Impredicative Encodings in Cedille
CPP
Denis Firsov University of Iowa, USA, Aaron Stump University of Iowa, USA
DOI
14:30
30m
Talk
Large Model Constructions for Second-Order ZF in Dependent Type Theory
CPP
Dominik Kirst Saarland University, Gert Smolka Saarland University
DOI
15:00
30m
Talk
A Constructive Formalisation of Semi-algebraic Sets and Functions
CPP
14:00 - 15:30
SESSION III (invited tutorial + 1 talk) PPS at Bradbury
Chair(s): Cameron Freer Remine and Borelian
14:00
60m
Talk
Deep Probabilistic Programming: TensorFlow Distributions and Edward
PPS
15:00
30m
Talk
More support for symbolic disintegration
PPS
Praveen Narayanan Indiana University, USA, Chung-chieh Shan Indiana University, USA
14:00 - 15:30
Session 2-2PEPM at Crocker
Chair(s): Kohei Suenaga Graduate School of Informatics, Kyoto University
14:00
30m
Talk
Partially Static Data as Free Extension of Algebras (Short Paper)
PEPM
Jeremy Yallop University of Cambridge, UK, Tamara von Glehn University of Cambridge, Ohad Kammar University of Oxford
Pre-print
14:30
30m
Talk
Program Generation for ML Modules (Short Paper)
PEPM
Takahisa Watanabe University of Tsukuba, Japan, Yukiyoshi Kameyama University of Tsukuba, Japan
DOI
15:00
30m
Talk
Recursive Programs in Normal Form (Short Paper)
PEPM
Barry Jay University of Technology Sydney
DOI
14:00 - 15:30
Types and AnalysisVMCAI at Watercourt
Chair(s): Tachio Terauchi Waseda University
14:00
30m
Talk
From Shapes to Amortized Complexity
VMCAI
Tomas Fiedor VUT Brno, Lukáš Holík Brno University of Technology, Adam Rogalewicz Brno University of Technology , Moritz Sinn St. Polten University of Applied Sciences, Tomáš Vojnar Brno University of Technology, Florian Zuleger TU Vienna
14:30
30m
Talk
Invariant Generation for Multi-Path Loops with Polynomial Assignments
VMCAI
Andreas Humenberger Vienna University of Technology, Maximilian Jaroschek Vienna University of Technology, Laura Kovacs Chalmers University of Technology
15:00
30m
Talk
Refinement Types for Ruby
VMCAI
Milod Kazerounian , Niki Vazou University of Maryland, Austin Bourgerie University of Maryland, Jeffrey S. Foster University of Maryland, College Park, Emina Torlak University of Washington
16:00 - 18:00
SESSION IV (4 talks) PPS at Bradbury
Chair(s): Rif A. Saurous Google
16:00
30m
Talk
Auxiliary variables in Probabilistic Programs
PPS
16:30
30m
Talk
Probabilistic Program Inference With Abstractions
PPS
Steven Holtzen University of California, Los Angeles, Guy Van den Broeck University of California, Los Angeles, Todd Millstein University of California, Los Angeles
Pre-print
17:00
30m
Talk
SlicStan: Improving Probabilistic Programming using Information Flow Analysis
PPS
Maria I. Gorinova The University of Edinburgh, Andrew D. Gordon Microsoft Research and University of Edinburgh, Charles Sutton University of Edinburgh
Pre-print
17:30
30m
Talk
Contextual Equivalence for a Probabilistic Language with Continuous Random Variables and Recursion
PPS
Mitchell Wand Northeastern University, USA, Theophilos Giannakopoulos BAE Systems, Inc., Andrew Cobb Northeastern University, Ryan Culpepper Northeastern University
16:00 - 17:30
Session 2-3PEPM at Crocker
Chair(s): Barry Jay University of Technology Sydney
16:00
10m
Talk
Towards Language-independent Code Synthesis (Poster/Demo Talk)
PEPM
Jan Bessai Technical University Dortmund, Boris Düdder University of Copenhagen, George Heineman Worcester Polytechnic Institute, Jakob Rehof Technical University Dortmund
File Attached
16:10
10m
Talk
Dataflow Metaprogramming (Poster/Demo Talk)
PEPM
Dominic Duggan , Jianhua Yao Stevens Institute of Technology
16:20
10m
Talk
An Approach to Generating Text-Based IDEs with Syntax Completion (Poster/Demo Talk)
PEPM
Isao Sasano Shibaura Institute of Technology
16:30
10m
Talk
Modular Macros (Poster/Demo Talk)
PEPM
Olivier Nicole , Leo White Jane Street, Jeremy Yallop University of Cambridge, UK
File Attached
16:40
10m
Talk
Equations: From Clauses to Splittings to Functions (Poster/Demo Talk)
PEPM
File Attached
16:50
40m
Other
Posters/Demos
PEPM

16:00 - 18:00
Afternoon Session 2NetPL at Hershey
16:00
30m
Talk
P4: A Language for Data Plane Programming
NetPL
Calin Cascaval Barefoot Networks
16:30
30m
Talk
A Vision for Network Design Automation
NetPL
17:00
30m
Other
Panel
NetPL
Nate Foster Cornell University, David Walker Princeton University, Barath Raghavan ICSI, Jonathan Smith DARPA
17:30
30m
Day closing
Wrap Up
NetPL
Marco Canini KAUST, Nate Foster Cornell University, Todd Millstein University of California, Los Angeles
16:00 - 18:00
Formalizing Meta-TheoryCPP at Museum A
Chair(s): Brigitte Pientka McGill University
16:00
30m
Talk
HOpi in Coq
CPP
Sergueï Lenglet University of Lorraine, France, Alan Schmitt Inria
DOI
16:30
30m
Talk
A Coq Formalization of Normalization by Evaluation for Martin-Löf Type Theory
CPP
Paweł Wieczorek University of Wrocław, Dariusz Biernacki University of Wrocław
DOI
17:00
30m
Talk
A Two-Level Logic Perspective on (Simultaneous) Substitutions
CPP
Kaustuv Chaudhuri Inria, France
DOI
17:30
30m
Talk
Binder Aware Recursion over Well-Scoped de Bruijn Syntax
CPP
Jonas Kaiser , Steven Schäfer , Kathrin Stark Saarland University, Germany
DOI
16:00 - 18:00
Panel IIPLMW at Museum B
16:00
30m
Talk
Work-Life Balance?
PLMW
Andrew Myers Cornell University
File Attached
16:30
90m
Talk
Panel II: Life in Grad School (and Beyond)
PLMW
Azadeh Farzan University of Toronto, Zachary Tatlock University of Washington, Seattle, Thomas Ball Microsoft Research, Jennifer Paykin University of Pennsylvania
16:00 - 18:00
Best Papers PADL at Rose
16:00
30m
Talk
Probabilistic Functional Logic Programming
PADL
A: Sandra Dylus University of Kiel, Germany, A: Jan Christiansen Flensburg University of Applied Sciences, Germany, A: Finn Teegen University of Kiel, Germany
16:30
30m
Talk
Optimizing Answer Set Computation via Heuristic-Based Decomposition
PADL
A: Francesco Calimeri University of Calabria, A: Davide Fuscà , A: Simona Perri , A: Jessica Zangari
17:00
30m
Day closing
Closing
PADL

16:00 - 17:30
Model CheckingVMCAI at Watercourt
Chair(s): Kenneth L. McMillan Microsoft Research
16:00
30m
Talk
Learning to Complement Büchi Automata
VMCAI
Yong Li Institute of Software, Chinese Academy of Sciences, Andrea Turrini State Key Laboratory of Computer Science, Institute of Software, Chinese Academy of Sciences, Lijun Zhang Institute of Software, Chinese Academy of Sciences, Sven Schewe University of Liverpool
16:30
30m
Talk
Selfless Interpolation for Infinite-State Model Checking
VMCAI
Tanja Schindler University of Freiburg, Dejan Jovanović SRI International
17:00
30m
Talk
Parameterized Model Checking of Synchronous Distributed Algorithms by Abstraction
VMCAI
Benjamin Aminof Vienna University of Technology, Sasha Rubin University of Naples Federico II, Ilina Stoilkovska Vienna University of Technology , Josef Widder TU Wien, Florian Zuleger TU Vienna

Wed 10 Jan

Displayed time zone: Tijuana, Baja California change

08:30 - 10:00
Awards & Keynote-IResearch Papers at Bunker Hill / Watercourt
Chair(s): Ranjit Jhala University of California, San Diego
08:30
5m
Day opening
Welcome to POPL 2018
Research Papers
G: Ranjit Jhala University of California, San Diego, P: Andrew Myers Cornell University
08:35
10m
Awards
SIGPLAN Awards
Research Papers
Satnam Singh X, the moonshot factory
08:45
60m
Talk
Milner Award Lecture: The Type Soundness Theorem That You Really Want to Prove (and Now You Can)
Research Papers
Derek Dreyer MPI-SWS
09:45
20m
Talk
Lightning Overview - Day 1
Research Papers

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
10:30 - 12:10
Types and EffectsResearch Papers at Watercourt
Chair(s): Neel Krishnaswami Computer Laboratory, University of Cambridge
10:30
25m
Talk
Linear Haskell: practical linearity in a higher-order polymorphic language
Research Papers
Jean-Philippe Bernardy University of Gothenburg, Mathieu Boespflug Tweag I/O, Ryan R. Newton Indiana University, Simon Peyton Jones Microsoft Research, Arnaud Spiwack Tweag I/O
Pre-print File Attached
10:55
25m
Talk
Polyadic Approximations, Fibrations and Intersection Types
Research Papers
11:20
25m
Talk
Handling fibred algebraic effects
Research Papers
Danel Ahman Inria Paris
11:45
25m
Talk
Handle with Care: Relational Interpretation of Algebraic Effects and Handlers
Research Papers
Dariusz Biernacki University of Wrocław, Maciej Piróg University of Wrocław, Piotr Polesiuk University of Wrocław, Filip Sieczkowski University of Wrocław
12:10 - 13:40
Wednesday LunchResearch Papers at Lunch Room
12:10
90m
Lunch
Wednesday Lunch
Research Papers

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
13:40 - 15:20
Interpretation and EvaluationResearch Papers at Watercourt
Chair(s): Atsushi Igarashi Kyoto University, Japan
13:40
25m
Talk
Unifying Analytic and Statically-Typed Quasiquotes
Research Papers
Lionel Parreaux EPFL, Antoine Voizard University of Pennsylvannia, Amir Shaikhha EPFL, Christoph E. Koch EPFL
Pre-print
14:05
25m
Talk
Jones-Optimal Partial Evaluation by Specialization-Safe Normalization
Research Papers
Matt Brown UCLA, Jens Palsberg University of California, Los Angeles (UCLA)
14:30
25m
Talk
Migrating Gradual Types
Research Papers
John Peter Campora ULL Lafayette, Sheng Chen University of Louisiana at Lafayette, Martin Erwig Oregon State University, Eric Walkingshaw Oregon State University
14:55
25m
Talk
Intrinsically-Typed Definitional Interpreters for Imperative Languages
Research Papers
Casper Bach Poulsen Delft University of Technology, Arjen Rouvoet Delft University of Technology, Andrew Tolmach Portland State University, Robbert Krebbers Delft University of Technology, Eelco Visser Delft University of Technology
DOI Pre-print
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
15:50 - 17:30
TypesResearch Papers at Watercourt
Chair(s): Thorsten Altenkirch University of Nottingham
15:50
25m
Talk
A Principled approach to Ornamentation in ML
Research Papers
16:15
25m
Talk
Type-Preserving CPS Translation of Σ and Π Types is Not Not Possible
Research Papers
William J. Bowman Northeastern University, USA, Youyou Cong Ochanomizu University, Japan, Nick Rioux Northeastern University, USA, Amal Ahmed Northeastern University, USA
Link to publication DOI Pre-print
16:40
25m
Talk
Safety and Conservativity of Definitions in HOL and Isabelle/HOL
Research Papers
Ondřej Kunčar Technische Universität München, Germany, Andrei Popescu Middlesex University, London
17:05
25m
Talk
Univalent Higher Categories via Complete Semi-Segal Types
Research Papers
Paolo Capriotti University of Nottingham, Nicolai Kraus University of Nottingham
19:00 - 22:00
POPL BanquetResearch Papers at MOCA
19:00
3h
Dinner
POPL Banquet
Research Papers

Thu 11 Jan

Displayed time zone: Tijuana, Baja California change

08:30 - 10:00
Keynote-IIResearch Papers at Bunker Hill / Watercourt
Chair(s): Andrew Myers Cornell University
08:30
60m
Talk
Some Principles of Differential Programming Languages
Research Papers
Gordon Plotkin University of Edinburgh, UK
09:30
30m
Talk
Lightning Overview - Day 2
Research Papers

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
10:30 - 12:10
Program Analysis IResearch Papers at Watercourt
Chair(s): Tachio Terauchi Waseda University
10:30
25m
Talk
Inference of Static Semantics for Incomplete C Programs
Research Papers
Pre-print
10:55
25m
Talk
Optimal Dyck Reachability for Data-dependence and Alias Analysis
Research Papers
Krishnendu Chatterjee IST Austria, Andreas Pavlogiannis IST Austria, Bhavya Choudhary IIT Bombay
11:20
25m
Talk
Data-centric Dynamic Partial Order Reduction
Research Papers
Marek Chalupa Masaryk University, Krishnendu Chatterjee IST Austria, Andreas Pavlogiannis IST Austria, Kapil Vaidya IIT Bombay, Nishant Sinha IBM Research
11:45
25m
Talk
Analytical Modeling of Cache Behavior for Affine Programs
Research Papers
Wenlei Bao Ohio State University, Sriram Krishnamoorthy Pacific Northwest National Laboratories, Louis-Noël Pouchet Colorado State University, P. Sadayappan Ohio State University
12:10 - 13:40
Thursday LunchResearch Papers at Lunch Room
12:10
90m
Lunch
Thursday Lunch
Research Papers

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
13:40 - 15:20
Outside the boxResearch Papers at Watercourt
Chair(s): Lars Birkedal Aarhus University
13:40
25m
Talk
Go with the Flow: Compositional Abstractions for Concurrent Data Structures
Research Papers
Siddharth Krishna New York University, Dennis Shasha New York University, Thomas Wies New York University
14:05
25m
Talk
Parametricity versus the Universal Type
Research Papers
Dominique Devriese KU Leuven, Marco Patrignani Saarland University, CISPA, Frank Piessens KU Leuven
14:30
25m
Talk
Linearity in Higher-Order Recursion Schemes
Research Papers
Pierre Clairambault CNRS & ENS Lyon, Charles Grellois INRIA Sophia Antipolis & Aix-Marseille Université, Andrzej Murawski University of Oxford
14:55
25m
Talk
Symbolic Types for Lenient Symbolic Execution
Research Papers
Stephen Chang Northeastern University, Alex Knauth Northeastern University, Emina Torlak University of Washington
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
15:50 - 16:40
Dependent TypesResearch Papers at Watercourt
Chair(s): Karl Crary Carnegie Mellon University
15:50
25m
Talk
Up-to Techniques Using Sized Types
Research Papers
Nils Anders Danielsson University of Gothenburg, Chalmers University of Technology
16:15
25m
Talk
Decidability of Conversion for Type Theory in Type Theory
Research Papers
Andreas Abel Gothenburg University, Joakim Öhman IMDEA Software Institute, Andrea Vezzosi Chalmers University of Technology
17:00 - 18:00
Business MeetingResearch Papers at Bunker Hill / Watercourt
Chair(s): Ranjit Jhala University of California, San Diego, Andrew Myers Cornell University
17:00
20m
Talk
Chairs' Report
Research Papers
P: Andrew Myers Cornell University, G: Ranjit Jhala University of California, San Diego
17:20
10m
Talk
POPL 2019 Preview
Research Papers
G: Fritz Henglein DIKU, Denmark, P: Stephanie Weirich University of Pennsylvania, USA
17:30
30m
Talk
SIGPLAN Town Hall
Research Papers
Michael Hicks University of Maryland, College Park, Benjamin C. Pierce University of Pennsylvania
18:15 - 20:15
POPL Poster SessionResearch Papers at SRC
18:15
2h
Other
POPL Poster Session
Research Papers

18:30 - 20:30
18:30
7m
Talk
A Decidable Logic for Tree Data-Structures with Measurements
Student Research Competition
18:37
7m
Talk
Combining Control Operators and Dependent Types
Student Research Competition
Youyou Cong Ochanomizu University, Japan
18:44
7m
Talk
Comparing Liquid Haskell and Coq: Evaluating the Great Expectations of “A Tale of Two Provers”
Student Research Competition
18:51
7m
Talk
Comparison among three program verification techniques in Dependent Haskell, Liquid Haskell and F*
Student Research Competition
Xinyue Zhang Bryn Mawr College, USA, Rachel Xu
18:58
7m
Talk
Finite Maps At The Type Level
Student Research Competition
19:05
7m
Talk
Formal Models Underlying Blockchain Technology
Student Research Competition
Haochen Xie Nagoya University
19:12
7m
Talk
Generating Information-Flow Control Mechanisms from Programming Language Specifications
Student Research Competition
Andrew Bedford Laval University
19:19
7m
Talk
How to Make Your Programs Very Safe: A Review of Practical Applications of Dependent Types
Student Research Competition
19:26
7m
Talk
Modelling Microcontroller Hardware using Typestate
Student Research Competition
Rudi Horn University of Edinburgh
19:33
7m
Talk
Program Synthesis with Neural Oracles
Student Research Competition
19:40
7m
Talk
Propositional Dynamic Logic for Higher-Order Functional Programs
Student Research Competition
Yuki Satake University of Tsukuba
19:47
7m
Talk
Relational Cost Analysis with State
Student Research Competition
Weihao Qu University at Buffalo, SUNY
19:54
7m
Talk
Robust Example-based Synthesis
Student Research Competition
20:01
7m
Talk
Simplifying incremental code with IODyn
Student Research Competition
Kyle Headley University of Colorado Boulder
20:08
7m
Talk
Software Fault Isolation for Robust Compilation
Student Research Competition
Ana Nora Evans University of Virginia, USA
20:15
7m
Talk
Synchronous Proofs for Asynchronous Programs
Student Research Competition
Bernhard Kragl IST Austria
20:22
7m
Talk
Type-Driven Gradual Security with References
Student Research Competition
Matías Toro University of Chile

Fri 12 Jan

Displayed time zone: Tijuana, Baja California change

08:30 - 10:00
Keynote-IIIResearch Papers at Bunker Hill / Watercourt
Chair(s): Andrew Myers Cornell University
08:30
60m
Talk
Formal Methods and the Law
Research Papers
S: Sarah Lawsky Northwestern University
09:30
30m
Talk
Lightning Overview - Day 3
Research Papers

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
10:30 - 12:00
Finalist PresentationsStudent Research Competition at SRC
10:30
15m
Talk
Graduate Finalist 1
Student Research Competition

10:45
15m
Talk
Graduate Finalist 2
Student Research Competition

11:00
15m
Talk
Graduate Finalist 3
Student Research Competition

11:15
15m
Talk
Undergraduate Finalist 1
Student Research Competition

11:30
15m
Talk
Undergraduate Finalist 2
Student Research Competition

11:45
15m
Talk
Undergraduate Finalist 3
Student Research Competition

10:30 - 12:10
Dynamic LanguagesResearch Papers at Watercourt
Chair(s): Jean Yang Carnegie Mellon University
10:30
25m
Talk
Correctness of Speculative Optimizations with Dynamic Deoptimization
Research Papers
Olivier Flückiger Northeastern University, USA, Gabriel Scherer Northeastern University, USA, Ming-Ho Yee Northeastern University, USA, Aviral Goel Northeastern University, Amal Ahmed Northeastern University, USA, Jan Vitek Northeastern University
DOI Pre-print
10:55
25m
Talk
JaVerT: JavaScript Verification Toolchain
Research Papers
José Fragoso Santos Imperial College London, Petar Maksimović Imperial College London, Daiva Naudžiūnienė Imperial College London, Thomas Wood Imperial College London, Philippa Gardner Imperial College London
11:20
25m
Talk
Soft Contract Verification for Higher-order Stateful Programs
Research Papers
Phúc C. Nguyễn University of Maryland, Thomas Gilray University of Maryland, Sam Tobin-Hochstadt Indiana University, David Van Horn University of Maryland
11:45
25m
Talk
Collapsing Towers of Interpreters
Research Papers
Nada Amin University of Cambridge, Tiark Rompf Purdue University
12:10 - 13:30
12:10
80m
Lunch
Friday Lunch
Research Papers

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
13:40 - 15:20
ProbabilityResearch Papers at Watercourt
Chair(s): Lars Birkedal Aarhus University
13:40
25m
Talk
Proving expected sensitivity of probabilistic programs
Research Papers
Gilles Barthe IMDEA Software Institute, Thomas Espitau Universite Pierre et Marie Curie, Benjamin Gregoire INRIA, Justin Hsu University College London, Pierre-Yves Strub Ecole Polytechnique
14:05
25m
Talk
Synthesizing Coupling Proofs of Differential Privacy
Research Papers
Aws Albarghouthi University of Wisconsin-Madison, Justin Hsu University College London
14:30
25m
Talk
Measurable cones and stable, measurable functions
Research Papers
Thomas Ehrhard CNRS and University Paris Diderot, Michele Pagani University Paris Diderot, Christine Tasson University Paris Diderot
14:55
25m
Talk
Denotational validation of higher-order Bayesian inference
Research Papers
Adam Ścibior University of Cambridge and MPI Tuebingen, Ohad Kammar University of Oxford, Matthijs Vákár University of Oxford, Sam Staton University of Oxford, Hongseok Yang University of Oxford, Yufei Cai University of Tuebingen, Klaus Ostermann University of Tuebingen, Sean Moss University of Oxford, Chris Heunen University of Edinburgh, Zoubin Ghahramani University of Cambridge
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
15:50 - 17:05
Types for StateResearch Papers at Watercourt
Chair(s): Neel Krishnaswami Computer Laboratory, University of Cambridge
15:50
25m
Talk
A Logical Relation for Monadic Encapsulation of State: Proving contextual equivalences in the presence of runST
Research Papers
Amin Timany imec-Distrinet KU-Leuven, Leo Stefanesco ENS Lyon, Morten Krogh-Jespersen Aarhus University, Lars Birkedal Aarhus University
16:15
25m
Talk
Recalling a Witness: Foundations and Applications of Monotonic State
Research Papers
Danel Ahman Inria Paris, Cédric Fournet Microsoft Research, Cătălin Hriţcu Inria Paris, Kenji Maillard Inria Paris and ENS Paris, Aseem Rastogi Microsoft Research, Nikhil Swamy Microsoft Research
Pre-print
16:40
25m
Talk
RustBelt: Securing the Foundations of the Rust Programming Language
Research Papers
Ralf Jung MPI-SWS, Jacques-Henri Jourdan CNRS, LRI, Université Paris-Sud, Robbert Krebbers Delft University of Technology, Derek Dreyer MPI-SWS

Sat 13 Jan

Displayed time zone: Tijuana, Baja California change

09:00 - 10:00
Welcome and Invited TalkPriSC at Hershey
Chair(s): Cătălin Hriţcu Inria Paris
09:00
10m
Talk
PriSC Welcome
PriSC
Cătălin Hriţcu Inria Paris
File Attached
09:10
50m
Talk
Challenges For Compiler-backed Security: From Sanitizer to Mitigation (Invited Talk)
PriSC
Mathias Payer Purdue University
File Attached
09:00 - 10:00
KeynoteCoqPL at Watercourt A
Chair(s): Yves Bertot INRIA
09:00
60m
Talk
CoqHammer: Strong Automation for Program Verification
CoqPL
Lukasz Czajka University of Innsbruck, Cezary Kaliszyk University of Innsbruck
File Attached
10:30 - 12:00
10:30
30m
Talk
Synthesizing Program-Specific Static Analyses
Off the Beaten Track
Colin Gordon Drexel University
File Attached
11:00
30m
Talk
On quantifying the degree of unsoundness of static analyses
Off the Beaten Track
File Attached
11:30
30m
Talk
Explaining Type Errors
Off the Beaten Track
Brent Yorgey Hendrix College, Richard A. Eisenberg Bryn Mawr College, USA, Harley D. Eades III Augusta University
File Attached
10:30 - 12:10
Tactics and Proof EngineeringCoqPL at Watercourt A
Chair(s): Benjamin Delaware Purdue University
10:30
25m
Talk
A “destruct” Tactic for Mtac2
CoqPL
Jan-Oliver Kaiser MPI-SWS, Beta Ziliani FAMAF, UNC and CONICET
File Attached
10:55
25m
Talk
Typed Template Coq
CoqPL
Simon Boulier , Matthieu Sozeau Inria, Nicolas Tabareau Inria, France, Abhishek Anand Cornell University
File Attached
11:20
25m
Talk
Elpi: an extension language for Coq
CoqPL
File Attached
11:45
25m
Talk
Coqatoo: Generating Natural Language Versions of Coq Proofs
CoqPL
Andrew Bedford Laval University
File Attached
13:30 - 15:30
Session 2Off the Beaten Track at Crocker
Chair(s): William E. Byrd University of Alabama at Birmingham, USA
13:30
30m
Lunch
Lunch (12pm-2pm)
Off the Beaten Track

14:00
30m
Talk
SweetPea: A Language for Designing Experiments
Off the Beaten Track
Annie Cherkaev University of Utah, Sebastian Musslick Princeton University, Jonathan Cohen Princeton University, Vivek Srikumar University of Utah, Matthew Flatt University of Utah
File Attached
14:30
30m
Talk
Extensible Semantics for Fluidics
Off the Beaten Track
Max Willsey University of Washington, Jared Roesch University of Washington, USA
File Attached
15:00
30m
Talk
Towards Proof Synthesis by Neural Machine Translation
Off the Beaten Track
Taro Sekiyama IBM Research, Japan, Akifumi Imanishi Kyoto University, Kohei Suenaga Graduate School of Informatics, Kyoto University
File Attached
13:30 - 15:30
Session 2PriSC at Hershey
Chair(s): David Naumann Stevens Institute of Technology
13:30
30m
Talk
Building Secure SGX Enclaves using F*, C/C++ and X64
PriSC
Anitha Gollamudi , Cédric Fournet Microsoft Research
File Attached
14:00
30m
Talk
Robust Hyperproperty Preservation for Secure Compilation
PriSC
Deepak Garg Max Planck Institute for Software Systems, Cătălin Hriţcu Inria Paris, Marco Patrignani Saarland University, CISPA, Marco Stronati , David Swasey MPI-SWS
Pre-print File Attached
14:30
30m
Talk
Formally Secure Compilation of Unsafe Low-Level Components
PriSC
Guglielmo Fachini Inria Paris, Cătălin Hriţcu Inria Paris, Marco Stronati , Ana Nora Evans University of Virginia, USA, Théo Laurent , Arthur Azevedo de Amorim Carnegie Mellon University, USA, Benjamin C. Pierce University of Pennsylvania, Andrew Tolmach Portland State University
Pre-print File Attached
15:00
30m
Talk
Secure Compilation in a Production Environment
PriSC
File Attached
14:00 - 14:50
PL MetatheoryCoqPL at Watercourt A
Chair(s): Steve Zdancewic University of Pennsylvania
14:00
25m
Talk
Locally Nameless at Scale
CoqPL
Stephanie Weirich University of Pennsylvania, USA, Antoine Voizard University of Pennsylvannia, Anastasiya Kravchuk-Kirilyuk University of Pennsylvania
File Attached
14:25
25m
Talk
A Coq Formalisation of a Core of R
CoqPL
File Attached
14:50 - 15:30
Coq developers talk & panelCoqPL at Watercourt A
14:50
40m
Talk
Session with the Coq Development Team
CoqPL
File Attached
16:00 - 18:00
16:00
30m
Talk
Back to the Future with Denotational Semantics
Off the Beaten Track
Jeremy G. Siek Indiana University, USA
File Attached
16:30
30m
Talk
Climbing Up the Semantic Tower — at Runtime
Off the Beaten Track
File Attached
17:00
30m
Talk
Towards A Systems Approach To Distributed Programming
Off the Beaten Track
Christopher Meiklejohn Université catholique de Louvain, Peter Van Roy Université catholique de Louvain
File Attached
17:30
30m
Day closing
Discussion and business meeting
Off the Beaten Track

16:00 - 18:05
Semantics and SynthesisCoqPL at Watercourt A
Chair(s): Ilya Sergey University College London
16:00
25m
Talk
Phantom Types for Quantum Programs
CoqPL
Robert Rand University of Pennsylvania, Jennifer Paykin University of Pennsylvania, Steve Zdancewic University of Pennsylvania
File Attached
16:25
25m
Talk
Revisiting Parametricity: Inductives and Uniformity of Propositions
CoqPL
Abhishek Anand Cornell University, Greg Morrisett Cornell University
File Attached
16:50
25m
Talk
Towards Context-Aware Data Refinement
CoqPL
Paul Krogmeier Purdue University, Steven Kidd Purdue University, Benjamin Delaware Purdue University
File Attached
17:15
25m
Talk
Mechanizing the Construction and Rewriting of Proper Functions in Coq
CoqPL
Edwin Westbrook Galois, Inc.
File Attached
17:40
25m
Talk
A calculus for logical refinements in separation logic
CoqPL
Dan Frumin Radboud University, Robbert Krebbers Delft University of Technology
File Attached