POPL 2024
Sun 14 - Sat 20 January 2024 London, United Kingdom
VenueInstitution of Engineering and Technology
Room nameTuring Lecture
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

Sun 14 Jan

Displayed time zone: London change

09:00 - 10:30
ApplicationsDafny at Turing Lecture
Chair(s): Stefan Zetzsche Amazon Web Services
09:00
10m
Day opening
Day opening
Dafny
Stefan Zetzsche Amazon Web Services, Joseph Tassarotti NYU
09:10
60m
Keynote
Verifying a concurrent file system with sequential reasoning
Dafny
Tej Chajed UW-Madison
10:12
18m
Talk
Towards the verification of a generic interlocking logic: Dafny meets parameterized model checking
Dafny
Alessandro Cimatti Fondazione Bruno Kessler, Alberto Griggio Fondazione Bruno Kessler, Gianluca Redondi Fondazione Bruno Kessler
11:00 - 12:30
Testing and Teaching / ComparisonDafny at Turing Lecture
Chair(s): Joseph Tassarotti NYU
11:00
18m
Talk
Dafny Test Generationremote
Dafny
Aleksandr Fedchin Tufts University, Jeffrey S. Foster Tufts University, Zvonimir Rakamaric Amazon Web Services, Aaron Tomb Amazon Web Services
11:18
18m
Talk
Randomised Testing of the Dafny Compiler
Dafny
Alastair F. Donaldson Imperial College London, Dilan Sheth Imperial College London, Jean-Baptiste Tristan Amazon Web Services, Alex Usher Imperial College London
11:36
18m
Talk
Teaching Logic and Set Theory with Dafny
Dafny
Ran Ettinger NVIDIA and Ben-Gurion University of the Negev and Israel Academic College in Ramat Gan, Hezi Daniel Israel Academic College in Ramat Gan
11:54
18m
Talk
Learn 'em Dafny
Dafny
James Noble Creative Research & Programming
Pre-print
12:12
18m
Talk
Colouring Flags with Dafny & Idris
Dafny
Jan de Muijnck-Hughes University of Strathclyde, James Noble Creative Research & Programming
14:00 - 15:30
Proof Stability / Brittleness / ScaleDafny at Turing Lecture
Chair(s): Stefan Zetzsche Amazon Web Services
14:00
18m
Talk
Enhancing Proof Stability
Dafny
Sean McLaughlin Amazon Web Services, Georges-Axel Jaloyan Amazon Web Services, Tongtong Xiang Amazon Web Services, Florian Rabe Amazon Web Services
14:18
18m
Talk
Improving the Stability of Type Safety Proofs in Dafny
Dafny
Joseph W. Cutler University of Pennsylvania, Michael Hicks Amazon Web Services and the University of Maryland, Emina Torlak Amazon Web Services, USA
14:36
18m
Talk
Incremental Proof Development in Dafny with Module-Based Induction
Dafny
14:54
18m
Talk
Portfolio Solving for Dafny
Dafny
Eric Mugnier University of California San Diego, Sean McLaughlin Amazon Web Services, Aaron Tomb Amazon Web Services
15:12
18m
Talk
Domesticating Automation
Dafny
Pranav Srinivasan University of Michigan / VMware Research, Oded Padon VMware Research, Jon Howell VMware Research, Andrea Lattuada VMware Research
16:00 - 17:30
Probabilistic Programs and Testing / Verifying ContractsDafny at Turing Lecture
Chair(s): Joseph Tassarotti NYU
16:00
18m
Talk
VMC: a Dafny Library for Verified Monte Carlo Algorithms
Dafny
Fabian Zaiser University of Oxford, Stefan Zetzsche Amazon Web Services, Jean-Baptiste Tristan Amazon Web Services
16:18
18m
Talk
Caesar: A Verifier for Probabilistic Programs
Dafny
Philipp Schröer RWTH Aachen University, Kevin Batz RWTH Aachen University, Benjamin Lucien Kaminski Saarland University; University College London, Joost-Pieter Katoen RWTH Aachen University, Christoph Matheja DTU
16:36
18m
Talk
Verifying Dafny Contract Integrity
Dafny
Cassidy Waldrip Brigham Young University, Eric Mercer Brigham Young University
16:54
18m
Talk
Testing Specifications In Dafny
Dafny
Eli Goldweber University Of Michigan, Weixin Yu University Of Michigan, Armin Vakil University Of Michigan, Manos Kapritsos University of Michigan, USA
17:30 - 18:15
Code GenerationDafny at Turing Lecture
Chair(s): Stefan Zetzsche Amazon Web Services
17:30
18m
Talk
Generation of Verified Assembly Code Using Dafny and Reinforcement Learning
Dafny
Christopher Brix RWTH Aachen University, Jean-Baptiste Tristan Amazon Web Services
17:48
18m
Talk
CLOVER: Closed-Loop Verifiable Code Generation
Dafny
Chuyue Sun Stanford University, Ying Sheng Stanford University, Oded Padon VMware Research, Clark Barrett Stanford University
18:06
9m
Day closing
Day closing
Dafny
Stefan Zetzsche Amazon Web Services, Joseph Tassarotti NYU

