Filter Program
Dates
Rooms
Tracks
Badges
Your Program
Sun 14 JanDisplayed time zone: London change
Sun 14 Jan
Displayed time zone: London change
09:00 - 10:30 | |||
09:00 90mTutorial | Automated Datastructure Verification using Unfoldings and SMT Solving: Foundations and FO-CompletenessRemote TutorialFest P. Madhusudan University of Illinois at Urbana-Champaign, Adithya Murali University of Illinois at Urbana-Champaign | ||
09:00 - 10:30 | First SessionLAFI at Kelvin Lecture Chair(s): Steven Holtzen Northeastern University, Matthijs Vákár Utrecht University | ||
09:00 10mTalk | Opening Remarks LAFI | ||
09:10 60mKeynote | Hong Ge: Bayesian inference using probabilistic programming LAFI Hong Ge University of Cambridge | ||
10:10 20mTalk | Basis Talk LAFI | ||
09:00 - 10:30 | |||
09:00 45mKeynote | On Interaction, Efficiency, and Reversibility GALOP Ugo Dal Lago University of Bologna & INRIA Sophia Antipolis | ||
09:45 22mTalk | Normal Form Bisimulations by Value GALOP Beniamino Accattoli Inria & Ecole Polytechnique, Adrienne Lancelot Inria, LIX Ecole Polytechnique, IRIF Université Paris Cité, Claudia Faggian Université de Paris & CNRS | ||
10:08 22mTalk | Fully Abstract Normal Form Bisimulation for Call-by-Value PCF GALOP Nikos Tzevelekos Queen Mary University of London, Vasileios Koutavas Trinity College Dublin, Yu-Yang Lin Queen Mary University of London | ||
09:00 - 10:30 | |||
09:00 90mTalk | MetaCoq Tutorial TutorialFest Yannick Forster Inria, Meven Lennon-Bertrand University of Cambridge, Matthieu Sozeau Inria, Théo Winterhalter INRIA Saclay | ||
09:00 - 10:30 | Session 1O'Hearn Fest at Mountbatten Exhibition Chair(s): Matthew J. Parkinson Microsoft Azure Research | ||
09:00 22mTalk | Introduction O'Hearn Fest | ||
09:22 22mTalk | Peter's early work on parametricity, and why it still matters to me O'Hearn Fest Hongseok Yang KAIST; IBS | ||
09:45 22mTalk | Strong vs. weak separating conjunction in CSL O'Hearn Fest | ||
10:07 22mTalk | Verified Software at Scale O'Hearn Fest Philippa Gardner Imperial College London | ||
09:00 - 10:30 | |||
09:00 10mDay opening | Day opening Dafny | ||
09:10 60mKeynote | Verifying a concurrent file system with sequential reasoning Dafny Tej Chajed UW-Madison | ||
10:12 18mTalk | 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 | ||
10:30 - 11:00 | |||
10:30 30mCoffee break | Break Catering | ||
10:30 - 11:00 | |||
10:30 30mCoffee break | Break Catering | ||
11:00 - 12:30 | |||
11:00 90mTutorial | Automated Datastructure Verification using Unfoldings and SMT Solving: Foundations and FO-CompletenessRemote TutorialFest P. Madhusudan University of Illinois at Urbana-Champaign, Adithya Murali University of Illinois at Urbana-Champaign | ||
11:00 - 12:30 | |||
11:00 22mTalk | Operational game semantics for generative algebraic effects and handlers GALOP | ||
11:23 22mTalk | An abstract, certified account of Operational Game Semantics GALOP Peio Borthelle Univ. Grenoble Alpes, Univ. Savoie Mont Blanc, LAMA, 73000 Chambéry, Tom Hirschowitz Univ. Grenoble Alpes, Univ. Savoie Mont Blanc, CNRS, LAMA, 73000 Chambéry, Guilhem Jaber Nantes Université, Yannick Zakowski Inria | ||
11:45 22mTalk | Operational Algorithmic Game Semantics GALOP | ||
12:08 22mTalk | An algebraic theory of named threads (work in progress) GALOP Cristina Matache University of Edinburgh | ||
11:00 - 12:30 | |||
11:00 90mTalk | MetaCoq Tutorial TutorialFest Yannick Forster Inria, Meven Lennon-Bertrand University of Cambridge, Matthieu Sozeau Inria, Théo Winterhalter INRIA Saclay | ||
11:00 - 12:30 | |||
11:00 22mTalk | Later Credits: A Case Study in the Unreasonable Effectiveness of Separation Logic O'Hearn Fest Derek Dreyer MPI-SWS | ||
11:22 22mTalk | Bi-abductive adversarial program synthesis O'Hearn Fest Julien Vanegue Bloomberg, USA | ||
11:45 22mTalk | CSL and relaxed memory O'Hearn Fest Stephen Brookes CMU | ||
12:07 22mTalk | Is Peter Correct or Incorrect? O'Hearn Fest | ||
11:00 - 12:30 | |||
11:00 18mTalk | 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 18mTalk | 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 18mTalk | 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 18mTalk | Learn 'em Dafny Dafny James Noble Creative Research & Programming Pre-print | ||
12:12 18mTalk | Colouring Flags with Dafny & Idris Dafny | ||
12:30 - 14:00 | |||
12:30 90mLunch | Lunch Catering | ||
12:30 - 14:00 | |||
12:30 90mLunch | Lunch Catering | ||
14:00 - 15:30 | |||
14:00 90mTutorial | Scaling Verification of Concurrent Programs with the Civl Verifier TutorialFest | ||
14:00 - 15:30 | Third SessionLAFI at Kelvin Lecture Chair(s): Steven Holtzen Northeastern University, Matthijs Vákár Utrecht University | ||
14:00 10mTalk | Effect Handlers for Choice-Based Learning LAFI File Attached | ||
14:10 10mTalk | Guaranteed Bounds for Discrete Probabilistic Programs with Loops via Generating Functions LAFI File Attached | ||
14:20 10mTalk | JuliaBUGS: A Graph-Based Probabilistic Programming Language using BUGS syntax LAFI Xianda Sun University of Cambridge, Philipp Gabler Independent researcher, Andrew Thomas University of Cambridge, Hong Ge University of Cambridge | ||
14:30 10mTalk | Mixture Languages LAFI File Attached | ||
14:40 10mTalk | Structured Tensor Algebra for Efficient Discrete Probabilistic Inference LAFI Amir Shaikhha University of Edinburgh | ||
14:50 10mTalk | Towards a Categorical Model of the Lilac Separation Logic LAFI John Li Northeastern University, Jon Aytac Sandia National Laboratories, Philip Johnson-Freyd Sandia National Laboratories, Amal Ahmed Northeastern University, USA, Steven Holtzen Northeastern University File Attached | ||
15:00 10mTalk | Toward Probabilistic Coarse-to-Fine Program Synthesis LAFI Maddy Bowers Massachusetts Institute of Technology, Alexander K. Lew Massachusetts Institute of Technology, Vikash K. Mansinghka Massachusetts Institute of Technology, Joshua B. Tenenbaum Massachusetts Institute of Technology, Armando Solar-Lezama Massachusetts Institute of Technology | ||
15:10 10mTalk | Static Posterior Inference of Bayesian Probabilistic Programming via Polynomial SolvingOnline LAFI Peixin Wang University of Oxford, Hongfei Fu Shanghai Jiao Tong University, Tengshun Yang SKLCS, Institute of Software, Chinese Academy of Sciences & University of Chinese Academy of Sciences, Guanyan Li University of Oxford, C.-H. Luke Ong NTU | ||
15:20 10mTalk | Abstract Interpretation for Automatic DifferentiationOnline LAFI Jacob Laurel University of Illinois at Urbana-Champaign, Siyuan Brant Qian University of Illinois at Urbana-Champaign; Zhejiang University, Gagandeep Singh University of Illinois at Urbana-Champaign; VMware Research, Sasa Misailovic University of Illinois at Urbana-Champaign | ||
14:00 - 15:30 | |||
14:00 45mKeynote | Compositional Development of Certified System Software GALOP Zhong Shao Yale University | ||
14:45 22mTalk | SSA is Freyd Categories GALOP Jad Elkhaleq Ghalayini University of Cambridge | ||
15:08 22mTalk | A Denotational Approach to Release/Acquire Concurrency GALOP | ||
14:00 - 15:30 | |||
14:00 90mTutorial | String Solving for Verification TutorialFest Matthew Hague Royal Holloway University of London, Artur Jez University of Wroclaw, Anthony Widjaja Lin TU Kaiserslautern; MPI-SWS, Philipp Ruemmer University of Regensburg and Uppsala University | ||
14:00 - 15:30 | |||
14:00 22mTalk | Massive proofs for the masses O'Hearn Fest Byron Cook Amazon | ||
14:22 22mTalk | Designing Wait-free Weak Reference Counting O'Hearn Fest Matthew J. Parkinson Microsoft Azure Research | ||
14:45 22mTalk | Elegance and generosity are scientific values - And other things I've learned from Peter O'Hearn Fest Jade Alglave Arm and University College London | ||
15:07 22mTalk | Peter, the May and the Must, and Lacework O'Hearn Fest Patrice Godefroid Lacework | ||
14:00 - 15:30 | Proof Stability / Brittleness / ScaleDafny at Turing Lecture Chair(s): Stefan Zetzsche Amazon Web Services | ||
14:00 18mTalk | 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 18mTalk | 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 18mTalk | Incremental Proof Development in Dafny with Module-Based Induction Dafny | ||
14:54 18mTalk | Portfolio Solving for Dafny Dafny Eric Mugnier University of California San Diego, Sean McLaughlin Amazon Web Services, Aaron Tomb Amazon Web Services | ||
15:12 18mTalk | Domesticating Automation Dafny Pranav Srinivasan University of Michigan / VMware Research, Oded Padon VMware Research, Jon Howell VMware Research, Andrea Lattuada VMware Research | ||
15:30 - 16:00 | |||
15:30 30mCoffee break | Break Catering | ||
15:30 - 16:00 | |||
15:30 30mCoffee break | Break Catering | ||
16:00 - 17:30 | |||
16:00 90mTutorial | Scaling Verification of Concurrent Programs with the Civl Verifier TutorialFest | ||
16:00 - 17:30 | Poster and Interactive SessionLAFI at Kelvin Lecture Chair(s): Steven Holtzen Northeastern University, Matthijs Vákár Utrecht University Poster session taking place in the same room as the workshop. | ||
16:00 - 17:52 | |||
16:00 22mTalk | Invisible pebbles and the geometry of affine higher-order tree transducers GALOP | ||
16:22 22mTalk | Taylor Expansion is Game Semantics GALOP Lison Blondeau-Patissier LIS & I2M, Aix-Marseille Université, Pierre Clairambault CNRS & LIS, Aix-Marseille Université, Lionel Vaux Auclair University of Aix-Marseille | ||
16:44 22mTalk | Game-enriched categories GALOP Paul Blain Levy University of Birmingham | ||
17:07 22mTalk | Fair omega-Regular Games GALOP Daniel Hausmann University of Gothenburg, Nir Piterman University Gothenburg, Irmak Saglam Max Planck Institute for Software Systems (MPI-SWS), Anne-Kathrin Schmuck Max Planck Institute for Software Systems | ||
17:29 22mTalk | MELL proof-nets without boxes: thirty years later GALOP | ||
16:00 - 17:30 | |||
16:00 90mTutorial | String Solving for Verification TutorialFest Matthew Hague Royal Holloway University of London, Artur Jez University of Wroclaw, Anthony Widjaja Lin TU Kaiserslautern; MPI-SWS, Philipp Ruemmer University of Regensburg and Uppsala University | ||
16:00 - 17:30 | |||
16:00 22mTalk | Working with Peter O'Hearn in academia and industry O'Hearn Fest Mark Harman Meta Platforms, Inc. and UCL | ||
16:22 22mTalk | Pete's Footprints O'Hearn Fest Nick Benton Meta | ||
16:45 22mTalk | Symbolic Execution with Separating Decision Diagrams O'Hearn Fest Josh Berdine SkipLabs | ||
17:07 22mTalk | With Peter from Theory to Engineering O'Hearn Fest Dino Distefano Meta | ||
16:00 - 17:30 | Probabilistic Programs and Testing / Verifying ContractsDafny at Turing Lecture Chair(s): Joseph Tassarotti NYU | ||
16:00 18mTalk | 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 18mTalk | 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 18mTalk | Verifying Dafny Contract Integrity Dafny | ||
16:54 18mTalk | 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 | |||
17:30 18mTalk | Generation of Verified Assembly Code Using Dafny and Reinforcement Learning Dafny | ||
17:48 18mTalk | 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 9mDay closing | Day closing Dafny | ||
Mon 15 JanDisplayed time zone: London change
Mon 15 Jan
Displayed time zone: London change
09:00 - 10:30 | |||
09:00 90mTutorial | Foundations of Type-Driven Probabilistic Modelling TutorialFest Ohad Kammar University of Edinburgh Pre-print | ||
09:00 - 10:30 | |||
09:00 90mTutorial | Arm Architecture and Formal Artifacts: Memory Model and Instruction Semantics TutorialFest Jade Alglave Arm and University College London, Artem Khyzha Tel Aviv University, Israel, Luc Maranget Inria, Nikos Nikoleris Arm Research, Hugo O'Keeffe ARM, Hadrien Renaud UCL | ||
09:00 - 10:30 | |||
09:00 60mKeynote | Under-approximation for Scalable Bug Detection CPP Azalea Raad Imperial College London | ||
10:00 30mTalk | A mechanised and constructive reverse analysis of soundness and completeness of bi-intuitionistic logic CPP Pre-print | ||
09:00 - 10:30 | |||
09:00 60mKeynote | Modular Higher-Order Effects PADL | ||
10:00 30mTalk | Asynchronous Reactive Programming with Modal Types in Haskell PADL Patrick Bahr IT University of Copenhagen, Emil Houlborg IT University of Copenhagen, Gregers Thomas Skat Rørdam IT University of Copenhagen Pre-print | ||
09:00 - 10:30 | Session 1: Openning, Keynote, SAT, SMT and Automated ReasoningVMCAI at Marconi Room Chair(s): Rayna Dimitrova CISPA Helmholtz Center for Information Security | ||
09:00 5mDay opening | Opening VMCAI | ||
09:05 60mKeynote | Two Projects on Human Interaction with AI VMCAI David Harel Weizmann Institute of Science, Israel | ||
10:05 20mTalk | Interpolation and Quantifiers in Ortholattices VMCAI Sankalp Gambhir Ecole Polytechnique Federale de Lausanne (EPFL), Simon Guilloud École Polytechnique Fédérale de Lausanne, Viktor Kunčak EPFL, Switzerland | ||
09:00 - 10:30 | |||
09:00 90mTutorial | Pulse: Proof-oriented Programming in a Concurrent Separation Logic DSL in F* TutorialFest Thibault Dardinier ETH Zurich, Megan Frisella Brown University, Guido Martínez Microsoft Research, Tahina Ramananandro Microsoft Research, Aseem Rastogi Microsoft Research, Nikhil Swamy Microsoft Research | ||
09:00 - 10:30 | |||
09:00 45mTalk | What is a WebAssembly component (and why?) WAW Luke Wagner Fastly | ||
09:45 45mTalk | WALI: A thin Linux kernel interface for WebAssembly WAW Ben L. Titzer Carnegie Mellon University | ||
09:00 - 10:30 | Session 1The Future of Weak Memory at Turing Lecture Chair(s): John Wickerson Imperial College London | ||
09:00 10mTalk | 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 20mTalk | Some things I wish I hadn’t seen The Future of Weak Memory Matthew J. Parkinson Microsoft Azure Research | ||
09:30 20mTalk | Heterogeneous concurrency -- a new frontier for weak memory The Future of Weak Memory Soham Chakraborty TU Delft | ||
09:50 20mTalk | 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 20mTalk | How Do We Know That Weak Memory Matters? The Future of Weak Memory Mike Dodds Galois, Inc. File Attached | ||
10:30 - 11:00 | |||
10:30 30mCoffee break | Break Catering | ||
11:00 - 12:30 | |||
11:00 90mTutorial | Foundations of Type-Driven Probabilistic Modelling TutorialFest Ohad Kammar University of Edinburgh Pre-print | ||
11:00 - 12:30 | |||
11:00 90mTutorial | Arm Architecture and Formal Artifacts: Memory Model and Instruction Semantics TutorialFest Jade Alglave Arm and University College London, Artem Khyzha Tel Aviv University, Israel, Luc Maranget Inria, Nikos Nikoleris Arm Research, Hugo O'Keeffe ARM, Hadrien Renaud UCL | ||
11:00 - 12:30 | Compiler / Program VerificationCPP at Kelvin Lecture Chair(s): Vadim Zaliva University of Cambridge, UK | ||
11:00 30mTalk | The Last Yard: Foundational End-to-End Verification of High-Speed Cryptography CPP Philipp G. Haselwarter Aarhus University, Benjamin Salling Hvass Aarhus University, Lasse Letager Hansen Aarhus University, Théo Winterhalter INRIA Saclay, Cătălin Hriţcu MPI-SP, Bas Spitters Aarhus University Pre-print File Attached | ||
11:30 30mTalk | UTC time, formally verified CPP Ana de Almeida Borges University of Barcelona and Formal Vindications S.L., Mireia González Bedmar University of Barcelona and Formal Vindications S.L., Juan Conejero Rodríguez University of Barcelona and Formal Vindications S.L., Eduardo Hermo Reyes University of Barcelona and Formal Vindications S.L., Joaquim Casals Buñuel University of Barcelona and Formal Vindications S.L., Joost J. Joosten University of Barcelona | ||
12:00 30mTalk | VCFloat2: Floating-point error analysis in Coq CPP Pre-print | ||
11:00 - 12:30 | Knowledge Representation and LearningPADL at Lovelace Room Chair(s): Jessica Zangari Università della Calabria | ||
11:00 30mTalk | Explanation and Knowledge Acquisition in Ad Hoc Teamwork PADL | ||
11:30 30mTalk | Ontological Reasoning over Shy and Warded Datalog+/- for Streaming-based Architectures PADL Teodoro Baldazzi Università degli Studi Roma Tre, Luigi Bellomarini Banca d'Italia, Marco Favorito Banca d'Italia, Emanuel Sallinger TU Wien & University of Oxford | ||
12:00 30mTalk | FOLD-SE: An Efficient Rule-based Machine Learning Algorithm with Scalable Explainability PADL | ||
11:00 - 12:30 | Session 2: SAT, SMT and Automated ReasoningVMCAI at Marconi Room Chair(s): David Monniaux Université Grenoble Alpes - CNRS - Grenoble INP - Verimag | ||
11:00 20mTalk | Function synthesis for maximizing model counting VMCAI Thomas Vigouroux VERIMAG - UGA, Marius Bozga CNRS; Université Grenoble Alpes, Cristian Ene Verimag, Grenoble, Laurent Mounier Université Grenoble Alpes Pre-print | ||
11:20 20mTalk | Boosting Constrained Horn Solving by Unsat Core Learning VMCAI Parosh Aziz Abdulla Uppsala University, Sweden, Chencheng Liang Uppsala University, Philipp Rümmer University of Regensburg and Uppsala University | ||
11:40 20mTalk | On the Verification of a Subgraph Construction Algorithm VMCAI Lucas Böltz Univerity of Koblenz, Viorica Sofronie-Stokkermans University of Koblenz, Hannes Frey University of Koblenz | ||
12:00 20mTalk | Efficient Local Search for Nonlinear Real Arithmetic VMCAI Zhonghan Wang State Key Laboratory of Computer Science, Institute of Software, Chinese Academy of Sciences, Bohua Zhan Institute of Software, Chinese Academy of Sciences, Bohan Li State Key Laboratory of Computer Science Institute of Software, Chinese Academy of Sciences, Beijing, China, Shaowei Cai Institute of Software at Chinese Academy of Sciences | ||
11:00 - 12:30 | |||
11:00 90mTutorial | Pulse: Proof-oriented Programming in a Concurrent Separation Logic DSL in F* TutorialFest Thibault Dardinier ETH Zurich, Megan Frisella Brown University, Guido Martínez Microsoft Research, Tahina Ramananandro Microsoft Research, Aseem Rastogi Microsoft Research, Nikhil Swamy Microsoft Research | ||
11:00 - 12:30 | |||
11:00 45mTalk | RichWasm: Bringing Safe, Fine-Grained, Shared Memory Interoperability to WebAssembly WAW Amal Ahmed Northeastern University, USA | ||
11:45 45mTalk | Stack Switching in WebAssembly with Effect Handlers WAW Daniel Hillerström Huawei Zurich Research Center | ||
11:00 - 12:30 | Session 2The Future of Weak Memory at Turing Lecture Chair(s): John Wickerson Imperial College London | ||
11:00 22mTalk | Weak Memory Demands Model-based Compiler Testing The Future of Weak Memory Luke Geeson University College London (UCL) File Attached | ||
11:22 22mTalk | 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 22mTalk | What we learned from C++ atomics and memory model standardization The Future of Weak Memory Hans-J. Boehm Google File Attached | ||
12:07 22mTalk | Why Languages Should Preserve Load-Store Order The Future of Weak Memory Stephen Dolan Jane Street | ||
12:30 - 14:00 | |||
12:30 90mLunch | Lunch Catering | ||
14:00 - 15:30 | |||
14:00 90mTutorial | Verified Message-Passing Concurrency in Iris: Separation Logic Meets Session Types TutorialFest Jonas Kastberg Hinrichsen Aarhus University, Denmark, Jules Jacobs Radboud University Nijmegen, Robbert Krebbers Radboud University Nijmegen File Attached | ||
14:00 - 15:30 | |||
14:00 90mTutorial | Machine Learning Meets Program Synthesis TutorialFest Nathanaël Fijalkow CNRS, LaBRI, and Alan Turing Institute | ||
14:00 - 15:30 | |||
14:00 30mTalk | A Temporal Differential Dynamic Logic Formal Embeddingremote presentation CPP | ||
14:30 30mTalk | Formal Probabilistic Methods for Combinatorial Structures using the Lovász Local Lemmadistinguished paper CPP Pre-print | ||
15:00 30mTalk | Certification of Confluence- and Commutation-Proofs via Parallel Critical Pairs CPP Nao Hirokawa Japan Advanced Institute of Science and Technology, Dohan Kim University of Innsbruck, Kiraku Shintani Japan Advanced Institute of Science and Technology, René Thiemann University of Innsbruck | ||
14:00 - 15:30 | |||
14:00 30mTalk | Marketplace Logistic via Answer Set Programming PADL Mario Alviano University of Calabria, Danilo Amendola Oliveru - Smartly Engineering, Luis Angel Rodriguez Reiners University of Calabria | ||
14:30 30mTalk | Rethinking Answer Set Programming Templates PADL Mario Alviano University of Calabria, Giovambattista Ianni University of Calabria, Italy, Francesco Pacenza Department of Mathematics and Computer Science, University of Calabria, Jessica Zangari Università della Calabria | ||
15:00 30mTalk | A direct ASP encoding for Declare PADL Francesco Chiariello University of Naples Federico II, Valeria Fionda University of Calabria, Antonio Ielo University of Calabria, Francesco Ricca University of Calabria, Italy | ||
14:00 - 15:30 | Session 3: Security and Privacy, Model Checking and SynthesisVMCAI at Marconi Room Chair(s): Caterina Urban Inria & École Normale Supérieure | Université PSL | ||
14:00 20mTalk | Automatic and Incremental Repair for Speculative Information Leaks VMCAI Joachim Bard CISPA Helmholtz Center for Information Security, Swen Jacobs CISPA, Yakir Vizel Technion—Israel Institute of Technology | ||
14:20 20mTalk | Sound Abstract Nonexploitability Analysis VMCAI Pre-print | ||
14:40 20mTalk | Solving Two-Player Games under Progress Assumptions VMCAI Anne-Kathrin Schmuck MPI-SWS, K. S. Thejaswini The University of Warwick, Irmak Saglam Max Planck Institute for Software Systems (MPI-SWS), Satya Prakash Nayak Max Planck Institute for Software Systems (MPI-SWS) Pre-print | ||
15:00 20mTalk | Model-Guided Synthesis for LTL over Finite Traces VMCAI Shengping Xiao East China Normal University, Yongkang Li East China Normal University, Xinyue Huang East China Normal University, Yicong Xu East China Normal University, Jianwen Li East China Normal University, China, Geguang Pu East China Normal University, Ofer Strichman Technion, Moshe Vardi Rice University | ||
15:20 10mTalk | Generic Model Checking for Modal Fixpoint Logics in COOL-MC VMCAI Daniel Hausmann University of Gothenburg, Merlin Humml Friedrich-Alexander Universität Erlangen-Nürnberg, Simon Prucker Friedrich-Alexander Universität Erlangen-Nürnberg, Lutz Schröder University of Erlangen-Nuremberg, Aaron Strahlberger Friedrich-Alexander-Universität Erlangen-Nürnberg Pre-print | ||
14:00 - 15:30 | |||
14:00 90mTalk | Cedar: A language for expressing fast, safe, and fine-grained authorization policies TutorialFest Michael Hicks Amazon Web Services and the University of Maryland | ||
14:00 - 15:30 | |||
14:00 45mTalk | Mechanising WebAssembly Well? WAW Philippa Gardner Imperial College London | ||
14:45 45mTalk | Generating Executable Specification from Formal Semantics of WebAssembly WAW Sukyoung Ryu KAIST | ||
14:00 - 15:30 | |||
14:00 20mTalk | Compilers should get over themselves and respect semantic dependencies! The Future of Weak Memory | ||
14:20 20mTalk | A case against semantic dependencies The Future of Weak Memory Ori Lahav Tel Aviv University | ||
14:40 20mTalk | What Compilers desire from Weak Memory SemanticsRemote The Future of Weak Memory Akshay Gopalakrishnan McGill University File Attached | ||
15:00 20mTalk | Programmers love mind-bogglingly complicated weak memory models The Future of Weak Memory Simon Cooksey NVIDIA File Attached | ||
15:30 - 16:00 | |||
15:30 30mCoffee break | Break Catering | ||
16:00 - 17:30 | |||
16:00 90mTutorial | Verified Message-Passing Concurrency in Iris: Separation Logic Meets Session Types TutorialFest Jonas Kastberg Hinrichsen Aarhus University, Denmark, Jules Jacobs Radboud University Nijmegen, Robbert Krebbers Radboud University Nijmegen File Attached | ||
16:00 - 17:30 | |||
16:00 90mTutorial | Machine Learning Meets Program Synthesis TutorialFest Nathanaël Fijalkow CNRS, LaBRI, and Alan Turing Institute | ||
16:00 - 17:30 | Formalizing MathematicsCPP at Kelvin Lecture Chair(s): Kuen-Bang Hou (Favonia) University of Minnesota | ||
16:00 30mTalk | A Formalization of Complete Discrete Valuation Rings and Local Fields CPP María Inés de Frutos-Fernández Universidad Autónoma de Madrid, Filippo Alberto Edoardo Nuccio Mortarino Majno di Capriglio Université Jean Monnet Saint-Étienne Pre-print | ||
16:30 30mTalk | Formalizing Giles Gardam's Disproof of Kaplansky's Unit Conjecture CPP Siddhartha Gadgil Indian Institute of Science, Anand Rao Tadipatri Indian Institute of Science Education and Research | ||
17:00 30mTalk | Strictly Monotone Brouwer Trees for Well Founded Recursion Over Multiple Argumentsremote presentation CPP Joseph Eremondi University of Regina Pre-print | ||
16:00 - 17:30 | Panel DiscussionPADL at Lovelace Room Chair(s): Ekaterina Komendantskaya Heriot-Watt University and Southampton University | ||
16:00 90mPanel | Declarative Languages for Safe AI PADL P: Gopal Gupta University of Texas at Dallas, P: Wen Kokke University of Edinburgh, P: Claudia Faggian Université de Paris & CNRS, P: Alessandro Bruni IT University of Copenhagen, P: Younesse Kaddar University of Oxford | ||
16:00 - 17:30 | Session 4: Infinite State Systems, Runtime VerificationVMCAI at Marconi Room Chair(s): Helmut Seidl Technische Universität München | ||
16:00 20mTalk | Project and Conquer: Fast Quantifier Elimination for Checking Petri Nets Reachability VMCAI Pre-print | ||
16:20 20mTalk | Parameterized Verification of Disjunctive Timed NetworksRecorded VMCAI Étienne André Université Sorbonne Paris Nord; LIPN; CNRS, Paul Eichler CISPA - Helmholtz Center for Information Security, Swen Jacobs CISPA, Shyam Karra CISPA | ||
16:40 20mTalk | Resilience and Home-Space for WSTS VMCAI | ||
17:00 20mTalk | Synthesizing Efficiently Monitorable Formulas in Metric Temporal Logic VMCAI Ritam Raha University of Antwerp, Antwerp, Belgium, Rajarshi Roy Max Planck Institute for Software Systems, Kaiserslautern, Germany, Nathanaël Fijalkow CNRS, LaBRI, and Alan Turing Institute, Daniel Neider Technical University of Dortmund, Germany, Guillermo A. Perez University of Antwerp Pre-print | ||
17:20 10mTalk | TP-DejaVu: Combining Operational and Declarative Runtime Verification VMCAI Klaus Havelund NASA/Caltech Jet Propulsion Laboratory, Panagiotis Katsaros Aristotle University of Thessaloniki, Moran Omer Bar Ilan University, Israel, Doron Peled Bar Ilan University, Anastasios Temperekidis Aristotle University of Thessaloniki | ||
16:00 - 17:30 | |||
16:00 90mTalk | Cedar: A language for expressing fast, safe, and fine-grained authorization policies TutorialFest Michael Hicks Amazon Web Services and the University of Maryland | ||
16:00 - 17:30 | |||
16:00 45mTalk | A Brief Tour of Binaryen WAW Thomas Lively Google | ||
16:45 45mOther | Lightning Talks - please sign up! WAW | ||
16:00 - 17:30 | |||
16:00 22mTalk | Evolving Weak Memory Models for Evolving Architectures The Future of Weak Memory Reese Levine University of California at Santa Cruz | ||
16:22 22mTalk | In-order execution nails every weak memory behavior The Future of Weak Memory Chung-Kil Hur Seoul National University | ||
16:45 22mTalk | 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 22mTalk | Relaxed systems semantics and how we (hope to) reason above it The Future of Weak Memory | ||
17:35 - 18:30 | |||
17:35 55mMeeting | Business Meeting CPP | ||
Tue 16 JanDisplayed time zone: London change
Tue 16 Jan
Displayed time zone: London change
09:00 - 10:30 | |||
09:00 40mTalk | The state of Morello and CHERI POCL Robert N. M. Watson University of Cambridge | ||
09:45 15mTalk | The state of Morello software and projects POCL Konrad Witaszczyk University of Cambridge, UK | ||
10:00 15mTalk | The Morello ISA semantics, proof, and test generation POCL | ||
10:15 15mTalk | Morello Cerise: proving secure encapsulation (work in progress) POCL | ||
09:00 - 10:30 | |||
09:00 5mTalk | Opening PEPM | ||
09:05 60mKeynote | From Theory to Practice: Crafting Differential Privacy Systems with Haskell PEPM Alejandro Russo Chalmers University of Technology, Sweden | ||
10:05 25mTalk | Productivity Verification for Functional Programs by Reduction to Termination Verification PEPM Ren Fukaishi The University of Tokyo, Naoki Kobayashi University of Tokyo, Ryosuke Sato University of Tokyo DOI | ||
09:00 - 10:30 | |||
09:00 60mKeynote | Improved Assistance for Interactive Proof CPP Cezary Kaliszyk University of Innsbruck | ||
10:00 30mTalk | Martin-Löf à la Coqdistinguished paper CPP Arthur Adjedj ENS Paris Saclay, Université Paris-Saclay, Meven Lennon-Bertrand University of Cambridge, Kenji Maillard INRIA, Pierre-Marie Pédrot INRIA, Loïc Pujet Stockholm University | ||
09:00 - 10:30 | Declarative Programming for AIPADL at Lovelace Room Chair(s): Martin Gebser University of Klagenfurt, Austria | ||
09:00 60mKeynote | Whats and Whys of Neural Network Verification (A Declarative Programming Perspective) PADL | ||
10:00 30mTalk | Using Logic Programming and Kernel-Grouping for Improving Interpretability of Convolutional Neural Networks PADL Parth Padalkar THE UNIVERSITY OF TEXAS AT DALLAS, Huaduo Wang THE UNIVERSITY OF TEXAS AT DALLAS, Gopal Gupta University of Texas at Dallas | ||
09:00 - 10:30 | Session 5: keynote, Program and System VerificationVMCAI at Marconi Room Chair(s): Ori Lahav Tel Aviv University | ||
09:00 60mKeynote | Automating Relational Verification of Infinite-State Programs VMCAI Hiroshi Unno University of Tsukuba | ||
10:00 20mTalk | Deductive Verification of Parameterized Embedded Systems modeled in SystemC VMCAI Philip Tasche University of Twente, Raúl E. Monti University of Twente, Stefanie Eva Drerup University of Münster, Pauline Blohm Uni Münster, Paula Herber University of Munster, Germany, Marieke Huisman University of Twente | ||
10:20 10mTalk | Automatically Enforcing Rust Trait Properties VMCAI Twain Byrnes Carnegie Mellon University, Yoshiki Takashima Carnegie Mellon University, Limin Jia Carnegie Mellon University | ||
09:00 - 10:30 | |||
09:00 5mDay opening | Welcome Incorrectness | ||
09:05 60mKeynote | My Journey to the Dark Side: Under-Approximation, Incorrectness, Proof Incorrectness Peter W. O'Hearn Lacework; University College London | ||
10:05 22mTalk | A Comparison of Program Logics for (In)Correctness Incorrectness Flavio Ascari University of Pisa Pre-print File Attached | ||
09:00 - 10:30 | |||
09:00 10mDay opening | Opening PLMW @ POPL Derek Dreyer MPI-SWS | ||
09:10 35mSocial Event | Ice Breaker PLMW @ POPL | ||
09:45 45mTalk | The Evolution of Effects PLMW @ POPL Nicolas Wu Imperial College London | ||
10:30 - 11:00 | |||
10:30 - 11:00 | |||
10:30 30mCoffee break | Break Catering | ||
11:00 - 12:30 | |||
11:00 22mTalk | Compartmentalisation models POCL Dapeng Gao University of Cambridge | ||
11:22 23mTalk | Proving capability safety in the presence of indirect sentries POCL June Rousseau Aarhus University, Aina Linn Georges Max Planck Institute for Software Systems (MPI-SWS), Dominique Devriese KU Leuven, Jean Pichon-Pharabod Aarhus University, Lars Birkedal Aarhus University | ||
11:45 22mTalk | Sealed with a Library Call: Memory Allocators Should Track Capability Seal Operations POCL Jeremy Singer University of Glasgow File Attached | ||
12:08 22mTalk | Secure Calling Conventions for CHERI Capability Machines in Practice (Work in Progress) POCL Elias Storme KU Leuven, Sander Huyghebaert Vrije Universiteit Brussel, Steven Keuchel Vrije Universiteit Brussel, Thomas Van Strydonck KULeuven, Dominique Devriese KU Leuven | ||
11:00 - 12:30 | |||
11:00 25mTalk | Complete Stream Fusion for Software-Defined RadioDistinguished Paper PEPM DOI | ||
11:25 25mTalk | A Case Study in Functional Conversion and Mode Inference in miniKanren PEPM Ekaterina Verbitskaia JetBrains Research; Constructor University Bremen, Igor Engel JetBrains Research; Constructor University Bremen, Daniil Berezun JetBrains Research; Constructor University Bremen DOI | ||
11:50 25mTalk | Partial Evaluation of Reversible Flowchart Programs PEPM DOI | ||
12:15 15mTalk | Towards a Language-parametric DSL for Refactoring (Short Paper) PEPM Casper Bach Poulsen Delft University of Technology, Xulei Liu Delft University of Technology, Luka Miljak Delft University of Technology File Attached | ||
11:00 - 12:30 | Formalizations of Category TheoryCPP at Kelvin Lecture Chair(s): Robert Atkey University of Strathclyde | ||
11:00 30mTalk | Displayed Monoidal Categories for the Semantics of Linear Logic CPP Benedikt Ahrens Delft University of Technology, Ralph Matthes IRIT, Université de Toulouse, CNRS, Toulouse INP, UT3, Toulouse, Niels van der Weide Radboud University, Kobe Wullaert Delft University of Technology | ||
11:30 30mTalk | Univalent Double Categories CPP Niels van der Weide Radboud University, Nima Rasekh Max Planck Institute for Mathematics, Benedikt Ahrens Delft University of Technology, Paige Randall North Utrecht University | ||
12:00 30mTalk | Formalizing the ∞-categorical Yoneda lemma CPP Nikolai Kudasov Innopolis University, Emily Riehl Johns Hopkins University, Jonathan Weinberger Johns Hopkins University Link to publication DOI Pre-print | ||
11:00 - 12:30 | |||
11:00 30mTalk | Rhyme: A Data-Centric Expressive Query Language for Nested Data Structures PADL | ||
11:30 30mTalk | Hardware implementation of OCaml using a synchronous functional language PADL Loïc Sylvestre LIP6 - Sorbonne Université, Paris, Jocelyn Sérot Institut Pascal, Clermont-Ferrand, Emmanuel Chailloux UPMC, France | ||
12:00 30mTalk | Cutting the Cake Into Crumbs: Verifying Envy-Free Cake-Cutting Protocols using Bounded Integer Arithmetic PADL Martin Lester University of Reading | ||
11:00 - 12:30 | Second SessionPLMW @ POPL at Turing Lecture Chair(s): Leonidas Lampropoulos University of Maryland, College Park | ||
11:00 45mTalk | Refinement Types from Light to Deep Verification PLMW @ POPL Niki Vazou IMDEA Software Institute | ||
11:45 45mPanel | 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 | ||
12:30 - 14:00 | |||
12:30 90mLunch | Lunch Catering | ||
12:30 - 14:00 | |||
12:30 90mLunch | Lunch Catering | ||
14:00 - 15:30 | |||
14:00 22mTalk | Morello software and compilers POCL Jessica Clarke University of Cambridge | ||
14:22 22mTalk | CHERI C semantics POCL Vadim Zaliva University of Cambridge, UK | ||
14:45 22mTalk | CHERI static analysis POCL Irina Dudina University of Edinburgh | ||
15:07 22mTalk | ESBMC-CHERI: Towards Verification of C/C++ Programs for CHERI Platforms with ESBMC POCL Franz Brausse The University of Manchester, Kunjian Song The University of Manchester, Fedor Shmarov The University of Manchester, Rafael Menezes University of Manchester, Mikhail R. Gadelha Igalia, Konstantin Korovin University of Manchester, Giles Reger University of Manchester, Lucas C. Cordeiro University of Manchester, UK | ||
14:00 - 15:30 | |||
14:00 25mTalk | An Intrinsically Typed Compiler for Algebraic Effect Handlers PEPM Syouki Tsuyama Tokyo Institute of Technology, Youyou Cong Tokyo Institute of Technology, Hidehiko Masuhara Tokyo Institute of Technology DOI | ||
14:25 25mTalk | Ownership Types for Verification of Programs with Pointer Arithmetic PEPM Izumi Tanaka University of Tokyo, Ken Sakayori University of Tokyo, Naoki Kobayashi University of Tokyo DOI | ||
14:50 25mTalk | Scoped and Typed Staging by EvaluationRemote PEPM Guillaume Allais University of Strathclyde DOI Pre-print | ||
15:15 15mTalk | One-Pass CPS Translation of Dependent Types (Talk Proposal) PEPM Youyou Cong Tokyo Institute of Technology Pre-print | ||
14:00 - 15:30 | |||
14:00 30mTalk | Compositional Verification of Concurrent C Programs with Search Structure Templates CPP Duc-Than Nguyen University of Illinois at Chicago, Lennart Beringer Princeton University, William Mansky University of Illinois Chicago, Shengyi Wang Princeton University, USA Pre-print | ||
14:30 30mTalk | Rooting for Efficiency: Mechanised Reasoning about Array-Based Trees in Separation Logicdistinguished paper CPP Qiyuan Zhao National University of Singapore, George Pîrlea National University of Singapore, Zhendong Ang National University of Singapore, Umang Mathur National University of Singapore, Ilya Sergey National University of Singapore Pre-print | ||
15:00 30mTalk | Unification for Subformula Linking under Quantifiers CPP Pre-print | ||
14:00 - 15:30 | |||
14:00 30mTalk | Automated Interactive Domain-Specific Conversational Agents that Understand Human Dialogs PADL Yankai Zeng The University of Texas at Dallas, Abhiramon Rajasekharan The University of Texas at Dallas, Parth Padalkar THE UNIVERSITY OF TEXAS AT DALLAS, Kinjal Basu IBM, Joaquín Arias Universidad Rey Juan Carlos, Gopal Gupta University of Texas at Dallas | ||
14:30 30mTalk | Forgetting Techniques for Optimizing ASP-based Stream Reasoning PADL Francesco Calimeri University of Calabria, Giovambattista Ianni University of Calabria, Italy, Francesco Pacenza Department of Mathematics and Computer Science, University of Calabria, Simona Perri University of Calabria, Italy, Jessica Zangari Università della Calabria | ||
14:00 - 15:30 | Concurrency, Security, & Hyper-propertiesIncorrectness at Mountbatten Exhibition Chair(s): Azalea Raad Imperial College London | ||
14:00 22mTalk | Quantitative Weakest Hyper Pre Incorrectness Linpeng Zhang University College London, Benjamin Lucien Kaminski Saarland University; University College London File Attached | ||
14:22 23mTalk | A Reachability Logic for a Weak Memory Model with Promises Incorrectness Lara Bargmann University of Oldenburg, Brijesh Dongol University of Surrey, Heike Wehrheim University of Oldenburg File Attached | ||
14:45 22mTalk | Towards Temporal Adversarial Logic Incorrectness Julien Vanegue Bloomberg, USA | ||
15:07 22mTalk | Finding counterexamples to ∀∃ hyperproperties Incorrectness DOI Pre-print | ||
14:00 - 15:30 | |||
14:00 45mTalk | The Potential of Information-Flow Control Research for helping GDPR Compliance PLMW @ POPL Alejandro Russo Chalmers University of Technology, Sweden | ||
14:45 45mTalk | Consider Collaboration PLMW @ POPL | ||
15:30 - 16:00 | |||
15:30 30mCoffee break | Break Catering | ||
15:30 - 16:00 | |||
15:30 30mCoffee break | Break Catering | ||
16:00 - 17:30 | |||
16:00 22mTalk | Rust on Morello POCL Sarah Harris University of Kent, Simon Cooksey NVIDIA, Michael Vollmer University of Kent, Mark Batty University of Kent | ||
16:22 22mTalk | Capabilities for safe cross-language interoperability POCL David Chisnall SCI Semiconductor | ||
16:45 22mTalk | Concurrent Mutation must go POCL Matthew J. Parkinson Microsoft Azure Research, Sylvan Clebsch Microsoft Azure Research, Tobias Wrigstad Uppsala University, Sophia Drossopoulou Imperial College London, Elias Castegren KTH Royal Institute of Technology, Ellen Arvidsson Uppsala University, Luke Cheeseman Imperial College London | ||
17:07 22mTalk | Object Capabilities POCL Sophia Drossopoulou Imperial College London, Susan Eisenbach Imperial College London, Julian Mackay Victoria University of Wellington, James Noble Creative Research & Programming | ||
16:00 - 18:30 | History of PEPMPEPM at Haslett Room Chair(s): Fritz Henglein Department of Computer Science, University of Copenhagen (DIKU) and Deon Digital | ||
16:00 30mTalk | In memoriam Neil Deaton Jones PEPM Fritz Henglein Department of Computer Science, University of Copenhagen (DIKU) and Deon Digital DOI | ||
16:30 30mTalk | The Genesis of Mix: Early Days of Self-Applicable Partial Evaluation (Invited Contribution) PEPM DOI | ||
17:00 30mTalk | A Historical Perspective on Program Transformation and Recent Developments (Invited Contribution) PEPM Alberto Pettorossi University of Rome Tor Vergata; IASI-CNR, Maurizio Proietti IASI-CNR, Fabio Fioravanti University of Chieti-Pescara, Emanuele De Angelis IASI-CNR DOI | ||
17:30 30mTalk | Incremental Computation: What Is the Essence? (Invited Contribution)Remote PEPM Y. Annie Liu Stony Brook University DOI | ||
18:00 30mMeeting | Informal discussion on history and future of PEPM PEPM | ||
16:00 - 17:30 | |||
16:00 30mTalk | Lean Formalization of Extended Regular Expression Matching with Lookarounds CPP Ekaterina Zhuchko Tallinn University of Technology, Margus Veanes Microsoft Research, Gabriel Ebner Microsoft Research | ||
16:30 30mTalk | Memory simulations, security and optimization in a verified compiler CPP David Monniaux Université Grenoble Alpes - CNRS - Grenoble INP - Verimag | ||
17:00 30mTalk | PfComp: A Verified Compiler for Packet Filtering Leveraging Binary Decision Diagrams CPP | ||
16:00 - 17:30 | Session 8: Concurrency, Program and System Verification, ClosingVMCAI at Marconi Room Chair(s): Viktor Kunčak EPFL, Switzerland | ||
16:00 20mTalk | Petrification: Software Model Checking for Programs with Dynamic Thread Management VMCAI Matthias Heizmann University of Freiburg, Germany, Dominik Klumpp University of Freiburg, Lars Nitzke University of Freiburg, Frank Schüssele University of Freiburg Pre-print | ||
16:20 20mTalk | A Fully Verified Persistency Library VMCAI Stefan Bodenmüller University of Augsburg, John Derrick , Brijesh Dongol University of Surrey, Gerhard Schellhorn Universitaet Augsburg, Heike Wehrheim University of Oldenburg | ||
16:40 20mTalk | A Navigation Logic for Recursive Programs with Dynamic Thread Creation VMCAI Roman Lakenbrink University of Münster, Markus Müller-Olm University of Münster, Christoph Ohrem University of Münster, Jens Oliver Gutsfeld Westfälische Wilhelm-Universität Münster (WWU), Germany Pre-print | ||
17:00 20mTalk | Borrowable Fractional Ownership Types for Verification VMCAI Takashi Nakayama The University of Tokyo, Yusuke Matsushita The University of Tokyo, Ken Sakayori University of Tokyo, Ryosuke Sato University of Tokyo, Naoki Kobayashi University of Tokyo Pre-print | ||
17:20 10mDay closing | Closing (+ best paper award announcement) VMCAI | ||
16:00 - 17:30 | |||
16:00 22mTalk | Type-Based Incorrectness Reasoning Incorrectness Zhe Zhou Purdue University, Benjamin Delaware Purdue University, Suresh Jagannathan Purdue University | ||
16:23 22mTalk | Ill-Typed Programs Don't Evaluate Incorrectness | ||
16:00 - 17:30 | |||
16:00 45mTalk | How to Give a Talk PLMW @ POPL Neel Krishnaswami University of Cambridge | ||
16:45 45mTalk | Managing undergraduate research, as mentor and mentee PLMW @ POPL Mae Milano Princeton University | ||
18:00 - 21:30 | |||
18:00 3h30mSocial Event | Jane Street Board Game Night PLMW @ POPL | ||
Wed 17 JanDisplayed time zone: London change
Wed 17 Jan
Displayed time zone: London change
08:25 - 08:45 | Wednesday Morning Sessions PreviewsSession Previews at Siemens Boardroom Chair(s): Clément Pit-Claudel EPFL | ||
08:25 10mResearch preview | Synthesis 1: Session Preview Session Previews Xiaokang Qiu Purdue University | ||
08:35 10mResearch preview | Types 1: Session Preview Session Previews Niki Vazou IMDEA Software Institute | ||
08:50 - 09:00 | |||
08:50 - 09:00 | |||
09:00 - 10:00 | |||
09:00 60mTalk | A New Perspective on Commutativity in Verification POPL Azadeh Farzan University of Toronto | ||
10:00 - 10:30 | |||
10:00 30mBreak | Break (head to any of the following rooms: Riverside Room, Maxwell Room, Lovelace Room, Flowers Room, Marconi Room, Haslett Room) POPL | ||
10:05 - 10:25 | Wednesday Morning Session PreviewsSession Previews at Siemens Boardroom Chair(s): Ariel E. Kellison Cornell University | ||
10:05 10mResearch preview | Effect Handlers: Session Preview Session Previews Sam Lindley University of Edinburgh | ||
10:15 10mResearch preview | Automated Verification: Session Preview Session Previews Viktor Kunčak EPFL, Switzerland | ||
10:30 - 11:50 | |||
10:30 20mTalk | Implementation and Synthesis of Math Library FunctionsDistinguished Paper POPL | ||
10:50 20mTalk | Enhanced Enumeration Techniques for Syntax-Guided Synthesis of Bit-Vector Manipulations POPL | ||
11:10 20mTalk | Efficient Bottom-Up Synthesis for Programs with Local Variables POPL Xiang Li University of Michigan, Ann Arbor, Xiangyu Zhou University of Michigan, Rui Dong University of Michigan, Yihong Zhang University of Washington, Xinyu Wang University of Michigan Pre-print | ||
11:30 20mTalk | Optimal Program Synthesis via Abstract Interpretation POPL Stephen Mell University of Pennsylvania, Steve Zdancewic University of Pennsylvania, Osbert Bastani University of Pennsylvania | ||
10:30 - 11:50 | |||
10:30 20mTalk | 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 20mTalk | 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 20mTalk | 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 20mTalk | Ill-Typed Programs Don't Evaluate POPL | ||
11:50 - 13:20 | |||
11:50 90mLunch | URM Lunch Diversity, Equity and Inclusion | ||
11:50 - 13:20 | |||
11:50 90mLunch | Lunch (head to any of the following rooms: Riverside Room, Lovelace Room, Flowers Room, Marconi Room, Haslett Room) POPL | ||
12:50 - 13:10 | Wednesday Lunch Session PreviewsSession Previews at Siemens Boardroom Chair(s): Aurèle Barrière EPFL | ||
12:50 10mResearch preview | Automata and Complexity: Session Preview Session Previews Benjamin Lucien Kaminski Saarland University; University College London | ||
13:00 10mResearch preview | Separation Logic: Session Preview Session Previews Ralf Jung ETH Zurich | ||
13:20 - 14:40 | |||
13:20 20mTalk | Soundly Handling LinearityDistinguished Paper POPL Wenhao Tang University of Edinburgh, Daniel Hillerström Huawei Zurich Research Center, Sam Lindley University of Edinburgh, J. Garrett Morris University of Iowa DOI Pre-print | ||
13:40 20mTalk | Answer Refinement Modification: Refinement Type System for Algebraic Effects and Handlers POPL Fuga Kawamata Waseda University, Hiroshi Unno University of Tsukuba, Taro Sekiyama National Institute of Informatics, Tachio Terauchi Waseda University | ||
14:00 20mTalk | Effectful Software Contracts POPL Cameron Moy Northeastern University, Christos Dimoulas Northwestern University, Matthias Felleisen Northeastern University | ||
14:20 20mTalk | Algebraic Effects Meet Hoare Logic in Cubical Agda POPL Donnacha Oisín Kidney Imperial College London, Zhixuan Yang Imperial College London, Nicolas Wu Imperial College London Pre-print | ||
13:20 - 14:40 | |||
13:20 20mTalk | Regular Abstractions for Array Systems POPL | ||
13:40 20mTalk | An Infinite Needle in a Finite Haystack: Finding Infinite Counter-Models in Deductive VerificationDistinguished Paper POPL Link to publication DOI | ||
14:00 20mTalk | 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 20mTalk | Decision and Complexity of Dolev-Yao Hyperproperties POPL Itsaka Rakotonirina MPI-SP, Gilles Barthe MPI-SP; IMDEA Software Institute, Clara Schneidewind MPI-SP | ||
14:40 - 15:10 | |||
14:40 30mBreak | Break (head to any of the following rooms: Riverside Room, Maxwell Room, Lovelace Room, Flowers Room, Marconi Room, Haslett Room) POPL | ||
14:45 - 15:05 | Wednesday Afternoon Session PreviewsSession Previews at Siemens Boardroom Chair(s): Samantha Frohlich University of Bristol | ||
14:45 10mResearch preview | Concurrency: Session Preview Session Previews Shaz Qadeer Meta, Inc. | ||
14:55 10mResearch preview | Domain-Specific Languages: Session Preview Session Previews John Wickerson Imperial College London | ||
15:10 - 16:30 | Automata And ComplexityPOPL at Kelvin Lecture Chair(s): Fritz Henglein Department of Computer Science, University of Copenhagen (DIKU) and Deon Digital | ||
15:10 20mTalk | Parikh's Theorem Made Symbolic POPL Matthew Hague Royal Holloway University of London, Artur Jez University of Wroclaw, Anthony Widjaja Lin TU Kaiserslautern; MPI-SWS | ||
15:30 20mTalk | Efficient Matching of Regular Expressions with Lookaround Assertions POPL | ||
15:50 20mTalk | The Complex(ity) Landscape of Checking Infinite Descent POPL Liron Cohen Ben-Gurion University of the Negev, Adham Jabarin Ben Gurion University, Andrei Popescu University of Sheffield, Reuben N. S. Rowe Royal Holloway University of London | ||
16:10 20mTalk | Positive Almost-Sure Termination – Complexity and Proof Rules POPL | ||
15:10 - 16:30 | |||
15:10 20mTalk | An Iris Instance for Verifying CompCert C Programs POPL Pre-print | ||
15:30 20mTalk | 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 20mTalk | 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 20mTalk | 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:30 - 16:50 | |||
16:30 20mBreak | Break (head to any of the following rooms: Riverside Room, Maxwell Room, Lovelace Room, Flowers Room, Marconi Room, Haslett Room) POPL | ||
16:50 - 18:10 | |||
16:50 20mTalk | A Universal, Sound, and Complete Forward Reasoning Technique for Machine-Verified Proofs of Linearizability POPL Prasad Jayanti Department of Computer Science, Dartmouth College, USA, Siddhartha Jayanti Google Research, Ugur Y. Yavuz Boston University, Lizzie Hernandez Videa Microsoft | ||
17:10 20mTalk | Predictive Monitoring against Pattern Regular Languages POPL Pre-print | ||
17:30 20mTalk | Commutativity Simplifies Proofs of Parameterized Programs POPL Azadeh Farzan University of Toronto, Dominik Klumpp University of Freiburg, Andreas Podelski University of Freiburg Pre-print | ||
17:50 20mTalk | Coarser Equivalences for Causal Concurrency POPL Pre-print | ||
16:50 - 18:10 | |||
16:50 20mTalk | 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 20mTalk | A Core Calculus for Documents: Or, Lambda: The Ultimate Document POPL Pre-print | ||
17:30 20mTalk | 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 20mTalk | 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 | ||
18:10 - 20:00 | |||
18:10 1h50mSocial Event | POPL Networking Reception POPL | ||
18:10 - 20:00 | |||
18:10 1h50mSocial Event | POPL Networking Reception POPL | ||
18:15 - 20:00 | |||
18:15 4mPoster | A Denotational Approach to Release/Acquire Concurrency Student Research Competition Yotam Dvir Tel Aviv University | ||
18:19 4mTalk | A Lean Formalization of Cedar Student Research Competition Bhakti Shah University of Chicago | ||
18:24 4mTalk | A Substructural Type and Effect System Student Research Competition Orpheas van Rooij Radboud University | ||
18:29 4mPoster | A type-safe generalized editor calculus (Extended Abstract) Student Research Competition Nikolaj Rossander Kristensen Department of Computer Science, Aalborg University, Benjamin Bennetzen Department of Computer Science, Aalborg University, Peter Buus Steffensen Department of Computer Science, Aalborg University, Andreas Tor Mortensen Department of Computer Science, Aalborg University | ||
18:34 4mPoster | Compilation Quotient (CQ): A Metric for the Compilation Hardness of Programming Languages Student Research Competition Vince Szabó Delft University of Technology | ||
18:38 4mPoster | Compositional Programming with Full Iso-recursive Types Student Research Competition Litao Zhou Shanghai Jiao Tong University; University of Hong Kong | ||
18:43 4mPoster | Differential Privacy in an Impure World Student Research Competition Damián Arquez University of Chile | ||
18:48 4mPoster | Effect handlers in Zig (extended abstract) Student Research Competition Alessio Duè University of Pisa | ||
18:53 4mTalk | Efficient Incremental Computation for Halide Student Research Competition Tyler Hou University of California, Berkeley Pre-print | ||
18:57 4mTalk | Embedding Pointful Array Programming in Python Student Research Competition Jakub Bachurski University of Cambridge | ||
19:02 4mPoster | Exploring the limitations of Contextual Modal Type Theory for Multi-Stage Programming Student Research Competition Theo Wang University of Oxford | ||
19:07 4mPoster | From Java to Kotlin with Contextual Equality Saturation Student Research Competition Alexandre Drewery INRIA | ||
19:12 4mPoster | GPU-Accelerated Synthesis of Boolean Circuits Student Research Competition Justin Du University of California, San Diego, Rana Lulla University of California San Diego, Melody Ruth University of California San Diego | ||
19:17 4mTalk | HOL4P4: A Heapless Small-Step Semantics and Type System for P4 Student Research Competition Anoud Alshnakat KTH Royal Institute of Technology, Roberto Guanciale KTH Royal Institute of Technology, Mads Dam KTH | ||
19:21 4mPoster | Linking Session-Typed Channels in Separation Logic Student Research Competition Thomas Somers Radboud University | ||
19:26 4mPoster | Optimization of a Gradual Verifier: Lazy evaluation of Iso-recursive Predicates as Equi-recursive at Runtime Student Research Competition Jan-Paul Ramos-Davila Cornell University | ||
19:31 4mPoster | Optimization of the Context-Free Language Reachability Matrix-Based Algorithm Student Research Competition Ilya Muravjov Saint Petersburg State University | ||
19:36 4mPoster | PiR (πr): Probabilistic Interpretation of Robustness Student Research Competition Abhinandan Pal University of Birmingham | ||
19:40 4mTalk | Session-Typed Effect Handlers Student Research Competition Wenhao Tang University of Edinburgh | ||
19:45 4mPoster | Tail: A Typed and Structured Document Editor Student Research Competition Alperen Keles University of Maryland at College Park | ||
19:50 4mPoster | Towards programmatic reinforcement learning: the case of deterministic gridworlds Student Research Competition Guruprerana Shabadi École Polytechnique, Institut Polytechnique de Paris | ||
19:55 4mPoster | Zero-Cost Capabilities: Retrofitting Effect Safety in Rust Student Research Competition George Berdovskiy University of California, Davis | ||
Thu 18 JanDisplayed time zone: London change
Thu 18 Jan
Displayed time zone: London change
08:30 - 08:50 | |||
08:30 10mResearch preview | Synthesis 2: Session Preview Session Previews Hila Peleg Technion | ||
08:40 10mResearch preview | Higher-Order Effectful Programs: Session Preview Session Previews Andrew K. Hirsch University at Buffalo, SUNY | ||
09:00 - 10:20 | Synthesis 2POPL at Kelvin Lecture Chair(s): Michael Hicks Amazon Web Services and the University of Maryland | ||
09:00 20mTalk | Semantic Code Refactoring for Abstract Data Types POPL Shankara Pailoor University of Texas at Austin, Yuepeng Wang Simon Fraser University, Işıl Dillig University of Texas at Austin | ||
09:20 20mTalk | API-driven Program Synthesis for Testing Static Typing Implementations POPL Thodoris Sotiropoulos ETH Zurich, Stefanos Chaliasos Imperial College London, Zhendong Su ETH Zurich | ||
09:40 20mTalk | Programmatic Strategy Synthesis: Resolving Nondeterminism in Probabilistic Programs POPL Kevin Batz RWTH Aachen University, Tom Biskup RWTH Aachen University, Germany, Joost-Pieter Katoen RWTH Aachen University, Tobias Winkler RWTH Aachen University | ||
10:00 20mTalk | A Case for Synthesis of Recursive Quantum Unitary Programs POPL Haowei Deng University of Maryland at College Park, Runzhou Tao Columbia University, Yuxiang Peng University of Maryland, Xiaodi Wu University of Maryland | ||
09:00 - 10:20 | |||
09:00 20mTalk | On Model-Checking Higher-Order Effectful Programs POPL | ||
09:20 20mTalk | Explicit Effects and Effect Constraints in ReML POPL Martin Elsman University of Copenhagen, Denmark Link to publication DOI | ||
09:40 20mTalk | 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 20mTalk | 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:20 - 10:50 | |||
10:40 10mLunch | Lunch (head to any of the following rooms: Riverside Room, Lovelace Room, Flowers Room, Marconi Room, Haslett Room) POPL | ||
10:25 - 10:45 | Thursday Morning Session PreviewsSession Previews at Siemens Boardroom Chair(s): Gabriele Vanoni IRIF, Université Paris Cité | ||
10:25 10mResearch preview | Types 2: Session Preview Session Previews Richard A. Eisenberg Jane Street | ||
10:35 10mResearch preview | Probabilistic Programs: Session Preview Session Previews Jules Jacobs Radboud University Nijmegen | ||
10:50 - 12:10 | |||
10:50 20mTalk | Quotient Haskell: Lightweight Quotient Types for All POPL | ||
11:10 20mTalk | Focusing on Refinement Typing (TOPLAS)Remote POPL Dimitrios Economou Queen's University, Canada, Neel Krishnaswami University of Cambridge, Jana Dunfield Queen's University, Kingston, Ontario Link to publication | ||
11:30 20mTalk | Polymorphic Reachability Types: Tracking Freshness, Aliasing, and Separation in Higher-Order Generic ProgramsRemote POPL Guannan Wei Purdue University, Oliver Bračevac Galois, Inc., Songlin Jia Purdue University, USA, Yuyan Bao Augusta University, Tiark Rompf Purdue University | ||
11:50 20mTalk | Capturing Types (TOPLAS) POPL Aleksander Boruch-Gruszecki EPFL, Martin Odersky EPFL, Edward Lee University of Waterloo, Ondřej Lhoták University of Waterloo, Jonathan Immanuel Brachthäuser University of Tübingen DOI File Attached | ||
10:50 - 12:10 | |||
10:50 20mTalk | 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 20mTalk | 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 20mTalk | 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 20mTalk | Strong Invariants Are Hard: On the Hardness of Strongest Polynomial Invariants for (Probabilistic) Programs POPL | ||
12:10 - 13:40 | |||
12:10 90mLunch | LGBTQ+ Lunch Diversity, Equity and Inclusion | ||
12:10 - 13:40 | |||
12:10 90mLunch | Lunch (head to any of the following rooms: Riverside Room, Lovelace Room, Flowers Room, Marconi Room, Haslett Room) POPL | ||
12:10 - 13:40 | |||
12:10 90mLunch | Mentoring Lunch Diversity, Equity and Inclusion | ||
13:10 - 13:30 | Thursday Lunch Session PreviewsSession Previews at Siemens Boardroom Chair(s): Lucy Menon Northeastern University | ||
13:10 10mResearch preview | Quantum Computing: Session Preview Session Previews Oded Padon VMware Research | ||
13:20 10mResearch preview | Weak Memory and Concurrent Separation Logic: Session Preview Session Previews Mike Dodds Galois, Inc. | ||
13:40 - 15:00 | |||
13:40 20mTalk | With a Few Square Roots, Quantum Computing is as Easy as Pi POPL Jacques Carette McMaster University, Chris Heunen University of Edinburgh, Robin Kaarsgaard University of Southern Denmark, Amr Sabry Indiana University Pre-print | ||
14:00 20mTalk | Quantum Bisimilarity via Barbs and Contexts: Curbing the Power of Non-Deterministic Observers POPL Lorenzo Ceragioli IMT Lucca, Italy, Fabio Gadducci University of Pisa, Giuseppe Lomurno University of Pisa, Italy, Gabriele Tedeschi University of Pisa, Italy | ||
14:20 20mTalk | SimuQ: A Framework for Programming Quantum Hamiltonian Simulation with Analog CompilationRemote POPL Yuxiang Peng University of Maryland, Jacob Young University of Maryland, Pengyu Liu Tsinghua University, Xiaodi Wu University of Maryland | ||
14:40 20mTalk | Enriched Presheaf Model of Quantum FPC POPL | ||
15:00 - 15:30 | |||
15:00 30mBreak | Break (head to any of the following rooms: Riverside Room, Maxwell Room, Lovelace Room, Flowers Room, Marconi Room, Haslett Room) POPL | ||
15:05 - 15:25 | |||
15:05 10mResearch preview | Parallelism: Session Preview Session Previews John Reppy University of Chicago, USA | ||
15:15 10mResearch preview | Algorithmic Verification: Session Preview Session Previews Konstantinos Mamouras Rice University | ||
15:30 - 16:50 | |||
15:30 20mTalk | Pipelines and Beyond: Graph Types for ADTs with Futures POPL Francis Rinaldi Illinois Institute of Technology, june wunder Boston University, Arthur Azevedo de Amorim Rochester Institute of Technology, USA, Stefan K. Muller Illinois Institute of Technology | ||
15:50 20mTalk | Disentanglement with Futures, State, and Interaction POPL Jatin Arora Carnegie Mellon University, Stefan K. Muller Illinois Institute of Technology, Umut A. Acar Carnegie Mellon University | ||
16:10 20mTalk | DisLog: A Separation Logic for Disentanglement POPL Alexandre Moine Inria, Sam Westrick Carnegie Mellon University, Stephanie Balzer Carnegie Mellon University Pre-print | ||
16:30 20mTalk | Automatic Parallelism ManagementDistinguished Paper POPL Sam Westrick Carnegie Mellon University, Matthew Fluet Rochester Institute of Technology, Mike Rainey Carnegie Mellon University, Umut A. Acar Carnegie Mellon University | ||
15:30 - 16:50 | |||
15:30 13mTalk | Embedding Pointful Array Programming in Python Student Research Competition Jakub Bachurski University of Cambridge | ||
15:43 13mTalk | A Lean Formalization of Cedar Student Research Competition Bhakti Shah University of Chicago | ||
15:56 13mTalk | Efficient Incremental Computation for Halide Student Research Competition Tyler Hou University of California, Berkeley Pre-print | ||
16:10 13mTalk | A Substructural Type and Effect System Student Research Competition Orpheas van Rooij Radboud University | ||
16:23 13mTalk | Session-Typed Effect Handlers Student Research Competition Wenhao Tang University of Edinburgh | ||
16:36 13mTalk | HOL4P4: A Heapless Small-Step Semantics and Type System for P4 Student Research Competition Anoud Alshnakat KTH Royal Institute of Technology, Roberto Guanciale KTH Royal Institute of Technology, Mads Dam KTH | ||
15:30 - 16:50 | |||
15:30 20mTalk | Polyregular functions on unordered trees of bounded height POPL | ||
15:50 20mTalk | 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 20mTalk | 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 20mTalk | 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 | ||
16:50 - 17:10 | |||
16:50 20mBreak | Break (head to any of the following rooms: Riverside Room, Maxwell Room, Lovelace Room, Flowers Room, Marconi Room, Haslett Room) POPL | ||
17:10 - 18:20 | SIGPLAN Awards, PC Chair's Report, and Business MeetingPOPL at Kelvin Lecture Chair(s): Philippa Gardner Imperial College London | ||
17:10 70mAwards | SIGPLAN Awards, PC Chair's Report, and Business Meeting POPL | ||
18:30 - 20:00 | |||
18:30 90mSocial Event | DEI4Everyone Reception Diversity, Equity and Inclusion | ||
Fri 19 JanDisplayed time zone: London change
Fri 19 Jan
Displayed time zone: London change
08:25 - 08:45 | Friday Breakfast Session PreviewsSession Previews at Siemens Boardroom Chair(s): Xulei Liu Delft University of Technology | ||
08:25 10mResearch preview | Program Analysis: Session Preview Session Previews Roberto Giacobazzi University of Arizona | ||
08:35 10mResearch preview | Type Theory: Session Preview Session Previews Kuen-Bang Hou (Favonia) University of Minnesota | ||
08:50 - 09:00 | |||
08:50 10mOther | Extraordinary Meeting: The Publicity Chairs Reflect on the Peer-Review Process POPL | ||
08:50 - 09:00 | |||
08:50 10mOther | Extraordinary Meeting: The Publicity Chairs Reflect on the Peer-Review Process POPL | ||
09:00 - 10:00 | |||
09:00 60mTalk | The Network is the Computer: A Programming Language Perspective POPL Nate Foster Cornell University and Jane Street | ||
10:00 - 10:30 | |||
10:00 30mBreak | Break (head to any of the following rooms: Riverside Room, Maxwell Room, Lovelace Room, Flowers Room, Marconi Room, Haslett Room) POPL | ||
10:05 - 10:25 | Friday Morning Session PreviewsSession Previews at Siemens Boardroom Chair(s): Aleksander Boruch-Gruszecki EPFL | ||
10:05 10mResearch preview | Types 3: Session Preview Session Previews Nick Benton Meta | ||
10:15 10mResearch preview | Medley: Session Preview Session Previews Philip Wadler University of Edinburgh | ||
10:30 - 11:50 | |||
10:30 20mTalk | Solvable Polynomial Ideals: The Ideal Reflection for Program Analysis POPL | ||
10:50 20mTalk | On-The-Fly Static Analysis via Dynamic Bidirected Dyck Reachability POPL Shankaranarayanan Krishna IIT Bombay, India, Aniket Lal IIT Bombay, Andreas Pavlogiannis Aarhus University, Omkar Tuppe IIT Bombay | ||
11:10 20mTalk | Monotonicity and the Precision of Program Analysis POPL Marco Campion INRIA & École Normale Supérieure | Université PSL, Mila Dalla Preda University of Verona, Roberto Giacobazzi University of Arizona, Caterina Urban Inria & École Normale Supérieure | Université PSL | ||
11:30 20mTalk | Flan: An Expressive and Efficient Datalog Compiler for Program AnalysisDistinguished PaperRemote POPL Supun Abeysinghe Purdue University, Anxhelo Xhebraj Purdue University, Tiark Rompf Purdue University | ||
10:30 - 11:50 | |||
10:30 20mTalk | 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 20mTalk | Internal and Observational Parametricity for Cubical Agda POPL | ||
11:10 20mTalk | 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 20mTalk | Polynomial Time and Dependent types POPL Robert Atkey University of Strathclyde | ||
11:50 - 13:20 | |||
11:50 90mLunch | Lunch (head to any of the following rooms: Riverside Room, Lovelace Room, Flowers Room, Marconi Room, Haslett Room) POPL | ||
11:50 - 13:20 | |||
11:50 90mLunch | Women Lunch Diversity, Equity and Inclusion | ||
12:50 - 13:10 | Friday Lunch Session PreviewsSession Previews at Siemens Boardroom Chair(s): Ekaterina Zhuchko Tallinn University of Technology | ||
12:50 10mResearch preview | Machine and Automata Learning: Session Preview Session Previews Steven Holtzen Northeastern University | ||
13:00 10mResearch preview | Mechanized Proofs: Session Preview Session Previews Sandrine Blazy University of Rennes | ||
13:20 - 14:40 | |||
13:20 20mTalk | 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 20mTalk | 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 20mTalk | 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 20mTalk | Nominal Recursors as Epi-RecursorsDistinguished Paper POPL Andrei Popescu University of Sheffield | ||
14:40 - 15:10 | |||
14:40 30mBreak | Break (head to any of the following rooms: Riverside Room, Maxwell Room, Lovelace Room, Flowers Room, Marconi Room, Haslett Room) POPL | ||
14:45 - 15:05 | Friday Afternoon Session PreviewsSession Previews at Siemens Boardroom Chair(s): Paulette Koronkevich University of British Columbia | ||
14:45 10mResearch preview | Gradual Typing and Verification: Session Preview Session Previews Ronald Garcia University of British Columbia | ||
14:55 10mResearch preview | Logical Foundations: Session Preview Session Previews Emanuele D’Osualdo MPI-SWS | ||
15:10 - 16:30 | Machine and Automata LearningPOPL at Kelvin Lecture Chair(s): Steven Holtzen Northeastern University | ||
15:10 20mTalk | Efficient CHAD POPL DOI Pre-print | ||
15:30 20mTalk | ReLU Hull Approximation POPL Zhongkui Ma The University of Queensland, Jiaying LI Microsoft, Guangdong Bai The University of Queensland | ||
15:50 20mTalk | On Learning Polynomial Recursive Programs POPL Alex Buna-Marginean University of Oxford, Vincent Cheval Inria Paris, Mahsa Shirmohammadi CNRS & IRIF, Paris, James Worrell University of Oxford | ||
16:10 20mTalk | Programming-by-Demonstration for Long-Horizon Robot Tasks POPL Noah Patton The University of Texas at Austin, Kia Rahmani The University of Texas at Austin, Meghana Missula The University of Texas at Austin, Joydeep Biswas The University of Texas at Austin, Işıl Dillig University of Texas at Austin | ||
15:10 - 16:30 | |||
15:10 20mTalk | 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 20mTalk | 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 20mTalk | 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 20mTalk | A Formalization of Core Why3 in Coq POPL | ||
16:30 - 16:50 | |||
16:30 20mBreak | Break (head to any of the following rooms: Riverside Room, Maxwell Room, Lovelace Room, Flowers Room, Marconi Room, Haslett Room) POPL | ||
16:50 - 18:10 | Gradual Typing and VerificationPOPL at Kelvin Lecture Chair(s): Ronald Garcia University of British Columbia | ||
16:50 20mTalk | Securing Verified IO Programs Against Unverified Code in F* POPL Cezar-Constantin Andrici MPI-SP, Stefan Ciobaca Alexandru Ioan Cuza University of Iasi, Cătălin Hriţcu MPI-SP, Guido Martínez Microsoft Research, Exequiel Rivas Tallinn University of Technology, Éric Tanter University of Chile, Théo Winterhalter INRIA Saclay Pre-print | ||
17:10 20mTalk | Sound Gradual Verification with Symbolic Execution POPL Conrad Zimmerman Brown University, Jenna DiVincenzo (Wise) Purdue University, Jonathan Aldrich Carnegie Mellon University | ||
17:30 20mTalk | Type-based Gradual Typing Performance Optimization POPL | ||
17:50 20mTalk | Total Type Error Localization and Recovery with HolesDistinguished Paper POPL Eric Zhao University of Michigan, Raef Maroof University of Michigan, Anand Dukkipati University of Michigan, Andrew Blinn University of Michigan, Zhiyi Pan University of Michigan, Cyrus Omar University of Michigan | ||
16:50 - 17:50 | |||
16:50 20mTalk | Orthologic with Axioms POPL Pre-print | ||
17:10 20mTalk | 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 20mTalk | Calculational Design of [In]Correctness Transformational Program Logics by Abstract Interpretation POPL Patrick Cousot New York University | ||
18:10 - 18:15 | |||
18:10 - 18:15 | |||
Sat 20 JanDisplayed time zone: London change
Sat 20 Jan
Displayed time zone: London change
09:00 - 10:30 | |||
09:00 45mKeynote | Setting the stage for AI for biodiversity PROPL Drew Purves Google DeepMind | ||
09:45 45mKeynote | Building Open Source Software for Climate Change Research — Lessons Learned from Mimi.jlRemote PROPL Lisa Rennels University of California at Berkeley | ||
09:00 - 10:30 | |||
09:00 60mKeynote | Inside the Scala Capture Checker WITS Martin Odersky EPFL | ||
10:00 30mTalk | Binding Syntax for Dependently-Typed Programs WITS Andre Videla University Of Strathclyde | ||
09:00 - 10:30 | |||
09:00 5mDay opening | Introduction CoqPL | ||
09:05 60mKeynote | Melocoton: A Program Logic for Verified Interoperability Between OCaml and C (Invited Talk) CoqPL File Attached | ||
10:05 25mTalk | CertiCoq-Wasm: Verified compilation from Coq to WebAssembly CoqPL File Attached | ||
09:00 - 10:30 | |||
09:00 45mKeynote | Monoidal Adventures PLanQC Conor McBride University of Strathclyde | ||
09:45 22mTalk | Introducing BRAT PLanQC Ross Duncan Quantinuum, Mark Koch Quantinuum, Alan Lawrence Quantinuum, Conor McBride University of Strathclyde, Craig Roy Quantinuum File Attached | ||
10:07 22mTalk | Circuit Width Estimation via Effect Typing and Linear Dependency (Extended Abstract) PLanQC Andrea Colledan University of Bologna & INRIA Sophia Antipolis, Ugo Dal Lago University of Bologna & INRIA Sophia Antipolis | ||
09:00 - 10:30 | |||
09:00 45mTalk | Mechanizing Abstract Interpretation N40AI Xavier Leroy Collège de France | ||
09:45 45mTalk | Program Synthesis via Bi-directional Reduced-product Abstract Interpretation N40AI Kwangkeun Yi Seoul National University | ||
09:00 - 10:30 | |||
09:00 5mDay opening | Introduction PriSC | ||
09:05 60mKeynote | Keynote: Can we reason about the security of concurrent systems code? PriSC Peter Sewell University of Cambridge | ||
10:05 25mTalk | 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 | ||
10:30 - 11:00 | |||
10:30 30mCoffee break | Break Catering | ||
10:30 - 11:00 | |||
10:30 30mCoffee break | Break Catering | ||
10:30 - 11:00 | |||
10:30 30mCoffee break | Break Catering | ||
11:00 - 12:30 | |||
11:00 20mTalk | The programming challenges of climate data analysis PROPL Ezequiel Cimadevilla Instituto de Fisica de Cantabria | ||
11:20 20mTalk | Categorical Composition of Discrete Exterior Calculus Climate ModelsRemote PROPL Luke Morris University of Florida, George Rauta University of Florida, James Fairbanks University of Florida | ||
11:40 20mTalk | Formal Methods to Save the Earth PROPL Hongyi Huang National University of Singapore, Jialin Li National University of Singapore, Singapore, Umang Mathur National University of Singapore | ||
12:00 20mTalk | Kepler Watt Store: Kepler Software Watt Watcher StoreRemote PROPL | ||
12:20 10mOther | Discussion PROPL | ||
11:00 - 12:30 | |||
11:00 30mTalk | Retrofitting Null-Safety into Java WITS Artem Pianykh Facebook London | ||
12:00 30mTalk | Type inference for application spines WITS Simon Peyton Jones Epic Games | ||
11:00 - 12:30 | |||
11:00 90mPanel | Session with the Coq Development Team CoqPL | ||
11:00 - 12:30 | |||
11:00 22mTalk | Graphical Primitive Recursion For String Diagrams PLanQC | ||
11:22 22mTalk | Optimal compilation of parametrised quantum circuits PLanQC John van de Wetering University of Amsterdam, Richie Yeung University of Oxford, Tuomas Laakkonen Quantinuum, Aleks Kissinger University of Oxford | ||
11:45 22mTalk | Polynomial-time Classical Simulation of Roetteler’s Shifted Bent Function Algorithm PLanQC | ||
12:07 22mTalk | Qadence: a differentiable interface for digital-analog programs PLanQC Dominik Seitz PASQAL SAS, Niklas Heim PASQAL SAS, João P. Moutinho PASQAL SAS, Roland Guichard PASQAL SAS, Vytautas Abramavicius PASQAL SAS, Aleksander Wennersteen PASQAL SAS, Gert-Jan Both PASQAL SAS, Mario Dagrada PASQAL SAS, Vincent Elfving PASQAL SAS Pre-print File Attached | ||
11:00 - 12:30 | Invited Talks 2N40AI at Siemens Boardroom Chair(s): Caterina Urban Inria & École Normale Supérieure | Université PSL | ||
11:00 45mTalk | Quantum Abstract Interpretation N40AI Jens Palsberg University of California, Los Angeles (UCLA) | ||
11:45 45mTalk | Trust but Verify: Scaling Deductive Verification with Abstract Interpretation N40AI Mooly Sagiv Tel Aviv University File Attached | ||
11:00 - 12:30 | |||
11:00 22mTalk | Microarchitectural Side-Channel Mitigations for Serverless Applications PriSC File Attached | ||
11:22 22mTalk | 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 22mTalk | 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 22mTalk | 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 | ||
12:30 - 14:00 | |||
12:30 90mLunch | Lunch Catering | ||
12:30 - 14:00 | |||
12:30 - 14:00 | |||
12:30 90mLunch | Lunch Catering | ||
14:00 - 15:30 | Software engineering and ecosystemsPROPL at Flowers Room Chair(s): Michael Dales University of Cambridge, UK | ||
14:00 20mTalk | Assessing the availability, reproducibility and reuseability of research software PROPL Vashti Galpin University of Edinburgh | ||
14:20 20mTalk | Fluid: towards transparent, self-explanatory research outputs PROPL Joe Bond University of Bristol, UK, Cristina David University of Bristol, Minh Nguyen University of Bristol, Roly Perera University of Cambridge/University of Bristol Pre-print | ||
14:40 20mTalk | Toward a Live, Rich, Composable, and Collaborative Planetary Compute Engine PROPL Alexander Bandukwala Unaffiliated, Andrew Blinn University of Michigan, Cyrus Omar University of Michigan | ||
15:00 30mOther | Discussion on multidisciplinary PROPL-work PROPL | ||
14:00 - 15:30 | |||
14:00 30mTalk | On Modelling Heap Invariants for Type Systems in Dafny WITS | ||
14:30 30mTalk | Solving constraints during type inference WITS Simon Peyton Jones Epic Games | ||
15:00 30mTalk | Yaffle: A New Core for Idris 2 WITS Edwin Brady University of St Andrews, UK | ||
14:00 - 15:30 | |||
14:00 22mTalk | Well-founded recursion done right CoqPL Xavier Leroy Collège de France File Attached | ||
14:22 22mTalk | Functorial Syntax for All CoqPL File Attached | ||
14:45 22mTalk | Specifying Smart Contract with Hax and ConCert CoqPL File Attached | ||
15:07 22mTalk | A formal security analysis of Blockchain voting CoqPL Nikolaj Sidorenco Aarhus University, Laura Brædder , Lasse Letager Hansen Aarhus University, Eske Hoy Nielsen Aarhus University, Bas Spitters Aarhus University File Attached | ||
14:00 - 15:30 | New Directions for Quantum ProgrammingPLanQC at Marconi Room Chair(s): Aleks Kissinger University of Oxford | ||
14:00 22mTalk | A feasible and unitary programming language with quantum control PLanQC Alejandro Díaz-Caro ICC (UBA-CONICET) & UNQ, Emmanuel Hainry LORIA, Université de Lorraine, Romain Péchoux Université de Lorraine; CNRS; Inria; LORIA, Mário Silva LORIA, Université de Lorraine | ||
14:22 22mTalk | GUPPY: Pythonic Quantum-Classical Programming PLanQC Mark Koch Quantinuum, Alan Lawrence Quantinuum, Kartik Singhal Quantinuum, Seyon Sivarajah Quantinuum, Ross Duncan Quantinuum Media Attached File Attached | ||
14:44 22mTalk | Quantum and Classical Control (work-in-progress)remote PLanQC Kinnari Dave Université Paris-Saclay, CNRS, ENS Paris-Saclay, Inria, Laboratoire Méthodes Formelles, Louis Lemonnier Université Paris-Saclay, CNRS, ENS Paris-Saclay, Inria, Laboratoire Méthodes Formelles, Romain Péchoux Université de Lorraine; CNRS; Inria; LORIA, Vladimir Zamdzhiev Inria | ||
14:00 - 15:30 | |||
14:00 45mTalk | AI for the People N40AI Peter W. O'Hearn Lacework; University College London | ||
14:45 45mTalk | Unified Compositional Symbolic Execution N40AI Philippa Gardner Imperial College London | ||
14:00 - 15:30 | |||
14:00 22mTalk | Compiler Support for Control-Flow Linearization Using Architectural Mimicry PriSC File Attached | ||
14:22 22mTalk | 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 22mTalk | All the Binaries Together: A Semantic Approach to Application Binary Interfaces PriSC File Attached | ||
15:07 22mTalk | Short Talks PriSC | ||
15:30 - 16:00 | |||
15:30 30mCoffee break | Break Catering | ||
15:30 - 16:00 | |||
15:30 30mCoffee break | Break Catering | ||
15:30 - 16:00 | |||
15:30 30mCoffee break | Break Catering | ||
16:00 - 17:30 | Policy and decision making / BrainstormingPROPL at Flowers Room Chair(s): Vashti Galpin University of Edinburgh | ||
16:00 20mTalk | Scalable agent-based models for optimized policy design: applications to the economics of biodiversity and carbon PROPL Sharan Agrawal University of Cambridge, UK Link to publication | ||
16:20 20mTalk | Can computer science help climate policy making?Remote PROPL Nicola Botta Potsdam Institute for Climate Impact Research (PIK), Patrik Jansson Chalmers University of Technology and University of Gothenbrug | ||
16:40 50mOther | Discussion and brain storming: How can the CS/PL community help address the current planetary crises? PROPL Dominic Orchard University of Kent, UK and University of Cambridge, UK, Anil Madhavapeddy University of Cambridge, UK | ||
16:00 - 17:30 | |||
16:00 30mTalk | asai: a Library for Compiler Diagnostics WITS | ||
16:30 30mTalk | Efficient Evaluation with Controlled Definition Unfolding WITS András Kovács University of Gothenburg | ||
17:00 30mTalk | Implementing separation logic using an SMT-backed Frame RuleRemote WITS | ||
16:00 - 17:30 | |||
16:00 22mTalk | InducTeX: A MetaCoq plugin for typesetting inductive definitions CoqPL Jacco Krijnen Utrecht University File Attached | ||
16:22 22mTalk | VsCoq 2, new foundations CoqPL File Attached | ||
16:45 22mTalk | Integrating Dependency Building with Document Checking in Coq CoqPL File Attached | ||
17:07 22mTalk | A diagram editor to mechanize categorical proofs CoqPL Ambroise Lafont Ecole Polytechnique File Attached | ||
16:00 - 17:30 | |||
16:00 22mTalk | Effect Semantics for Quantum Protocols PLanQC Lorenzo Ceragioli IMT Lucca, Italy, Fabio Gadducci University of Pisa, Giuseppe Lomurno University of Pisa, Italy, Gabriele Tedeschi University of Pisa, Italy | ||
16:22 22mTalk | QbC: Quantum Correctness by Constructionremote PLanQC Pre-print | ||
16:45 22mTalk | Quantum Controlled Measurements via Program Transformation PLanQC File Attached | ||
17:07 22mTalk | QGAT: A Generate-and-Test Paradigm for Quantum Circuits PLanQC Ulrik de Muelenaere University of Notre Dame File Attached | ||
16:00 - 17:30 | |||
16:00 90mTalk | Short talks: Past, Present and Future of AI N40AI Roberto Giacobazzi University of Arizona, Eric Goubault Ecole Polytechnique, Laurent Mauborgne Absint GmbH, Dominique Mery Université de Lorraine, CNRS, INRIA / LORIA & Telecom Nancy, France, David Monniaux Université Grenoble Alpes - CNRS - Grenoble INP - Verimag, Andreas Podelski University of Freiburg, David Schmidt , Reinhard Wilhelm Saarland University | ||
16:00 - 17:30 | |||
16:00 22mTalk | 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 22mTalk | 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 DiVincenzo (Wise) Purdue University File Attached | ||
16:45 22mTalk | Towards Modular Specification and Verification of Concurrent Hypervisor-based Isolation PriSC File Attached | ||
17:07 8mDay closing | Closing Remarks PriSC Shweta Shinde ETH Zurich | ||