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

Room information: Hershey

VenueOmni Hotel
Room nameHershey
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

Mon 8 Jan

Displayed time zone: Tijuana, Baja California change

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
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
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

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
10:30 - 11:30
Session 1PriSC at Hershey
Chair(s): Amal Ahmed Northeastern University, USA
10:30
30m
Talk
Linear capabilities for modular fully-abstract compilation of verified code
PriSC
Thomas Van Strydonck KULeuven, Dominique Devriese KU Leuven, Frank Piessens KU Leuven
File Attached
11:00
30m
Talk
Enforcing Well-bracketed Control Flow and Stack Encapsulation using Linear Capabilities
PriSC
Lau Skorstengaard , Dominique Devriese KU Leuven, Lars Birkedal Aarhus University
File Attached
11:30 - 12:00
Short Talks SessionPriSC at Hershey
Chair(s): Dominique Devriese KU Leuven
11:30
5m
Talk
Short talk: The Meaning of Memory Safety
PriSC
Arthur Azevedo de Amorim Carnegie Mellon University, USA, Cătălin Hriţcu Inria Paris, Benjamin C. Pierce University of Pennsylvania
Pre-print File Attached
11:35
5m
Talk
Short talk: Dependently Typed Assembly for Secure Linking
PriSC
William J. Bowman Northeastern University, USA
Link to publication File Attached
11:40
5m
Talk
Short talk: Compiler Optimizations with Retrofitting Transformations: Is there a Semantic Mismatch?
PriSC
Santosh Nagarakatte Rutgers University, USA
Pre-print File Attached
11:45
5m
Talk
Short Talk: Secure compilation from F* to WebAssembly
PriSC
Jonathan Protzenko Microsoft Research, n.n.
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
Vijay D'Silva Google
File Attached
16:00 - 18:00
Session 3PriSC at Hershey
Chair(s): Lars Birkedal Aarhus University
16:00
30m
Talk
Constant-time WebAssembly
PriSC
John Renner UCSD, Sunjay Cauligi UCSD, Deian Stefan University of California, San Diego
Pre-print File Attached
16:30
30m
Talk
Per-Thread Compositional Compilation for Confidentiality-Preserving Concurrent Programs
PriSC
Rob Sison Data61, CSIRO and UNSW
File Attached
17:00
30m
Talk
On Compositional Compiler Correctness and Fully Abstract Compilation
PriSC
Daniel Patterson Northeastern University, Amal Ahmed Northeastern University, USA
File Attached
17:30
30m
Talk
Foundations of Dependent Interoperability
PriSC
Pierre-Evariste Dagand LIP6/CNRS , Nicolas Tabareau Inria, France, Éric Tanter University of Chile
Link to publication File Attached

Mon 8 Jan

Displayed time zone: Tijuana, Baja California change

Room11:003012:003013:003014:003015:003016:0030
Hershey

TutorialFest

Programming and Reasoning with Infinite Data in Isabelle

TutorialFest

Introduction to Algebraic Program analysis

TutorialFest

Introduction to Algebraic Program analysis

Sat 13 Jan

Displayed time zone: Tijuana, Baja California change

Room9:003010:003011:003012:003013:003014:003015:003016:003017:0030
Hershey

PriSC

Welcome and Invited Talk

PriSC

Session 1

PriSC

Short Talks Session

PriSC

Session 2

PriSC

Session 3

Mon 8 Jan

Displayed time zone: Tijuana, Baja California change

Room11:0015304512:0015304513:0015304514:0015304515:0015304516:00153045
Hershey
POPL TutorialFest
Programming and Reasoning with Infinite Data in Isabelle/HOL.
11:00 - 12:00
POPL TutorialFest
Introduction to Algebraic Program analysis.
14:00 - 15:30
POPL TutorialFest
Introduction to Algebraic Program analysis.
16:00 - 17:00

Sat 13 Jan

Displayed time zone: Tijuana, Baja California change

Room9:0015304510:0015304511:0015304512:0015304513:0015304514:0015304515:0015304516:0015304517:00153045
Hershey
PriSC
PriSC Welcome
09:00 - 09:10
PriSC
Challenges For Compiler-backed Security: From Sanitizer to Mitigation ( ...
09:10 - 10:00
PriSC
Linear capabilities for modular fully-abstract compilation of verified code
10:30 - 11:00
PriSC
Enforcing Well-bracketed Control Flow and Stack Encapsulation using Lin ...
11:00 - 11:30
PriSC
Short talk: The Meaning of Memory Safety
11:30 - 11:35
PriSC
Short talk: Dependently Typed Assembly for Secure Linking
11:35 - 11:40
PriSC
Short talk: Compiler Optimizations with Retrofitting Transformations: I ...
11:40 - 11:45
PriSC
Short Talk: Secure compilation from F* to WebAssembly
11:45 - 11:50
PriSC
Building Secure SGX Enclaves using F*, C/C++ and X64
13:30 - 14:00
PriSC
Robust Hyperproperty Preservation for Secure Compilation
14:00 - 14:30
PriSC
Formally Secure Compilation of Unsafe Low-Level Components
14:30 - 15:00
PriSC
Secure Compilation in a Production Environment
15:00 - 15:30
PriSC
Constant-time WebAssembly
16:00 - 16:30
PriSC
Per-Thread Compositional Compilation for Confidentiality-Preserving Con ...
16:30 - 17:00
PriSC
On Compositional Compiler Correctness and Fully Abstract Compilation
17:00 - 17:30
PriSC
Foundations of Dependent Interoperability
17:30 - 18:00