Mon 15 Jan

Displayed time zone: London change

09:00 - 10:30
Session 1The Future of Weak Memory at Turing Lecture
Chair(s): John Wickerson Imperial College London
09:00
10m
Talk
Welcome
The Future of Weak Memory
John Wickerson Imperial College London, Azalea Raad Imperial College London, Brijesh Dongol University of Surrey, Mark Batty University of Kent, Peter Sewell University of Cambridge
09:10
20m
Talk
Some things I wish I hadn’t seen
The Future of Weak Memory
Matthew J. Parkinson Microsoft Azure Research
09:30
20m
Talk
Heterogeneous concurrency -- a new frontier for weak memory
The Future of Weak Memory
09:50
20m
Talk
Chasing Unicorns and Not Losing Hope in Validating Weak Memory Persistency Models
The Future of Weak Memory
Vasileios Klimis Queen Mary University of London
File Attached
10:10
20m
Talk
How Do We Know That Weak Memory Matters?
The Future of Weak Memory
Mike Dodds Galois, Inc.
File Attached
11:00 - 12:30
Session 2The Future of Weak Memory at Turing Lecture
Chair(s): John Wickerson Imperial College London
11:00
22m
Talk
Weak Memory Demands Model-based Compiler Testing
The Future of Weak Memory
Luke Geeson University College London (UCL)
File Attached
11:22
22m
Talk
On the need for available, functional, and reusable memory models
The Future of Weak Memory
Hernán Ponce de León Huawei Dresden Research Center
11:45
22m
Talk
What we learned from C++ atomics and memory model standardization
The Future of Weak Memory
12:07
22m
Talk
Why Languages Should Preserve Load-Store Order
The Future of Weak Memory
Stephen Dolan Jane Street
14:00 - 15:30
Session 3The Future of Weak Memory at Turing Lecture
Chair(s): Brijesh Dongol University of Surrey
14:00
20m
Talk
Compilers should get over themselves and respect semantic dependencies!
The Future of Weak Memory
14:20
20m
Talk
A case against semantic dependencies
The Future of Weak Memory
Ori Lahav Tel Aviv University
14:40
20m
Talk
What Compilers desire from Weak Memory SemanticsRemote
The Future of Weak Memory
Akshay Gopalakrishnan McGill University
File Attached
15:00
20m
Talk
Programmers love mind-bogglingly complicated weak memory models
The Future of Weak Memory
File Attached
16:00 - 17:30
Session 4The Future of Weak Memory at Turing Lecture
Chair(s): Brijesh Dongol University of Surrey
16:00
22m
Talk
Evolving Weak Memory Models for Evolving Architectures
The Future of Weak Memory
Reese Levine University of California at Santa Cruz
16:22
22m
Talk
In-order execution nails every weak memory behavior
The Future of Weak Memory
Chung-Kil Hur Seoul National University
16:45
22m
Talk
System-level weak memory models: The need for formalisation, ISA semantics integration and model diversity
The Future of Weak Memory
Thibaut Pérami University of Cambridge
17:07
22m
Talk
Relaxed systems semantics and how we (hope to) reason above it
The Future of Weak Memory

Tue 16 Jan

Displayed time zone: London change

09:00 - 10:30
First SessionPLMW @ POPL at Turing Lecture
09:00
10m
Day opening
Opening
PLMW @ POPL
Derek Dreyer MPI-SWS
09:10
35m
Social Event
Ice Breaker
PLMW @ POPL

09:45
45m
Talk
The Evolution of Effects
PLMW @ POPL
Nicolas Wu Imperial College London
11:00 - 12:30
Second SessionPLMW @ POPL at Turing Lecture
Chair(s): Leonidas Lampropoulos University of Maryland, College Park
11:00
45m
Talk
Refinement Types from Light to Deep Verification
PLMW @ POPL
Niki Vazou IMDEA Software Institute
11:45
45m
Panel
Panel
PLMW @ POPL
Leonidas Lampropoulos University of Maryland, College Park, Derek Dreyer MPI-SWS, Jules Jacobs Radboud University Nijmegen, Niki Vazou IMDEA Software Institute, Sam Westrick Carnegie Mellon University
14:00 - 15:30
Third SessionPLMW @ POPL at Turing Lecture
Chair(s): Andrew K. Hirsch University at Buffalo, SUNY
14:00
45m
Talk
The Potential of Information-Flow Control Research for helping GDPR Compliance
PLMW @ POPL
Alejandro Russo Chalmers University of Technology, Sweden
14:45
45m
Talk
Consider Collaboration
PLMW @ POPL
Harrison Goldstein University of Pennsylvania, Samantha Frohlich University of Bristol
16:00 - 17:30
Fourth SessionPLMW @ POPL at Turing Lecture
Chair(s): Hannah Gommerstadt Vassar College
16:00
45m
Talk
How to Give a Talk
PLMW @ POPL
Neel Krishnaswami University of Cambridge
16:45
45m
Talk
Managing undergraduate research, as mentor and mentee
PLMW @ POPL
Mae Milano Princeton University
18:00 - 21:30
18:00
3h30m
Social Event
Jane Street Board Game Night
PLMW @ POPL
Chris Casinghino Jane Street, Richard A. Eisenberg Jane Street

Wed 17 Jan

Displayed time zone: London change

08:50 - 09:00
Welcome from the ChairPOPL at Turing Lecture
10:30 - 11:50
Types 1POPL at Turing Lecture
Chair(s): Mae Milano Princeton University
10:30
20m
Talk
Generating Well-Typed Terms that are not "Useless"
POPL
Justin Frank University of Maryland, College Park, Benjamin Quiring University of Maryland, Leonidas Lampropoulos University of Maryland, College Park
10:50
20m
Talk
Indexed Types for a Statically Safe WebAssembly
POPL
Adam Geller Computer Science, University of British Columbia, Justin Frank University of Maryland, College Park, William J. Bowman University of British Columbia
DOI Pre-print
11:10
20m
Talk
The Essence of Generalized Algebraic Data TypesRemote
POPL
Filip Sieczkowski Heriot-Watt University, Sergei Stepanenko Aarhus University, Jonathan Sterling University of Cambridge, Lars Birkedal Aarhus University
11:30
20m
Talk
Ill-Typed Programs Don't Evaluate
POPL
Steven Ramsay University of Bristol, Charlie Walpole University of Bristol
13:20 - 14:40
Automated VerificationPOPL at Turing Lecture
Chair(s): Gregory Malecha BedRock Systems
13:20
20m
Talk
Regular Abstractions for Array Systems
POPL
Chih-Duo Hong National Chengchi University, Anthony Widjaja Lin TU Kaiserslautern; MPI-SWS
13:40
20m
Talk
An Infinite Needle in a Finite Haystack: Finding Infinite Counter-Models in Deductive VerificationDistinguished Paper
POPL
Neta Elad Tel Aviv University, Oded Padon VMware Research, Sharon Shoham Tel Aviv University
Link to publication DOI
14:00
20m
Talk
Mostly Automated Verification of Liveness Properties for Distributed Protocols with Ranking FunctionsRemote
POPL
Jianan Yao Columbia University, Runzhou Tao Columbia University, Ronghui Gu Columbia University, Jason Nieh Columbia University
14:20
20m
Talk
Decision and Complexity of Dolev-Yao Hyperproperties
POPL
Itsaka Rakotonirina MPI-SP, Gilles Barthe MPI-SP; IMDEA Software Institute, Clara Schneidewind MPI-SP
15:10 - 16:30
Separation LogicPOPL at Turing Lecture
Chair(s): Azalea Raad Imperial College London
15:10
20m
Talk
An Iris Instance for Verifying CompCert C Programs
POPL
William Mansky University of Illinois Chicago, Ke Du
Pre-print
15:30
20m
Talk
The Logical Essence of Well-Bracketed Control Flow
POPL
Amin Timany Aarhus University, Armaël Guéneau Université Paris-Saclay - CNRS - ENS Paris-Saclay - Inria, Lars Birkedal Aarhus University
15:50
20m
Talk
Asynchronous Probabilistic Couplings in Higher-Order Separation Logic
POPL
Simon Oddershede Gregersen Aarhus University, Alejandro Aguirre Aarhus University, Philipp G. Haselwarter Aarhus University, Joseph Tassarotti NYU, Lars Birkedal Aarhus University
DOI Pre-print
16:10
20m
Talk
Thunks and Debits in Separation Logic with Time Credits
POPL
François Pottier Inria, Armaël Guéneau Université Paris-Saclay - CNRS - ENS Paris-Saclay - Inria, Jacques-Henri Jourdan CNR, LMF, Glen Mével
16:50 - 18:10
Domain-Specific LanguagesPOPL at Turing Lecture
Chair(s): Satnam Singh Groq
16:50
20m
Talk
EasyBC: A Cryptography-Specific Language for Security Analysis of Block Ciphers against Differential Cryptanalysis
POPL
Pu Sun ShanghaiTech University, Fu Song State Key Laboratory of Computer Science, Institute of Software, Chinese Academy of Sciences, and University of Chinese Academy of Sciences Beijing, China, Yuqi Chen ShanghaiTech University, China, Taolue Chen University of London
17:10
20m
Talk
A Core Calculus for Documents: Or, Lambda: The Ultimate Document
POPL
Will Crichton Brown University, Shriram Krishnamurthi Brown University
Pre-print
17:30
20m
Talk
Validation of Modern JSON Schema: Formalization and Complexity
POPL
Lyes Attouche Université Paris-Dauphine -- PSL, Mohamed-Amine Baazizi Sorbonne Université, Dario Colazzo Université Paris-Dauphine -- PSL, Giorgio Ghelli Universita di Pisa, Carlo Sartiani Università della Basilicata, Stefanie Scherzinger Universität Passau
DOI
17:50
20m
Talk
Shoggoth - A Formal Foundation for Strategic Rewriting
POPL
Xueying Qin The University of Edinburgh, Liam O'Connor University of Edinburgh, Rob van Glabbeek The University of Edinburgh, Peter Hoefner Australian National University, Ohad Kammar University of Edinburgh, Michel Steuwer TU Berlin; University of Edinburgh
Pre-print

Thu 18 Jan

Displayed time zone: London change

09:00 - 10:20
Higher-Order Effectful ProgramsPOPL at Turing Lecture
Chair(s): Sam Lindley University of Edinburgh
09:00
20m
Talk
On Model-Checking Higher-Order Effectful Programs
POPL
Ugo Dal Lago University of Bologna & INRIA Sophia Antipolis, Alexis Ghyselen University of Bologna
09:20
20m
Talk
Explicit Effects and Effect Constraints in ReML
POPL
Martin Elsman University of Copenhagen, Denmark
Link to publication DOI
09:40
20m
Talk
Decalf: A Directed, Effectful Cost-Aware Logical Framework
POPL
Harrison Grodin , Jonathan Sterling University of Cambridge, Yue Niu Carnegie Mellon University, Robert Harper Carnegie Mellon University
Pre-print
10:00
20m
Talk
Modular Denotational Semantics for Effects with Guarded Interaction TreesDistinguished PaperRemote
POPL
Daniel Frumin University of Groningen, Amin Timany Aarhus University, Lars Birkedal Aarhus University
DOI Pre-print
10:50 - 12:10
Probabilistic ProgramsPOPL at Turing Lecture
Chair(s): Jules Jacobs Radboud University Nijmegen
10:50
20m
Talk
Probabilistic programming interfaces for random graphs: Markov categories, graphons, and nominal sets
POPL
Nate Ackerman Harvard University, Cameron Freer Massachusetts Institute of Technology, Younesse Kaddar University of Oxford, Jacek Karwowski University of Oxford, Sean Moss University of Oxford, Daniel Roy University of Toronto, Sam Staton University of Oxford, Hongseok Yang KAIST; IBS
11:10
20m
Talk
Inference of Probabilistic Programs with Moment-Matching Gaussian Mixtures
POPL
Francesca Randone IMT School for Advanced Studies Lucca, Luca Bortolussi Department of Mathematics and Geosciences, University of Trieste, Emilio Incerto IMT School for Advanced Studies Lucca, Mirco Tribastone IMT Institute for Advanced Studies Lucca, Italy
11:30
20m
Talk
Higher Order Bayesian Networks, Exactly
POPL
Claudia Faggian Université de Paris & CNRS, Daniele Pautasso Università di Torino, Gabriele Vanoni IRIF, Université Paris Cité
11:50
20m
Talk
Strong Invariants Are Hard: On the Hardness of Strongest Polynomial Invariants for (Probabilistic) Programs
POPL
13:40 - 15:00
Weak Memory and Concurrent Separation LogicPOPL at Turing Lecture
Chair(s): William Mansky University of Illinois Chicago
13:40
20m
Talk
How Hard is Weak-Memory Testing?
POPL
Soham Chakraborty TU Delft, Shankaranarayanan Krishna IIT Bombay, India, Umang Mathur National University of Singapore, Andreas Pavlogiannis Aarhus University
Pre-print
14:00
20m
Talk
An Axiomatic Basis for Computer Programming on the Relaxed Arm-A Architecture: The AxSL Logic
POPL
Angus Hammond University of Cambridge, Zongyuan Liu Aarhus University, Thibaut Pérami University of Cambridge, Peter Sewell University of Cambridge, Lars Birkedal Aarhus University, Jean Pichon-Pharabod Aarhus University
Pre-print
14:20
20m
Talk
Trillium: Higher-Order Concurrent and Distributed Separation Logic for Intensional Refinement
POPL
Amin Timany Aarhus University, Simon Oddershede Gregersen Aarhus University, Leo Stefanesco MPI-SWS, Jonas Kastberg Hinrichsen Aarhus University, Denmark, Léon Gondelman Aarhus University, Abel Nieto Aarhus University, Lars Birkedal Aarhus University
14:40
20m
Talk
Deadlock-Free Separation Logic: Linearity Yields Progress for Dependent Higher-Order Message Passing
POPL
Jules Jacobs Radboud University Nijmegen, Jonas Kastberg Hinrichsen Aarhus University, Denmark, Robbert Krebbers Radboud University Nijmegen
Pre-print
15:30 - 16:50
Algorithmic VerificationPOPL at Turing Lecture
Chair(s): Andreas Pavlogiannis Aarhus University
15:30
20m
Talk
Polyregular functions on unordered trees of bounded height
POPL
Mikolaj Bojanczyk Warsaw University, Bartek Klin University of Oxford
15:50
20m
Talk
Solving Infinite-State Games via Acceleration
POPL
Philippe Heim CISPA Helmholtz Center for Information Security, Rayna Dimitrova CISPA Helmholtz Center for Information Security
Pre-print
16:10
20m
Talk
Ramsey Quantifiers in Linear Arithmetics
POPL
Pascal Bergsträßer University of Kaiserslautern-Landau, Moses Ganardi MPI-SWS, Anthony Widjaja Lin TU Kaiserslautern; MPI-SWS, Georg Zetzsche MPI-SWS
Pre-print
16:30
20m
Talk
Reachability in Continuous Pushdown VASS
POPL
A. R. Balasubramanian Technical University of Munich, Rupak Majumdar MPI-SWS, Ramanathan S. Thinniyam Uppsala University, Georg Zetzsche MPI-SWS
Pre-print

Fri 19 Jan

Displayed time zone: London change

08:50 - 09:00
WelcomePOPL at Turing Lecture
08:50
10m
Other
Extraordinary Meeting: The Publicity Chairs Reflect on the Peer-Review Process
POPL
Alastair F. Donaldson Imperial College London, John Wickerson Imperial College London
10:30 - 11:50
Type TheoryPOPL at Turing Lecture
Chair(s): Kuen-Bang Hou (Favonia) University of Minnesota
10:30
20m
Talk
Internal parametricity, without an interval
POPL
Thorsten Altenkirch University of Nottingham, Yorgo Chamoun École Polytechnique, Ambrus Kaposi Eötvös Loránd University, Michael Shulman University of San Diego
Pre-print
10:50
20m
Talk
Internal and Observational Parametricity for Cubical Agda
POPL
Antoine Van Muylder KU Leuven, Andreas Nuyts KU Leuven, Belgium, Dominique Devriese KU Leuven
11:10
20m
Talk
Internalizing Indistinguishability with Dependent TypesRemote
POPL
Yiyun Liu University of Pennsylvania, Jonathan Chan University of Pennsylvania, Jessica Shi University of Pennsylvania, Stephanie Weirich University of Pennsylvania
11:30
20m
Talk
Polynomial Time and Dependent types
POPL
Robert Atkey University of Strathclyde
13:20 - 14:40
MedleyPOPL at Turing Lecture
Chair(s): Xiaokang Qiu Purdue University
13:20
20m
Talk
Guided Equality Saturation
POPL
Thomas Koehler INRIA, Andrés Goens University of Amsterdam, Siddharth Bhat the University of Edinburgh, Tobias Grosser University of Edinburgh, Phil Trinder University of Glasgow, Michel Steuwer TU Berlin; University of Edinburgh
Pre-print
13:40
20m
Talk
Fusing Direct Manipulations into Functional Programs
POPL
Xing Zhang Peking University, Ruifeng Xie Peking University, Guanchen Guo Peking University, Xiao He University of Science and Technology Beijing, Tao Zan Longyan University, Zhenjiang Hu Peking University
Pre-print
14:00
20m
Talk
Inference of Robust Reachability Constraints
POPL
Yanis Sellami CEA, List, Univ. Grenoble Alpes, Guillaume Girol CEA, List, Université Paris Saclay, Frédéric Recoules CEA, List, Damien Couroussé Univ Grenoble Alpes, CEA, List, Sébastien Bardin CEA LIST, University Paris-Saclay
14:20
20m
Talk
Nominal Recursors as Epi-RecursorsDistinguished Paper
POPL
Andrei Popescu University of Sheffield
15:10 - 16:30
Mechanized ProofsPOPL at Turing Lecture
Chair(s): Andrei Popescu University of Sheffield
15:10
20m
Talk
Mechanizing Refinement Types
POPL
Michael Borkowski University of California, San Diego, Niki Vazou IMDEA Software Institute, Ranjit Jhala University of California at San Diego
15:30
20m
Talk
VST-A: A Foundationally Sound Annotation Verifier
POPL
Litao Zhou Shanghai Jiao Tong University; University of Hong Kong, Jianxing Qin Shanghai Jiao Tong University, Qinshi Wang Princeton University, Andrew W. Appel Princeton University, Qinxiang Cao Shanghai Jiao Tong University
15:50
20m
Talk
Fully Composable and Adequate Verified Compilation with Direct Refinements between Open Modules
POPL
Ling Zhang Shanghai Jiao Tong University, Yuting Wang Shanghai Jiao Tong University, Jinhua Wu Shanghai Jiao Tong University, Jérémie Koenig Yale University, Zhong Shao Yale University
Pre-print
16:10
20m
Talk
A Formalization of Core Why3 in Coq
POPL
Joshua M. Cohen Princeton University, Philip Johnson-Freyd Sandia National Laboratories
16:50 - 17:50
Logical FoundationsPOPL at Turing Lecture
Chair(s): Emanuele D’Osualdo MPI-SWS
16:50
20m
Talk
Orthologic with Axioms
POPL
Simon Guilloud École Polytechnique Fédérale de Lausanne, Viktor Kunčak EPFL, Switzerland
Pre-print
17:10
20m
Talk
Deciding Asynchronous Hyperproperties for Recursive Programs
POPL
Jens Oliver Gutsfeld Westfälische Wilhelm-Universität Münster (WWU), Germany, Markus Müller-Olm University of Münster, Christoph Ohrem University of Münster
Pre-print
17:30
20m
Talk
Calculational Design of [In]Correctness Transformational Program Logics by Abstract Interpretation
POPL
Patrick Cousot New York University
18:10 - 18:15
Farewell from the ChairPOPL at Turing Lecture

Sat 20 Jan

Displayed time zone: London change

09:00 - 10:30
Session 1PriSC at Turing Lecture
Chair(s): Marco Patrignani University of Trento
09:00
5m
Day opening
Introduction
PriSC
Shweta Shinde ETH Zurich, Marco Patrignani University of Trento
09:05
60m
Keynote
Keynote: Can we reason about the security of concurrent systems code?
PriSC
Peter Sewell University of Cambridge
10:05
25m
Talk
Secure Calling Conventions for CHERI Capability Machines in Practice (Work in Progress)
PriSC
Elias Storme KU Leuven, Sander Huyghebaert Vrije Universiteit Brussel, Steven Keuchel Vrije Universiteit Brussel, Thomas Van Strydonck KULeuven, Dominique Devriese KU Leuven
File Attached
11:00 - 12:30
Session 2PriSC at Turing Lecture
Chair(s): Marco Vassena Utrecht University
11:00
22m
Talk
Microarchitectural Side-Channel Mitigations for Serverless Applications
PriSC
Yayu Wang The University of British Columbia, Aastha Mehta The University of British Columbia
File Attached
11:22
22m
Talk
Lifting Compiler Security Properties to Stronger Attackers: the Speculation Case
PriSC
Xaver Fabian Cispa Helmholtz Center for Information Security, Marco Guarnieri IMDEA Software Institute, Michael Backes Cispa Helmholtz Center for Information Security
File Attached
11:45
22m
Talk
Secure Composition of SPECTRE Mitigations
PriSC
Matthis Kruse CISPA Helmholtz Center for Information Security, Michael Backes Cispa Helmholtz Center for Information Security
File Attached
12:07
22m
Talk
When Obfuscations Preserve Cryptographic Constant-Time
PriSC
Matteo Busi University Ca' Foscari, Venice, Pierpaolo Degano University of Pisa and IMT School for Advanced Studies Lucca, Letterio Galletta IMT School for Advanced Studies Lucca
File Attached
14:00 - 15:30
Session 3PriSC at Turing Lecture
Chair(s): Matteo Busi University Ca' Foscari, Venice
14:00
22m
Talk
Compiler Support for Control-Flow Linearization Using Architectural Mimicry
PriSC
File Attached
14:22
22m
Talk
Modularizing CPU Semantics for Virtualization
PriSC
Paolo G. Giarrusso BedRock Systems, Abhishek Anand BedRock Systems, Gregory Malecha BedRock Systems, František Farka BedRock Systems, Hoang-Hai Dang BedRock Systems
File Attached
14:45
22m
Talk
All the Binaries Together: A Semantic Approach to Application Binary Interfaces
PriSC
Andrew Wagner Northeastern University, Amal Ahmed Northeastern University, USA
File Attached
15:07
22m
Talk
Short Talks
PriSC

16:00 - 17:30
Session 4PriSC at Turing Lecture
Chair(s): Dominique Devriese KU Leuven
16:00
22m
Talk
Computational-Bounded Robust Compilation and Universally Composable Security
PriSC
Robert Künnemann CISPA Helmholtz Center for Information Security, Ethan Cecchetti University of Wisconsin-Madison
File Attached
16:22
22m
Talk
Gradual Verification for Smart Contracts
PriSC
Haojia Sun Shanghai Jiao Tong University, Kunal Singh Carnegie Mellon University, Jan-Paul Ramos-Davila Cornell University, Jonathan Aldrich Carnegie Mellon University, Jenna Wise (DiVincenzo) Purdue University
File Attached
16:45
22m
Talk
Towards Modular Specification and Verification of Concurrent Hypervisor-based Isolation
PriSC
Hoang-Hai Dang BedRock Systems, David Swasey BedRock Systems, Gregory Malecha BedRock Systems
File Attached
17:07
8m
Day closing
Closing Remarks
PriSC
Shweta Shinde ETH Zurich

Mon 15 Jan

Displayed time zone: London change

Tue 16 Jan

Displayed time zone: London change

Room9:003010:003011:003012:003013:003014:003015:003016:003017:003018:003019:003020:003021:0030
Turing Lecture

Wed 17 Jan

Displayed time zone: London change

Fri 19 Jan

Displayed time zone: London change

Sat 20 Jan

Displayed time zone: London change

Room9:003010:003011:003012:003013:003014:003015:003016:003017:0030
Turing Lecture

Mon 15 Jan

Displayed time zone: London change

Room9:0015304510:0015304511:0015304512:0015304513:0015304514:0015304515:0015304516:0015304517:00153045
Turing Lecture

Tue 16 Jan

Displayed time zone: London change