Filter Program
Dates
Rooms
Tracks
Badges
Your Program
This program is tentative and subject to change.
Sun 19 JanDisplayed time zone: Mountain Time (US & Canada) change
Sun 19 Jan
Displayed time zone: Mountain Time (US & Canada) change
09:00 - 10:30 | |||
09:00 10mDay opening | Day opening Dafny Stefan Zetzsche Amazon Web Services | ||
09:10 60mKeynote | Keynote Dafny K. Rustan M. Leino Amazon | ||
09:00 - 10:30 | |||
09:00 5mDay opening | Welcome LAFI | ||
09:06 20mIndustry talk | Industry Talk: Basis AI LAFI | ||
09:27 15mTalk | Towards Symbolic Execution for Probability and Non-determinism LAFI Jack Czenszak Northeastern University, John Li Northeastern University, Steven Holtzen Northeastern University | ||
09:43 15mTalk | Lazy Knowledge Compilation for Discrete PPLs LAFI Maddy Bowers Massachusetts Institute of Technology, Alexander K. Lew Massachusetts Institute of Technology, Joshua B. Tenenbaum Massachusetts Institute of Technology, Vikash K. Mansinghka Massachusetts Institute of Technology, Armando Solar-Lezama Massachusetts Institute of Technology | ||
09:59 15mTalk | Reasoning About Sampling Without Sampling: Atomic Machines for Contextual Equivalence in Probabilistic Programs LAFI Anthony D'Arienzo University of Illinois and Sandia National Laboratories, Jon Aytac Sandia National Laboratories | ||
10:15 15mTalk | Exact Inference for Nested Discrete Probabilistic Programs (Remote) LAFI File Attached | ||
09:00 - 10:30 | |||
09:00 90mTutorial | Substructural Type Systems Tutorials | ||
11:00 - 12:30 | |||
11:00 18mTalk | Helping users to reduce Brittleness in their Dafny programs - a success story Dafny | ||
11:18 18mTalk | Towards Proof Stability in SMT-based Program Verification Dafny | ||
11:36 18mTalk | Verifying the Fisher-Yates Shuffle Algorithm in Dafny Dafny Stefan Zetzsche Amazon Web Services, Tancrède Lepoint Amazon Web Services, Jean-Baptiste Tristan Amazon Web Services, Mikael Mayer Automated Reasoning Group, Amazon Web Services Pre-print | ||
11:54 18mTalk | Shipwright: A Modular Framework for Verifying Liveness of Byzantine Fault Tolerant Systems Dafny Derek Leung MIT, Nickolai Zeldovich Massachusetts Institute of Technology, USA, M. Frans Kaashoek Massachusetts Institute of Technology, USA | ||
12:12 18mTalk | Well-Behaved (Co)algebraic Semantics of Regular Expressions in Dafny Dafny | ||
11:00 - 12:30 | |||
11:00 40mTalk | Invited talk: TORAX - A Fast and Differentiable Tokamak Transport Simulator in JAX (Remote) LAFI Jonathan Citrin Google Deepmind | ||
11:41 15mTalk | Data-Parallel Differentiation by Optic Composition LAFI | ||
11:57 15mTalk | Data-oriented Design for Differentiable, Probabilistic Programming LAFI Owen Lynch University of Oxford, Maria-Nicoleta Craciun University of Oxford, Younesse Kaddar University of Oxford, Sam Staton University of Oxford | ||
12:13 15mTalk | A Domain-Specific PPL for Reasoning about Reasoning (or: a memo on memo) LAFI Kartik Chandra MIT, Tony Chen MIT, Joshua B. Tenenbaum Massachusetts Institute of Technology, Jonathan Ragan-Kelley Massachusetts Institute of Technology | ||
11:00 - 12:30 | |||
11:00 90mTutorial | Substructural Type Systems Tutorials | ||
12:30 - 14:00 | |||
12:30 90mLunch | Lunch Catering | ||
14:00 - 15:30 | |||
14:00 18mTalk | Baking for Dafny: A CakeML Backend for Dafny Dafny Daniel Nezamabadi Chalmers University of Technology and University of Gothenburg, Magnus O. Myreen Chalmers University of Technology Pre-print | ||
14:18 18mTalk | Lean on Dafny: Exploring Interactive Verification of Dafny Programs in Lean Dafny Wojciech Różowski University College London, Georges-Axel Jaloyan Amazon Web Services, Sean McLaughlin Amazon Web Services | ||
14:36 18mTalk | Performant, Readable and Interoperable Rust from Dafny Dafny Mikael Mayer Automated Reasoning Group, Amazon Web Services, Shadaj Laddad University of California at Berkeley, Fabio Madge Automated Reasoning Group, Amazon Web Services, Siva Somayyajula Amazon Web Services, Jean-Baptiste Tristan Amazon Web Services | ||
14:54 18mTalk | Randomised Testing of the Dafny Compiler: Into the CI Dafny Karnbongkot Boonriong Imperial College London, Alastair F. Donaldson Imperial College London, Stefan Zetzsche Amazon Web Services | ||
15:12 18mTalk | Teaching Types and Non-Interference in Dafny Dafny Bryan Parno Carnegie Mellon University | ||
14:00 - 15:30 | |||
14:00 40mTalk | Invited talk: Modern Bayesian Experimental Design LAFI Desi R. Ivavona University of Oxford | ||
14:41 15mTalk | Semantics of the memo Probabilistic Programming Language LAFI | ||
14:57 15mTalk | NP-NUTS: A Nonparametric No-U-Turn Sampler LAFI Maria-Nicoleta Craciun University of Oxford, C.-H. Luke Ong NTU, Sam Staton University of Oxford, Matthijs Vákár Utrecht University | ||
15:13 15mTalk | Sandwood: Runtime Adaptable Probabilistic Programming for Java (Remote) LAFI | ||
14:00 - 15:30 | |||
14:00 90mTutorial | MPL: Provably Efficient Parallel Programming Tutorials | ||
16:00 - 18:00 | |||
16:00 18mTalk | Laurel: Unblocking Automated Verification with Large Language Models Dafny Eric Mugnier University of California San Diego, Emmanuel Anaya Gonzalez UCSD, Nadia Polikarpova University of California at San Diego, Ranjit Jhala University of California at San Diego, Zhou Yuanyuan UCSD | ||
16:18 18mTalk | VerMCTS: Synthesizing Multi-Step Programs using a Verifier, a Large Language Model, and Tree Search Dafny David Brandfonbrener Harvard, Simon Henniger Technical University of Munich, Sibi Raja Harvard, Tarun Prasad Harvard, Chloe Loughridge Harvard University, Federico Cassano Northeastern University, Sabrina Ruixin Hu Harvard, Jianang Yang Million.js, William E. Byrd University of Alabama at Birmingham, USA, Robert Zinkov University of Oxford, Nada Amin Harvard University | ||
16:36 18mTalk | dafny-annotator: AI-Assisted Verification of Dafny Programs Dafny Gabriel Poesia Stanford University, Chloe Loughridge Harvard University, Nada Amin Harvard University | ||
16:54 18mTalk | Dafny as Verification-Aware Intermediate Language for Code Generation Dafny Yue Chen Li Massachusetts Institute of Technology, Stefan Zetzsche Amazon Web Services, Siva Somayyajula Amazon Web Services Pre-print | ||
17:12 18mTalk | DafnyBench: A Benchmark for Formal Software Verification Dafny Chloe Loughridge Harvard University, Qinyi Sun Massachusetts Institute of Technology, Seth Ahrenbach Beneficial AI Foundation, Federico Cassano Northeastern University, Chuyue Sun Stanford University, Ying Sheng Stanford University, Anish Mudide Massachusetts Institute of Technology, Md Rakib Hossain Misu University of California Irvine, Nada Amin Harvard University, Max Tegmark Massachusetts Institute of Technology | ||
17:30 18mTalk | Towards Neural Synthesis for SMT-Assisted Proof-Oriented Programming Dafny Saikat Chakraborty Microsoft Research, Gabriel Ebner Microsoft Research, Siddharth Bhat University of Cambridge, Sarah Fakhoury Microsoft Research, Sakina Fatima University of Ottawa, Shuvendu K. Lahiri Microsoft Research, Nikhil Swamy Microsoft Research | ||
17:48 12mDay closing | Day closing Dafny Stefan Zetzsche Amazon Web Services | ||
16:00 - 17:30 | |||
16:00 15mTalk | Partially Evaluating Higher-Order Probabilistic Programs without Stochastic Recursion to Graphical Models LAFI | ||
16:16 15mTalk | State Space Model Programming in Turing.jl LAFI Tim Hargreaves Department of Engineering, University of Cambridge, Qing Li Department of Engineering, University of Cambridge, Charles Knipp Federal Reserve Board of Governors, USA, Frederic Wantiez , Simon J. Godsill Department of Engineering, University of Cambridge, Hong Ge University of Cambridge | ||
16:32 55mOther | Poster session LAFI | ||
17:28 2mDay closing | Closing remarks LAFI Atılım Güneş Baydin University of Oxford | ||
16:00 - 17:30 | |||
16:00 90mTutorial | MPL: Provably Efficient Parallel Programming Tutorials | ||
Mon 20 JanDisplayed time zone: Mountain Time (US & Canada) change
Mon 20 Jan
Displayed time zone: Mountain Time (US & Canada) change
09:00 - 10:30 | |||
09:00 40mKeynote | Full-Stack Correctness in Wasm: Eliminating Bugs Inside and Outside the Sandbox WAW Chris Fallin F5 | ||
09:40 25mTalk | An MLIR Dialect for WebAssembly WAW Byeongjee Kang Carnegie Mellon University, Harsh Desai Carnegie Mellon University, Limin Jia Carnegie Mellon University, Brandon Lucia Carnegie Mellon University, USA | ||
10:05 25mTalk | Meta-tracing Interpreters in WebAssembly WAW | ||
09:00 - 10:30 | |||
09:00 60mKeynote | Solvers, unite! A simple unified semantics for reasoning with assurance and agreement PADL Y. Annie Liu Stony Brook University | ||
10:00 30mTalk | Enhancing a Hierarchical Graph Rewriting Language based on MELL Cut EliminationBest Student Paper –Honorable Mention PADL | ||
09:00 - 10:30 | Keynote Talk and Cyber-Physical SystemsVMCAI at Hopscotch Chair(s): Sriram Sankaranarayanan University of Colorado, Boulder | ||
09:00 60mTalk | Keynote Talk: Formal methods in a model-free, data-driven world VMCAI Jyotirmoy Deshmukh University of Southern California | ||
10:00 30mTalk | Synthesis of Controllers for Continuous Blackbox Systems VMCAI Benedikt Maderbacher Graz University of Technology, Felix Windisch Graz University of Technology, Alberto Larrauri University of Oxford, Roderick Bloem Institute of Software Technology, Graz University of Technology | ||
09:00 - 10:30 | |||
09:00 4mDay opening | Opening Remarks PriSC | ||
09:05 59mKeynote | Keynote: Bringing Verified Cryptographic Protocols to Practice PriSC Bryan Parno Carnegie Mellon University | ||
10:05 25mTalk | A Semantic Approach to Robust Property Preservation PriSC Niklas Mück MPI-SWS, Michael Sammler Institute of Science and Technology Austria, Aina Linn Georges Max Planck Institute for Software Systems (MPI-SWS), Derek Dreyer MPI-SWS, Deepak Garg MPI-SWS | ||
09:00 - 10:30 | |||
09:00 60mKeynote | Prospects for Computer Formalization of Infinite-Dimensional Category Theory CPP Emily Riehl Johns Hopkins University | ||
10:00 30mTalk | Certifying rings of integers in number fieldsdistinguished paperremote presentation CPP Anne Baanen Vrije Universiteit Amsterdam, Alain Chavarri Villarello Vrije Universiteit Amsterdam, Sander R. Dahmen Vrije Universiteit Amsterdam | ||
09:00 - 10:30 | |||
09:00 90mTutorial | Viper: An Infrastructure for Automated Verification in Separation Logic Tutorials | ||
11:00 - 12:30 | |||
11:00 40mKeynote | Removing the runtime from the TCB and other adventures in making Wasm fast and more secure WAW Deian Stefan University of California at San Diego | ||
11:40 25mTalk | A Coq Formalization of WebAssembly Execution Costs WAW John Shortt University of Ottawa | ||
12:05 25mTalk | The WebAssembly Component Model WAW | ||
11:00 - 12:30 | |||
11:00 30mTalk | Type-Checking Heterogeneous Sequences in a Simple Embeddable Type System PADL Jim Newton EPITA / LRE https://www.lre.epita.fr | ||
11:30 30mTalk | Haskell Based Spreadsheets PADL Ignacio Ballesteros IMDEA Software Institute and Universidad Politécnica de Madrid, Luis Eduardo Bueso de Barrio Universidad Politécnica de Madrid, Julio Mariño Universidad Politécnica de Madrid | ||
12:00 30mTalk | The Scenic Route to Deforestation PADL | ||
11:00 - 12:30 | |||
11:00 30mTalk | Affine Disjunctive Invariant Generation with Farkas’ Lemma VMCAI Jingyu Ke Shanghai Jiao Tong University, Hongfei Fu Shanghai Jiao Tong University, Hongming Liu Shanghai Jiao Tong University, Zhouyue Sun Shanghai Jiao Tong University, Liqian Chen National University of Defense Technology, Guoqiang Li Shanghai Jiao Tong University | ||
11:30 30mTalk | Automatic Inference of Relational Object Invariants VMCAI Yusen Su University of Waterloo, Jorge A. Navas Certora, Arie Gurfinkel University of Waterloo, Isabel Garcia-Contreras University of Waterloo | ||
12:00 30mTalk | A Static Analysis of Entanglement VMCAI Nicola Assolini University of Verona, Alessandra Di Pierro University of Verona, Isabella Mastroeni University of Verona | ||
11:00 - 12:30 | |||
11:00 25mTalk | ILA: Correctness via Type Checking for Fully Homomorphic Encryption PriSC Tarakaram Gollamudi None, Anitha Gollamudi University of Massachusetts Lowell, Joshua Gancher Northeastern University | ||
11:25 24mTalk | Leveraging Duality for Programming with zkSNARKs PriSC | ||
11:50 24mTalk | Preservation of Speculative Constant-time by Compilation PriSC Santiago Arranz Olmos Max Planck Institute for Security and Privacy, Gilles Barthe MPI-SP; IMDEA Software Institute, Lionel Blatter Max Planck Institute for Security and Privacy, Benjamin Gregoire INRIA, Vincent Laporte Inria | ||
12:15 15mTalk | Lightning talks PriSC | ||
11:00 - 12:30 | |||
11:00 30mTalk | Split Decisions: Explicit Contexts for Substructural Languagesdistinguished paper CPP Daniel Zackon McGill University, Chuta Sano McGill University, Alberto Momigliano Università degli Studi di Milano, Brigitte Pientka McGill University | ||
11:30 30mTalk | Machine Checked Proofs and Programs in Algebraic Combinatorics CPP Florent Hivert Univ. Paris-Saclay, LISN, LMF, CNRS, INRIA | ||
12:00 30mTalk | Monadic interpreters for concurrent memory models: Executable semantics of a concurrent subset of LLVM IRremote presentation CPP Nicolas Chappe Inria Lyon, LIP, Ludovic Henrio University of Lyon - ENS Lyon - UCBL - CNRS - Inria - LIP, Yannick Zakowski Inria | ||
11:00 - 12:30 | |||
11:00 90mTutorial | Viper: An Infrastructure for Automated Verification in Separation Logic Tutorials | ||
12:30 - 14:00 | |||
12:30 90mLunch | Lunch Catering | ||
14:00 - 15:30 | |||
14:00 40mKeynote | Beyond the Baseline: Experimental WebAssembly for High Performance WAW Deepti Gandluri Google | ||
14:40 25mTalk | Continuing Stack Switching in Wasmtimeremote WAW Pre-print | ||
15:05 25mTalk | Experience Report: Stack Switching in Wasm SpecTec WAW Yalun Liang Shanghai Jiao Tong University, Sam Lindley The University of Edinburgh, Andreas Rossberg Independent | ||
14:00 - 15:30 | |||
14:00 30mTalk | A practical approach to handling tabular data in logic PADL | ||
14:30 30mTalk | C3G: Causally Constrained Counterfactual Generation PADL Sopam Dasgupta , Farhad Shakerin Microsoft, Joaquín Arias Universidad Rey Juan Carlos, Elmer Salazar The University of Texas at Dallas, Gopal Gupta | ||
15:00 30mTalk | On Bridging Prolog and Python to Enhance an Inductive Logic Programming System PADL | ||
14:00 - 15:30 | |||
14:00 30mTalk | Space-Efficient Model-Checking of Higher-Order Recursion Schemes VMCAI Florian Bruse University of Kassel | ||
14:30 30mTalk | Parameterized Verification of Systems with Precise (0,1)-Counter Abstraction VMCAI Paul Eichler CISPA - Helmholtz Center for Information Security, Swen Jacobs CISPA, Chana Weil-Kennedy IMDEA Software Institute | ||
15:00 30mTalk | Property-agnostic base case extension for scalable verification of distributed systems VMCAI | ||
14:00 - 15:30 | |||
14:00 24mTalk | Auditing Rust Crates Effectively PriSC Lydia Zoghbi University of California, San Diego, David Thien University of California, San Diego, Ranjit Jhala UCSD, Deian Stefan University of California at San Diego, Caleb Stanford University of California, Davis | ||
14:25 24mTalk | Automatic Inference of Enclave Placement in LLVM Compiler PriSC Wesley B Nuzzo University of Massachusetts, Lowell (UML), Mohamed Elwakil U.S. Coast Guard Academy, Anitha Gollamudi University of Massachusetts Lowell | ||
14:50 24mTalk | Counterexamples in Safe Rust PriSC | ||
15:15 15mTalk | Lightning talks PriSC | ||
14:00 - 15:30 | |||
14:00 30mTalk | An Isabelle Formalization of Co-rewrite Pairs for Non-reachability in Term Rewriting CPP Dohan Kim University of Innsbruck, Teppei Saito Japan Advanced Institute of Science and Technology, Japan, René Thiemann University of Innsbruck, Akihisa Yamada National Institute of Informatics | ||
14:30 30mTalk | Intrinsically Correct Sorting in Cubical Agda CPP Cass Alexandru RPTU Kaiserslautern-Landau, Vikraman Choudhury Università di Bologna & Inria OLAS, Jurriaan Rot Radboud University Nijmegen, Niels van der Weide Radboud University | ||
15:00 30mTalk | Formalizing Simultaneous Critical Pairs for Confluence of Left-Linear Rewrite Systems CPP | ||
14:00 - 15:30 | |||
14:00 90mTutorial | Verification of Distributed Protocols: Decidable Modeling and Invariant Inference Tutorials | ||
16:00 - 17:30 | |||
16:00 25mTalk | A Transactions Extension for Web Assemblyremote WAW Eliot Moss University of Massachusetts at Amherst | ||
16:25 25mTalk | A Big-Step Compositional Continuation-Passing Semantics for WebAssembly WAW Guannan Wei Inria/ENS; Tufts University, Alexander Bai MPI-SWS, Dinghong Zhong Xi'an Jiaotong University, Jiatai Zhang Tufts University | ||
16:50 40mTalk | Lighting talks and closing discussion WAW Conrad Watt Nanyang Technological University | ||
16:00 - 17:30 | |||
16:00 30mTalk | MOLA: A Runtime Verification Engine Factory by (Meta-)interpreting Embedded DSLs PADL Felipe Gorostiaga IMDEA Software Institute, Martin Ceresa IMDEA Software Institute, César Sánchez IMDEA Software Institute | ||
16:30 30mTalk | Checking Concurrency Coding Rules PADL Lars-Åke Fredlund Universidad Politécnica de Madrid, Ángel Herranz Universidad Politécnica de Madrid, Julio Mariño Universidad Politécnica de Madrid | ||
17:00 10mTalk | Can Logic Programming Be Liberated from Predicates and Backtracking? (Lightning talk) PADL Michael Hanus Kiel University | ||
17:10 10mTalk | Logic Programming with Extensible Types (Lightning talk) PADL Ivan Perez NASA Ames Research Center, Miguel Angel Fernandez Bitergia, P: Julio Mariño Universidad Politécnica de Madrid | ||
16:00 - 17:30 | |||
16:00 30mTalk | ExpectAll: A BDD Based Approach for Link Failure Resilience in Elastic Optical Networks VMCAI Gustav S. Bruhns Aalborg University, Martin P. Hansen Aalborg University, Rasmus Hebsgaard Aalborg University, Frederik M. W. Hyldgaard Aalborg University, Jiri Srba Aalborg University | ||
16:30 30mTalk | Constructing Trustworthy Smart Contracts VMCAI | ||
17:00 30mTalk | Automated Flaw Detection for Industrial Robot RESTful Service VMCAI Yuncheng Wang Institute of Information Engineering, Chinese Academy of Sciences; School of Cyber Security, UCAS Beijing, China, Puzhuo Liu Tsinghua University, Yaowen Zheng Institute of Information Engineering at Chinese Academy of Sciences, Dongliang Fang Beijing Key Laboratory of IOT Information Security Technology, Institute of Information Engineering, CAS, China; School of Cyber Security, University of Chinese Academy of Sciences, China, Zhiwen Pan Institute of Information Engineering, Chinese Academy of Sciences; School of Cyber Security, UCAS Beijing, China, Shuaizong Si Institute of Information Engineering, Chinese Academy of Sciences; School of Cyber Security, UCAS Beijing, China, Weidong Zhang Institute of Information Engineering, Chinese Academy of Sciences; School of Cyber Security, UCAS Beijing, China, Limin Sun Institute of Information Engineering at Chinese Academy of Sciences; University of Chinese Academy of Sciences | ||
16:00 - 17:30 | |||
16:00 24mTalk | BeePL: Correct-by-compilation kernel extensions PriSC Swarn Priya Virginia Tech, Tim Steenvoorden Open Universiteit, Connor Sughrue Virginia Tech, Frédéric Besson Inria, Rennes, Freek Verbeek Open Universiteit & Virginia Tech | ||
16:25 24mTalk | Non-Interference Preserving and Optimising Compilation with Hyperproperty Simulations PriSC Julian Rosemann Saarland University, Saarland Informatics Campus, Sebastian Hack Saarland University, Saarland Informatics Campus, Deepak Garg MPI-SWS | ||
16:50 24mTalk | SNIP: Speculative Execution and Non-Interference Preservation for Compiler Transformations PriSC Link to publication DOI | ||
17:15 15mDay closing | Closing Remarks PriSC | ||
16:00 - 17:30 | |||
16:00 30mTalk | Formalized Burrows-Wheeler Transform CPP Louis Cheung University of Melbourne, Alistair Moffat The University of Melbourne, Christine Rizkallah University of Melbourne | ||
16:30 30mTalk | Verified and Efficient Matching of Regular Expressions with Lookaroundremote presentation CPP | ||
17:00 30mTalk | Further Tackling Post Correspondence Problem and Proof Generation CPP Akihiro Omori Department of Mathematical and Computing Science, Tokyo Institute of Technology, Yasuhiko Minamide Tokyo Institute of Technology | ||
16:00 - 17:30 | |||
16:00 90mTutorial | Verification of Distributed Protocols: Decidable Modeling and Invariant Inference Tutorials | ||
Tue 21 JanDisplayed time zone: Mountain Time (US & Canada) change
Tue 21 Jan
Displayed time zone: Mountain Time (US & Canada) change
09:00 - 10:30 | High-level abstraction and automationPEPM at Dodgeball Chair(s): Sam Lindley The University of Edinburgh | ||
09:00 10mDay opening | Welcome PEPM Y. Annie Liu Stony Brook University | ||
09:10 50mKeynote | The Missing Diagonal: High Level Languages for Low Level Systems (Invited Talk Abstract) PEPM Satnam Singh Groq | ||
10:00 30mResearch paper | A type safe calculus for generating syntax-directed editors PEPM Andreas Tor Mortensen Department of Computer Science, Aalborg University, Benjamin Bennetzen Department of Computer Science, Aalborg University, Nikolaj Rossander Kristensen Department of Computer Science, Aalborg University, Peter Buus Steffensen Department of Computer Science, Aalborg University, Hans Hüttel Department of Computer Science, Aalborg University, Sune Skaanning Engtorp Department of Computer Science, University of Copenhagen | ||
09:00 - 10:30 | |||
09:00 60mKeynote | Bridging Safety and Performance PADL Umut A. Acar Carnegie Mellon University | ||
10:00 30mTalk | SM-based Semantics for Answer Set Programs Containing Conditional Literals and ArithmeticBest student paper PADL | ||
09:00 - 10:30 | Keynote Talk (Tuesday) and LearningVMCAI at Hopscotch Chair(s): Ashutosh Trivedi University of Colorado Boulder | ||
09:00 60mTalk | Keynote Talk: Outcome Logic: a foundational framework for concurrent and probabilistic program analysis VMCAI Alexandra Silva Cornell University | ||
10:00 30mTalk | 1–2–3–Go! Policy Synthesis for Parameterized Markov Decision Processes via Decision-Tree Learning and Generalization VMCAI Muqsit Azeem Technical University of Munich, Debraj Chakraborty Masaryk University, Sudeep Kanav LMU Munich, Jan Kretinsky Masaryk University, Czech Republic, Mohammadsadegh Mohagheghi Masaryk University, Stefanie Mohr Technical University of Munich, Maximilian Weininger Institute of Science and Technology Austria | ||
09:00 - 10:30 | |||
09:00 60mKeynote | CRIS: The power of imagination in specification and verification CPP | ||
10:00 30mTalk | The Nextgen Modality: A Modality for Non-Frame-Preserving Updates in Separation Logicdistinguished paper CPP Simon Friis Vindum Aarhus University, Aina Linn Georges Max Planck Institute for Software Systems (MPI-SWS), Lars Birkedal Aarhus University | ||
09:00 - 10:30 | |||
09:00 10mDay opening | Introduction TPSA | ||
09:10 60mKeynote | Improving Static Analysis using Information Collected at RuntimeKeynote TPSA Radu Grigore Meta | ||
09:00 - 10:30 | First SessionPLMW @ POPL at Peek-A-Boo Chair(s): Leonidas Lampropoulos University of Maryland, College Park | ||
09:00 45mTalk | Getting the Most Out of POPL PLMW @ POPL Joseph W. Cutler University of Pennsylvania | ||
09:45 45mSocial Event | Icebreaker PLMW @ POPL Leonidas Lampropoulos University of Maryland, College Park | ||
09:00 - 10:30 | |||
09:00 90mTutorial | Stateless Model Checking Concurrent and Distributed Programs Tutorials | ||
11:00 - 12:30 | Language design, pedagogical tool, and staged interpreterPEPM at Dodgeball Chair(s): Michael Hanus Kiel University | ||
11:00 45mKeynote | The Ethical Compiler: Addressing the Is-Ought Gap in Compilation (Invited Talk) PEPM William J. Bowman University of British Columbia DOI Pre-print | ||
11:45 30mResearch paper | Algebraic Stepper for Simple Modules PEPM | ||
12:15 15mShort-paper | Collapsing Towers for Side-Channel Security (Short Paper) PEPM Cameron Wong Harvard SEAS, Muhammad Abdullah MIT, Yuheng Yang MIT, Mengjia Yan MIT, Adam Chlipala Massachusetts Institute of Technology, Nada Amin Harvard University File Attached | ||
11:00 - 12:30 | |||
11:00 30mTalk | ASP for Language Documentation and Reclamation: A Derivational Stemming Tool for Myaamia PADL Daniela Inclezan Miami University, USA, Hunter Lockwood Myaamia Center & Miami University, Anita Baral Miami University, Jitendra Sharma Miami University, Pratiksha Shrestha Miami University | ||
11:30 30mTalk | A Weighted Bipolar Argumentation Framework and its ASP-based Implementation PADL Yan Yan Southeast University, Nanjing, Junru Li Southeast University, Nanjing, Fangzhou Liu Southeast University, Nanjing, Zerong Wang Southeast University, Nanjing, Zhizheng Zhang Southeast University, Nanjing | ||
12:00 30mTalk | Automated Playing of Survival Video Games with Commonsense Reasoning (short paper) PADL Dan Nguyen University of Texas at Dallas, USA, Bryant Hargreaves University of Texas at Dallas, USA, Keegan Kimbrell University of Texas at Dallas, USA, Gopal Gupta | ||
11:00 - 12:30 | |||
11:00 30mTalk | A Real-Blasting Extension of Cvc5 for Reasoning about Floating-Point Arithmetic VMCAI Daisuke Ishii JAIST | ||
11:30 30mTalk | Formally Verifiable Generated ASN.1/ACN Encoders and Decoders: A Case Study VMCAI Mario Bucev EPFL, Samuel Chassot EPFL, LARA, Simon Felix Ateleris GmbH, Filip Schramka Ateleris GmbH, Viktor Kunčak EPFL, Switzerland Pre-print | ||
12:00 30mTalk | Formal Verification of Probabilistic Deep Reinforcement Learning Policies with Abstract Training VMCAI Junfeng Yang Shanghai Key Laboratory of Trustworthy Computing, East China Normal University, Junfeng Yang Shanghai Key Laboratory of Trustworthy Computing, East China Normal University, Xin Chen University of New Mexico, USA, Qin Li Shanghai Key Laboratory of Trustworthy Computing, East China Normal University | ||
11:00 - 12:30 | |||
11:00 30mTalk | Leakage-Free Probabilistic Jasmin Programs CPP Denis Firsov Tallinn University of Technology, Tiago Oliveira SandboxAQ, José Bacelar Almeira University of Minho & INESC TEC, Dominique Unruh RWTH Aachen | ||
11:30 30mTalk | Formally verified hardening of C programs against hardware fault injection CPP Basile Pesin Ecole Nationale de l'Aviation Civile (ENAC), Sylvain Boulmé Université Grenoble Alpes - CNRS - Grenoble INP - Verimag, David Monniaux CNRS, Marie-Laure Potet Univ. Grenoble Alpes, CNRS, Grenoble INP, VERIMAG Pre-print | ||
12:00 30mTalk | CertiCoq-Wasm: A verified WebAssembly backend for CertiCoqremote presentation CPP Wolfgang Meier Aarhus University, Martin Jensen Aarhus University, Jean Pichon-Pharabod Aarhus University, Bas Spitters Aarhus University Pre-print | ||
11:00 - 12:30 | |||
11:00 18mTalk | Data Structure Abstraction and Incorrectness Separation Logic TPSA Andreas Lööw Imperial College London | ||
11:18 18mTalk | Gradual Exact Logic: Unifying Hoare Logic and Incorrectness Logic via Gradual Verification TPSA Pre-print | ||
11:36 18mTalk | Partial Incorrectness Logic TPSA Lena Verscht RWTH Aachen University; Saarland University, Ānrán Wáng Saarland University, Benjamin Lucien Kaminski Saarland University; University College London | ||
11:54 18mTalk | Concurrent Quantum Separation Logic for Fine-Grained Parallelism TPSA Yusuke Matsushita Kyoto University, Kengo Hirata University of Edinburgh, Ryo Wakizaka Kyoto University | ||
12:12 18mTalk | Total Outcome Logic: Termination and Nontermination Proving for Effectful Branching TPSA James Li Cornell University, Noam Zilberstein Cornell University, Alexandra Silva Cornell University | ||
11:00 - 12:30 | |||
11:00 45mTalk | How to give a good talk PLMW @ POPL Michael Greenberg Stevens Institute of Technology | ||
11:45 45mTalk | My Journey in Secure Compilation PLMW @ POPL Cătălin Hriţcu MPI-SP Pre-print | ||
11:00 - 12:30 | |||
11:00 90mTutorial | Stateless Model Checking Concurrent and Distributed Programs Tutorials | ||
12:30 - 14:00 | |||
12:30 90mLunch | Lunch Catering | ||
12:30 - 14:00 | |||
12:30 90mMeeting | SIGPLAN SC Meeting Catering | ||
14:00 - 15:30 | |||
14:00 45mKeynote | A Type-Theoretic Framework for Certified Meta-programming (Invited Talk Extended Abstract) PEPM Brigitte Pientka McGill University | ||
14:45 30mResearch paper | Typed Program Analysis Without Encodings PEPM | ||
15:15 15mShort-paper | A Fuelled Self-Reducer for System T (Short Paper) PEPM Greg Brown University of Edinburgh File Attached | ||
14:00 - 15:30 | |||
14:00 30mTalk | Exploring Answer Set Programming for Provenance Graph-Based Cyber Threat Detection: A Novel Approach PADL | ||
14:30 30mTalk | Leveraging LLM Reasoning with Dual Horn ProgramsRECORDED PADL Paul Tarau University of North Texas | ||
15:00 30mTalk | Enhancing network diagnosis with reflection in Prolog (extended abstract)RECORDED PADL Anduo Wang Temple University, USA Pre-print | ||
14:00 - 15:30 | |||
14:00 30mTalk | Abstract Local Completeness: A Local form of Abstract Non-Interference VMCAI Isabella Mastroeni University of Verona | ||
14:30 30mTalk | An Abstract Domain for Heap Commutativity VMCAI | ||
15:00 30mTalk | Two-way collaboration between flow and proof in SPARK VMCAI | ||
14:00 - 15:30 | |||
14:00 30mTalk | Nominal Matching Logic With Fixpoints CPP | ||
14:30 30mTalk | Tactic Script Optimisation for Aesop CPP Jannis Limperg University of Munich (LMU) | ||
15:00 30mTalk | An Isabelle/HOL Framework for Synthetic Completeness Proofsremote presentation CPP Asta Halkjær From University of Copenhagen | ||
14:00 - 15:30 | |||
14:00 18mTalk | Compositional Shape Analysis with Shared Abduction and Biabductive Loop Acceleration (Extended Abstract)Remote TPSA Florian Sextl TU Wien, Austria, Adam Rogalewicz Brno University of Technology, Czechia, Tomáš Vojnar Brno University of Technology, Florian Zuleger TU Vienna Pre-print | ||
14:18 18mTalk | Calculational design of Incorrectness Separation Logic TPSA Lorenzo Gazzella Università di Pisa | ||
14:36 18mTalk | Scalable Bug Detection for Internally Unsafe Libraries: A Logical Approach to Type Refutation TPSA Pedro Carrott Imperial College London, Sacha-Élie Ayoun Imperial College London, Azalea Raad Imperial College London | ||
14:54 18mTalk | Enhancing Infer Compositional Analysis with Summary Specialization TPSA David Pichardie Meta | ||
15:12 18mTalk | Cyclic Message Histories for Automated Safety Verification of Distributed Algorithms TPSA Christian Fontenot University of Colorado Boulder, Gowtham Kaki University of Colorado at Boulder, Bor-Yuh Evan Chang University of Colorado Boulder & Amazon | ||
14:00 - 15:30 | Third SessionPLMW @ POPL at Peek-A-Boo Chair(s): Bor-Yuh Evan Chang University of Colorado Boulder & Amazon | ||
14:00 45mTalk | From operational semantics to verified compilation (and more) PLMW @ POPL Sandrine Blazy University of Rennes | ||
14:45 45mTalk | A Research Career in Balance PLMW @ POPL Andrew Myers Cornell University | ||
16:00 - 17:30 | |||
16:00 15mShort-paper | Type-Sensitive Algebraic Macros (Short Paper)Remote PEPM File Attached | ||
16:15 30mResearch paper | Characterizations of Partial Well-Behaved Lenses PEPM Keishi HASHIBA The University of Osaka, Keisuke Nakano Tohoku University, Kazuyuki Asada Tohoku University, Kentaro Kikuchi Tohoku University | ||
16:45 40mPanel | Semantics-based program manipulation in the age of LLMs PEPM William J. Bowman University of British Columbia, Brigitte Pientka McGill University, Satnam Singh Groq, Sam Lindley The University of Edinburgh | ||
17:25 5mDay closing | Farewell PEPM Y. Annie Liu Stony Brook University | ||
16:00 - 17:30 | |||
16:00 30mTalk | LLOR: Automated Repair of OpenMP Programs VMCAI Gautam Muduganti Indian Institute of Technology Hyderabad, India, Utpal Bora University of Cambridge, Saurabh Joshi Supra Research, Ramakrishna Upadrasta | ||
16:30 30mTalk | Synthesis of Parametric Locally Symmetric Protocols from Abstract Temporal Specifications VMCAI Ruoxi Zhang University of Waterloo, Richard Trefler University of Waterloo, Canada, Kedar Namjoshi Nokia Bell Labs | ||
17:00 30mTalk | Correctness Witnesses for Concurrent Programs: Bridging the Semantic Divide with Ghosts VMCAI Julian Erhard LMU Munich; TU Munich, Manuel Bentele University of Freiburg, Matthias Heizmann University of Freiburg, Germany, Dominik Klumpp University of Freiburg, Simmo Saan University of Tartu, Estonia, Frank Schüssele University of Freiburg, Michael Schwarz TU Munich, Helmut Seidl TU Munich, Sarah Tilscher Technical University of Munich, Garching, Germany, Vesal Vojdani University of Tartu Pre-print | ||
16:00 - 17:30 | |||
16:00 30mTalk | Formalization of Differential Privacy in Isabelle/HOL CPP | ||
16:30 30mTalk | A CHERI C Memory Model for Verified Temporal Safety CPP Vadim Zaliva University of Cambridge, UK, Kayvan Memarian University of Cambridge, Brian Campbell University of Edinburgh, Ricardo Almeida University of Edinburgh, Nathaniel Filardo University of Cambridge, Ian Stark The University of Edinburgh, Peter Sewell University of Cambridge | ||
17:00 30mTalk | Formalizing the One-way to Hiding Theorem CPP | ||
16:00 - 17:30 | Fourth SessionPLMW @ POPL at Peek-A-Boo Chair(s): Leonidas Lampropoulos University of Maryland, College Park | ||
16:00 45mTalk | How to Write Papers So People Can Read Them PLMW @ POPL Derek Dreyer MPI-SWS | ||
16:45 45mPanel | PLMW Panel PLMW @ POPL | ||
17:30 - 18:00 | |||
17:30 30mMeeting | Business Meeting CPP | ||
18:00 - 22:00 | Jane Street Social EventPOPL at Patty Cake Chair(s): Chris Casinghino Jane Street, Richard A. Eisenberg Jane Street | ||
18:00 4hSocial Event | Jane Street Game Night POPL | ||
19:30 - 22:00 | |||
Wed 22 JanDisplayed time zone: Mountain Time (US & Canada) change
Wed 22 Jan
Displayed time zone: Mountain Time (US & Canada) change
08:55 - 09:00 | |||
08:55 5mDay opening | Welome from the general chair POPL | ||
09:00 - 10:00 | |||
09:00 60mKeynote | Finding Good Programs by Avoiding Bad Ones POPL Loris D'Antoni UCSD | ||
10:40 - 12:00 | |||
10:40 20mTalk | Coinductive Proofs for Temporal Hyperliveness POPL Arthur Correnson CISPA Helmholtz Center for Information Security, Bernd Finkbeiner CISPA Helmholtz Center for Information Security | ||
11:00 20mTalk | Derivative-Guided Symbolic Execution POPL Yongwei Yuan Purdue University, Zhe Zhou Purdue University, Julia Belyakova Purdue University, Suresh Jagannathan Purdue University | ||
11:20 20mTalk | Symbolic Automata: omega-Regularity Modulo Theories POPL Margus Veanes Microsoft Research, Thomas Ball Microsoft Research, Gabriel Ebner Microsoft Research, Ekaterina Zhuchko Tallinn University of Technology | ||
11:40 20mTalk | Translation of Temporal Logic for Efficient Infinite-State Reactive Synthesis POPL Philippe Heim CISPA Helmholtz Center for Information Security, Rayna Dimitrova CISPA Helmholtz Center for Information Security Pre-print | ||
10:40 - 12:00 | Program AnalysisPOPL at Peek-A-Boo Chair(s): Roland Leißa University of Mannheim, School of Business Informatics and Mathematics | ||
10:40 20mTalk | Maximal Simplification of Polyhedral Reductions POPL Louis Narmour Colorado State University, University of Rennes, Inria, CNRS, IRISA, Tomofumi Yuki , Sanjay Rajopadhye Colorado State University | ||
11:00 20mTalk | Program Analysis via Multiple Context Free Language Reachability POPL Giovanna Kobus Conrado Hong Kong University of Science and Technology, Adam Husted Kjelstrøm Aarhus University, Jaco van de Pol Aarhus University, Andreas Pavlogiannis Aarhus University | ||
11:20 20mTalk | The Best of Abstract Interpretations POPL Pre-print | ||
11:40 20mTalk | An Incremental Algorithm for Algebraic Program Analysis POPL Chenyu Zhou University of Southern California, Yuzhou Fang University of Southern California, Jingbo Wang Purdue University, Chao Wang University of Southern California | ||
12:00 - 13:20 | |||
12:00 80mLunch | PLMW Steering Committee Lunch Catering | ||
12:00 - 13:20 | |||
12:00 80mLunch | Lunch Catering | ||
12:00 - 13:20 | |||
12:00 80mLunch | Mentoring Lunch Catering | ||
13:20 - 14:20 | |||
13:20 20mTalk | Linear and non-linear relational analyses for Quantum Program Optimization POPL | ||
13:40 20mTalk | Automating equational proofs in Dirac notation POPL Yingte Xu MPI-SP and Institute of Software, Chinese Academy of Sciences, Gilles Barthe MPI-SP; IMDEA Software Institute, Li Zhou Institute of Software, Chinese Academy of Sciences | ||
14:00 20mTalk | Flexible Type-Based Resource Estimation in Quantum Circuit Description Languages POPL Andrea Colledan University of Bologna & INRIA Sophia Antipolis, Ugo Dal Lago University of Bologna & INRIA Sophia Antipolis | ||
13:20 - 14:20 | |||
13:20 20mTalk | Axe 'Em: Eliminating Spurious States with Induction Axioms POPL | ||
13:40 20mTalk | A Verified Foreign Function Interface Between Coq and C POPL Joomy Korkut Bloomberg LP, Kathrin Stark Heriot-Watt University, Andrew W. Appel Princeton University | ||
14:00 20mTalk | TensorRight: Automated Verification of Tensor Graph RewritesDistinguished Paper POPL Jai Arora University of Illinois at Urbana-Champaign, Sirui Lu University of Washington, Devansh Jain University of Illinois at Urbana-Champaign, Tianfan Xu University of Illinois at Urbana-Champaign, Farzin Houshmand Google, Phitchaya Mangpo Phothilimthana Google, Mohsen Lesani University of California at Santa Cruz, Praveen Narayanan Google, Karthik Srinivasa Murthy Google, Rastislav Bodík Google Research, Brain Team, Amit Sabne Google, Charith Mendis University of Illinois at Urbana-Champaign | ||
15:00 - 16:20 | Probabilistic Programming 1POPL at Marco Polo Chair(s): Louis Narmour Colorado State University, University of Rennes, Inria, CNRS, IRISA | ||
15:00 20mTalk | A quantitative probabilistic relational Hoare logic POPL Martin Avanzini Inria, Gilles Barthe MPI-SP; IMDEA Software Institute, Benjamin Gregoire INRIA, Davide Davoli Université Côte d’Azur, Inria | ||
15:20 20mTalk | Approximate Relational Reasoning for Higher-Order Probabilistic Programs POPL Philipp G. Haselwarter Aarhus University, Kwing Hei Li Aarhus University, Alejandro Aguirre Aarhus University, Simon Oddershede Gregersen New York University, Joseph Tassarotti New York University, Lars Birkedal Aarhus University Pre-print | ||
15:40 20mTalk | Compositional imprecise probability: a solution from graded monads and Markov categories POPL | ||
16:00 20mTalk | Sound and Complete Proof Rules for Probabilistic Termination POPL | ||
15:00 - 16:20 | |||
15:00 20mTalk | Consistency of a Dependent Calculus of Indistinguishability POPL Yiyun Liu University of Pennsylvania, Jonathan Chan University of Pennsylvania, Stephanie Weirich University of Pennsylvania | ||
15:20 20mTalk | Finite-Choice Logic Programming POPL Pre-print | ||
15:40 20mTalk | Denotational Semantics of Gradual Typing using Synthetic Guarded Domain Theory POPL Eric Giovannini University of Michigan, Tingting Ding University of Michigan, Max S. New University of Michigan | ||
16:00 20mTalk | Abstract Operational Methods for Call-by-Push-Value POPL Sergey Goncharov University of Birmingham, School of Comp. Sci., Stelios Tsampas FAU Erlangen-Nuremberg, INF 8, Henning Urbat FAU Erlangen-Nuremberg, INF 8 | ||
17:00 - 18:00 | |||
17:00 20mTalk | Universal Composability is Robust Compilation POPL Marco Patrignani University of Trento, Robert Künnemann CISPA Helmholtz Center for Information Security, Riad S. Wahby Stanford University, USA, Ethan Cecchetti University of Wisconsin-Madison | ||
17:20 20mTalk | Adversities in Abstract Interpretation - Accommodating Robustness by Abstract Interpretation POPL | ||
17:40 20mTalk | Gradual C0: Symbolic Execution for Gradual Verification POPL Jenna DiVincenzo (Wise) Purdue University, Ian McCormack Carnegie Mellon University, Hemant Gouni Carnegie Mellon University, Pittsburgh, Pennsylvania, United States, Jacob Gorenburg , Jan-Paul Ramos-Davila Cornell University, Mona Zhang Columbia University, Conrad Zimmerman Northeastern University, Joshua Sunshine Carnegie Mellon University, Éric Tanter University of Chile, Jonathan Aldrich Carnegie Mellon University | ||
17:00 - 18:00 | |||
17:00 20mTalk | Formal Foundations for Translational Separation Logic Verifiers POPL Thibault Dardinier ETH Zurich, Michael Sammler Institute of Science and Technology Austria, Gaurav Parthasarathy ETH Zurich, Alexander J. Summers University of British Columbia, Peter Müller ETH Zurich | ||
17:20 20mTalk | Fulminate: Testing CN Separation-Logic Specifications in C POPL Rini Banerjee University of Cambridge, Kayvan Memarian University of Cambridge, Dhruv Makwana University of Cambridge, Christopher Pulte University of Cambridge, Neel Krishnaswami University of Cambridge, Peter Sewell University of Cambridge | ||
17:40 20mTalk | Generically Automating Separation Logic by Functors, Homomorphisms, and Modules POPL Qiyuan Xu Nanyang Technological University, David Sanan Singapore Institute of Technology, Zhe Hou Griffith University, Xiaokun Luan Peking University, Conrad Watt Nanyang Technological University, Yang Liu Nanyang Technological University | ||
18:00 - 20:00 | |||
18:00 2hSocial Event | POPL Networking Reception Catering | ||
18:00 - 20:00 | |||
18:00 2hPoster | SRC Poster Presentations Student Research Competition | ||
19:30 - 22:00 | |||
19:30 2h30mDinner | Women @ POPL Dinner Catering | ||
Thu 23 JanDisplayed time zone: Mountain Time (US & Canada) change
Thu 23 Jan
Displayed time zone: Mountain Time (US & Canada) change
10:40 - 12:00 | Probabilistic Programming 2POPL at Marco Polo Chair(s): Simon Oddershede Gregersen New York University | ||
10:40 20mTalk | Inference Plans for Hybrid Particle Filtering POPL Ellie Y. Cheng MIT, Eric Atkinson , Guillaume Baudart Inria, Louis Mandel IBM Research, USA, Michael Carbin Massachusetts Institute of Technology | ||
11:00 20mTalk | Guaranteed Bounds on Posterior Distributions of Discrete Probabilistic Programs with LoopsDistinguished Paper POPL Pre-print | ||
11:20 20mTalk | Modelling Recursion and Probabilistic Choice in Guarded Type Theory POPL Philipp Stassen Aarhus University, Rasmus Ejlers Møgelberg IT University of Copenhagen, Maaike Annebet Zwart IT University of Copenhagen, Alejandro Aguirre Aarhus University, Lars Birkedal Aarhus University | ||
11:40 20mTalk | Bluebell: An Alliance of Relational Lifting and Independence For Probabilistic Reasoning POPL Jialu Bao Cornell University, Emanuele D'Osualdo University of Konstanz, Azadeh Farzan University of Toronto Pre-print | ||
10:40 - 12:00 | |||
10:40 20mTalk | RE#: High Performance Derivative-Based Regex Matching with Intersection, Complement and Restricted Lookarounds POPL Ian Erik Varatalu Tallinn University of Technology, Estonia, Margus Veanes Microsoft Research, Juhan Ernits Tallinn University of Technology | ||
11:00 20mTalk | Pantograph: A Fluid and Typed Structure Editor POPL Jacob Prinz University of Maryland, College Park, Henry Blanchette , Leonidas Lampropoulos University of Maryland, College Park | ||
11:20 20mTalk | Grove: A Bidirectionally Typed Collaborative Structure Editor Calculus POPL Michael D. Adams National University of Singapore, Eric Griffis University of Michigan, Thomas J. Porter University of Michigan, Sundara Vishnu Satish University of Michigan - Ann Arbor, Eric Zhao Brown University, Cyrus Omar University of Michigan | ||
11:40 20mTalk | Biparsers: Exact Printing for Data Synchronisation POPL | ||
12:00 - 13:20 | |||
12:00 80mLunch | LGBTQ+ Lunch Catering | ||
12:00 - 13:20 | |||
12:00 80mLunch | Lunch Catering | ||
13:20 - 14:40 | |||
13:20 80mTalk | SRC Competition Talks Student Research Competition | ||
13:20 - 14:20 | |||
13:20 20mTalk | The Decision Problem for Regular First Order Theories POPL Umang Mathur National University of Singapore, David Mestel Maastricht University, Mahesh Viswanathan University of Illinois at Urbana-Champaign Link to publication DOI Pre-print | ||
13:40 20mTalk | A Primal-Dual Perspective on Program Verification AlgorithmsDistinguished Paper POPL Takeshi Tsukada Chiba University, Hiroshi Unno Tohoku University, Oded Padon Weizmann Institute of Science, Sharon Shoham Tel Aviv University | ||
14:00 20mTalk | Dis/Equality Graphs POPL George Zakhour University of St. Gallen, Pascal Weisenburger University of St. Gallen, Jahrim Gabriele Cesario University of St. Gallen, Guido Salvaneschi University of St. Gallen | ||
13:20 - 14:20 | |||
13:20 20mTalk | Program logics à la carte POPL Max Vistrup ETH Zurich, Michael Sammler Institute of Science and Technology Austria, Ralf Jung ETH Zurich | ||
13:40 20mTalk | On Extending Incorrectness Logic with Backwards Reasoning POPL Freek Verbeek Open Universiteit & Virginia Tech, Md Syadus Sefat Virginia Tech, Zhoulai Fu State University of New York, Korea, Binoy Ravindran Virginia Tech | ||
14:00 20mTalk | A Demonic Outcome Logic for Randomized Nondeterminism POPL Noam Zilberstein Cornell University, Dexter Kozen Cornell University, Alexandra Silva Cornell University, Joseph Tassarotti New York University | ||
15:00 - 16:20 | |||
15:00 20mTalk | A Dependent Type Theory for Meta-programming with Intensional Analysis POPL | ||
15:20 20mTalk | Avoiding signature avoidance in ML modules with zippers POPL | ||
15:40 20mTalk | Bidirectional Higher-Rank Polymorphism with Intersection and Union Types POPL | ||
16:00 20mTalk | Algebraic Temporal Effects: Temporal Verification of Recursively Typed Higher-Order Programs POPL | ||
15:00 - 16:20 | |||
15:00 20mTalk | Data Race Freedom à la ModeDistinguished Paper POPL Aina Linn Georges Max Planck Institute for Software Systems (MPI-SWS), Benjamin Peters MPI-SWS, Laila Elbeheiry MPI-SWS, Leo White Jane Street, Stephen Dolan Jane Street, Richard A. Eisenberg Jane Street, Chris Casinghino Jane Street, François Pottier Inria, Derek Dreyer MPI-SWS | ||
15:20 20mTalk | RELINCHE: Automatically Checking Linearizability under Relaxed Memory Consistency POPL | ||
15:40 20mTalk | Relaxed Memory Concurrency Re-executedDistinguished Paper POPL Evgenii Moiseenko JetBrains Research, Matteo Meluzzi TU Delft, the Netherlands, Innokentii Meleshchenko JetBrains Research, Neapolis University Pafos, Cyprus, Ivan Kabashnyi JetBrains Research, Constructor University Bremen, Germany, Anton Podkopaev JetBrains Research, Constructor University, Soham Chakraborty TU Delft | ||
16:00 20mTalk | Model Checking C/C++ with Mixed-Size Accesses POPL | ||
17:00 - 17:40 | Quantum Computing 2POPL at Marco Polo Chair(s): Jens Palsberg University of California, Los Angeles (UCLA) | ||
17:00 20mTalk | Qurts: Automatic Quantum Uncomputation by Affine Types with Lifetime POPL Pre-print | ||
17:20 20mTalk | Verifying Quantum Circuits with Level-Synchronized Tree Automata POPL Parosh Aziz Abdulla Uppsala University, Sweden, Yo-Ga Chen Academia Sinica, Yu-Fang Chen Academia Sinica, Lukáš Holík Brno University of Technology, Ondřej Lengál Brno University of Technology, Jyun-Ao Lin National Taipei University of Technology, Fang-Yi Lo Academia Sinica, Wei-Lun Tsai Academia Sinica | ||
17:00 - 17:40 | |||
17:00 20mTalk | CF-GKAT: Efficient Validation of Control-Flow Transformations POPL Cheng Zhang University College London (UCL), Tobias Kappé LIACS, Leiden University, David E. Narváez Virginia Tech, Nico Naus Open University of The Netherlands & Virginia Tech | ||
17:20 20mTalk | Algebras for Deterministic Computation are Inherently Incomplete POPL | ||
17:50 - 19:00 | |||
17:50 70mAwards | SIGPLAN Awards, PC Chair's Report, and Business Meeting POPL | ||
Fri 24 JanDisplayed time zone: Mountain Time (US & Canada) change
Fri 24 Jan
Displayed time zone: Mountain Time (US & Canada) change
09:00 - 10:00 | |||
09:00 60mTalk | Welcome to Quantum 3.0! POPL Jens Palsberg University of California, Los Angeles (UCLA) | ||
10:40 - 12:00 | Synthesis and CompilationPOPL at Marco Polo Chair(s): Alexander K. Lew Massachusetts Institute of Technology | ||
10:40 20mTalk | MimIR: An Extensible and Type-Safe Intermediate Representation for the DSL Age POPL Roland Leißa University of Mannheim, School of Business Informatics and Mathematics, Marcel Ullrich Saarland University, Joachim Meyer Compiler Design Lab; Saarland Informatics Campus; Saarland University, Sebastian Hack Saarland University, Saarland Informatics Campus | ||
11:00 20mTalk | Simple Linear Loops: Algebraic Invariants and Applications POPL Rida Ait El Manssour CNRS & IRIF, Paris, George Kenison Liverpool John Moores University, Mahsa Shirmohammadi CNRS & IRIF, Paris, Anton Varonka TU Wien | ||
11:20 20mTalk | Automated Program Refinement: Guide and Verify Code Large Language Model with Refinement Calculus POPL Yufan Cai National University of Singapore, Zhe Hou Griffith University, David Sanan Nanyang Technological University, Singapore, Xiaokun Luan Peking University, Yun Lin Shanghai Jiao Tong University, Jun Sun Singapore Management University, Jin Song Dong National University of Singapore | ||
11:40 20mTalk | Tail Modulo Cons, OCaml, and Relational Separation Logic POPL Clément Allain INRIA, Frédéric Bour Tarides, Basile Clément OCamlPro, François Pottier Inria, Gabriel Scherer Université Paris Cité - Inria - CNRS | ||
10:40 - 12:00 | |||
10:40 20mTalk | Affect: An Affine Type and Effect SystemDistinguished Paper POPL Pre-print | ||
11:00 20mTalk | A modal deconstruction of Löb induction POPL Daniel Gratzer Aarhus University | ||
11:20 20mTalk | QuickSub: Efficient Iso-Recursive Subtyping POPL | ||
11:40 20mTalk | Generic Refinement Types POPL Nico Lehmann UCSD, Cole Kurashige UCSD, Nikhil Akiti UCSD, Niroop Krishnakumar UCSD, Ranjit Jhala UCSD | ||
12:00 - 13:20 | |||
12:00 80mLunch | URM Lunch Catering | ||
12:00 - 13:20 | |||
12:00 80mLunch | Lunch Catering | ||
13:20 - 14:20 | |||
13:20 20mTalk | Archmage and CompCertCast: End-to-End Verification Supporting Integer-Pointer Casting POPL Yonghyun Kim Seoul National University, South Korea, Minki Cho Seoul National University, Jaehyung Lee Seoul National University, Jinwoo Kim Seoul National University, Taeyoung Yoon Seoul National University, Youngju Song MPI-SWS, Chung-Kil Hur Seoul National University | ||
13:40 20mResearch paper | Formalising Graph Algorithms with Coinduction POPL Pre-print | ||
14:00 20mTalk | VeriRT: An End-To-End Verification Framework for Real-Time Distributed Systems POPL Yoonseung Kim Yale University, Sung-Hwan Lee Seoul National University, Yonghyun Kim Seoul National University, South Korea, Chung-Kil Hur Seoul National University | ||
13:20 - 14:20 | |||
13:20 20mTalk | BiSikkel: A Multimode Logical Framework in Agda POPL | ||
13:40 20mTalk | Calculational Design of Hyperlogics by Abstract Interpretation POPL | ||
14:00 20mTalk | A Taxonomy of Hoare-Like Logics POPL Lena Verscht RWTH Aachen University; Saarland University, Benjamin Lucien Kaminski Saarland University; University College London | ||
15:00 - 16:20 | |||
15:00 20mTalk | Flo: a Semantic Foundation for Progressive Stream Processing POPL Shadaj Laddad University of California at Berkeley, Alvin Cheung University of California at Berkeley, Joseph M. Hellerstein UC Berkeley, Mae Milano Princeton University Pre-print | ||
15:20 20mTalk | Top-Down or Bottom-Up? Complexity Analyses of Synchronous Multiparty Session Types POPL Pre-print | ||
15:40 20mTalk | Semantic Logical Relations for Timed Message-Passing Protocols POPL Yue Yao Carnegie Mellon University, Grant Iraci University at Buffalo, Cheng-En Chuang University at Buffalo, Stephanie Balzer Carnegie Mellon University, Lukasz Ziarek University at Buffalo | ||
16:00 20mTalk | Reachability Analysis of the Domain Name System POPL | ||
15:00 - 16:20 | |||
15:00 20mTalk | The Duality of λ-Abstraction POPL | ||
15:20 20mTalk | On Decidable and Undecidable Extensions of Simply Typed Lambda Calculus POPL Naoki Kobayashi University of Tokyo | ||
15:40 20mTalk | Interaction Equivalence POPL Beniamino Accattoli Inria & Ecole Polytechnique, Adrienne Lancelot Inria, LIX Ecole Polytechnique, IRIF Université Paris Cité, Giulio Manzonetto Université Paris Cité, Gabriele Vanoni IRIF, Université Paris Cité | ||
16:00 20mTalk | Barendregt Convenes with Knaster and Tarski: Strong Rule Induction for Syntax with BindingsDistinguished Paper POPL Jan van Brügge Heriot-Watt University, James McKinna Heriot-Watt University, Andrei Popescu University of Sheffield, Dmitriy Traytel University of Copenhagen | ||
17:00 - 18:00 | |||
17:00 20mTalk | Do You Even Lift? Strengthening Compiler Security Guarantees Against Spectre Attacks POPL Xaver Fabian CISPA, Marco Patrignani University of Trento, Marco Guarnieri IMDEA Software Institute, Michael Backes Cispa Helmholtz Center for Information Security | ||
17:20 20mTalk | Preservation of speculative constant-time by compilation POPL Santiago Arranz Olmos Max Planck Institute for Security and Privacy, Gilles Barthe MPI-SP; IMDEA Software Institute, Lionel Blatter Max Planck Institute for Security and Privacy, Benjamin Gregoire INRIA, Vincent Laporte Inria | ||
17:40 20mTalk | SNIP: Speculative Execution and Non-Interference Preservation for Compiler Transformations POPL Link to publication DOI | ||
17:00 - 18:00 | |||
17:00 20mTalk | Progressful Interpreters for Efficient WebAssembly Mechanisation POPL Xiaojia Rao Imperial College London, Stefan Radziuk Imperial College London, Conrad Watt Nanyang Technological University, Philippa Gardner Imperial College London | ||
17:20 20mTalk | Unifying compositional verification and certified compilation with a three-dimensional refinement algebra POPL Yu Zhang , Jérémie Koenig Yale University, Zhong Shao Yale University, Yuting Wang Shanghai Jiao Tong University | ||
17:40 20mTalk | All Your Base Are Belong to Us: Sort Polymorphism for Proof Assistants POPL Josselin Poiret Nantes Université, Inria, Gaetan Gilbert , Kenji Maillard Inria, Pierre-Marie Pédrot INRIA, Matthieu Sozeau Inria, Nicolas Tabareau Inria, Éric Tanter University of Chile | ||
Sat 25 JanDisplayed time zone: Mountain Time (US & Canada) change
Sat 25 Jan
Displayed time zone: Mountain Time (US & Canada) change
09:00 - 10:30 | |||
09:00 60mKeynote | Invited Talk: Type inference in OCaml and GHC using Levels WITS Richard A. Eisenberg Jane Street | ||
10:00 30mTalk | Towards Generic Higher-Order Unification Implementations in HaskellRemote WITS Nikolai Kudasov Innopolis University, Artem Starikov Innopolis University, Fedor Ivanov Innopolis University, Damir Alfiatonov Innopolis University File Attached | ||
09:00 - 10:30 | |||
09:00 50mKeynote | Elpi: rule-based meta-languge for Rocq CoqPL Enrico Tassi INRIA File Attached | ||
09:50 20mTalk | Implementing OCaml APIs in Coq CoqPL Joshua M. Cohen Princeton University File Attached | ||
10:10 20mTalk | Towards general white-box automation: a typeclass-guided context cleaner CoqPL Thibaut Pérami University of Cambridge File Attached | ||
09:00 - 10:30 | |||
09:00 45mKeynote | Unlocking quantum potential with software and compilersKeynote PLanQC Kaitlin Smith Northwestern University | ||
09:46 22mTalk | HUGR: A Quantum-Classical Intermediate RepresentationTalk PLanQC Seyon Sivarajah Quantinuum, Mark Koch Quantinuum, Agustin Borgna Quantinuum, Alan Lawrence Quantinuum, Alec Edgington Quantinuum, Douglas Wilson Quantinuum, Craig Roy Quantinuum, Luca Mondada University of Oxford, Lukas Heidemann Quantinuum, Ross Duncan Quantinuum File Attached | ||
10:08 22mTalk | QuteFuzz: Fuzzing quantum compilers using randomly generated circuits with control flow and subcircuitsTalk PLanQC Ilan Iwumbwe Imperial College London, Benny Zong Liu Imperial College London, John Wickerson Imperial College London Media Attached File Attached | ||
11:00 - 12:30 | |||
11:00 30mTalk | Towards Generic Type Checking Implementations in Haskell via Second-Order Abstract SyntaxRemote WITS Nikolai Kudasov Innopolis University, Anastasia Smirnova Innopolis University, Vladislav Deryabkin Innopolis University, Diana Tomilovskaia Innopolis University, Ekaterina Maksimova Innopolis University File Attached | ||
11:30 30mTalk | McTT: Building A Correct-By-Construction Proof Checker For Martin-Loef Type Theory WITS Junyoung Jang McGill University, Jason Z.S. Hu Amazon Web Services, USA, Antoine Gaulin McGill University, Brigitte Pientka McGill University Pre-print File Attached | ||
12:00 30mTalk | Eta conversion for the unit type (is still not that simple)Remote WITS András Kovács University of Gothenburg and Chalmers University of Technology File Attached | ||
11:00 - 12:30 | |||
11:00 70mPanel | Session with the Coq Development Team CoqPL | ||
12:10 20mTalk | Vellvm: Formalizing the Informal CoqPL Calvin Beck University of Pennsylvania, USA, Hanxi Chen , Steve Zdancewic University of Pennsylvania File Attached | ||
11:00 - 12:30 | |||
11:00 22mTalk | The Quantum Abstract MachineTalk PLanQC Le Chang University of Maryland, College Park, Liyi Li Iowa State University, Rance Cleaveland University of Maryland, Mingwei Zhu University of Maryland, College Park, Xiaodi Wu University of Maryland File Attached | ||
11:22 22mTalk | Algebraic and denotational semantics for Classically Controlled Quantum CommunicationTalk PLanQC File Attached | ||
11:45 22mTalk | Towards Quantum Multiparty Session TypesTalk PLanQC Ivan Lanese University of Bologna/INRIA, Ugo Dal Lago University of Bologna & INRIA Sophia Antipolis, Vikraman Choudhury Università di Bologna & Inria OLAS File Attached | ||
12:07 22mTalk | Concurrent Quantum Separation Logic for Fine-Grained ParallelismTalk PLanQC Yusuke Matsushita Kyoto University, Kengo Hirata University of Edinburgh, Ryo Wakizaka Kyoto University File Attached | ||
12:30 - 14:00 | |||
12:30 90mLunch | Lunch Catering | ||
14:00 - 15:30 | |||
14:00 30mOther | Collaboration Time 1 WITS | ||
14:30 30mTalk | Semantic Analysis of Normalisation for Directional Logic ProgrammingRemote WITS Vikraman Choudhury Università di Bologna & Inria OLAS, Neel Krishnaswami University of Cambridge, Ariadne Si Suo University of Cambridge File Attached | ||
15:00 30mTalk | Incremental Bidirectional Typing via Order Maintenance WITS Thomas J. Porter University of Michigan, Marisa Kirisame University of Utah, Liam Mulcahy University of Michigan, Pavel Panchekha University of Utah, Cyrus Omar University of Michigan File Attached | ||
14:00 - 15:30 | |||
14:00 22mTalk | Towards Verified Linear Algebra Programs Through Equivalence CoqPL Yihan Yang Harvey Mudd College, Mohit Tekriwal Lawrence Livermore National Laboratory, John Sarracino Lawrence Livermore National Laboratory, Matthew Sottile Lawrence Livermore National Laboratory, Ignacio Laguna Lawrence Livermore National Laboratory File Attached | ||
14:22 22mTalk | A Framework of Differential Operators CoqPL File Attached | ||
14:45 22mTalk | A Semantic Logical Relation for Termination of Intuitionistic Linear Logic Session Types CoqPL Tarakaram Gollamudi None, Jules Jacobs Cornell University, Yue Yao Carnegie Mellon University, Stephanie Balzer Carnegie Mellon University File Attached | ||
15:07 22mTalk | Formal Verification of a Software Defined Delay-Tolerant Network CoqPL Jan-Paul Ramos-Davila Cornell University File Attached | ||
14:00 - 15:30 | |||
14:00 22mTalk | Verifying the Equivalence of Parameterized Quantum CircuitsTalk PLanQC File Attached | ||
14:22 22mTalk | An Automata-based Framework for Quantum Circuit VerificationTalk PLanQC Parosh Aziz Abdulla Uppsala University, Sweden, Yo-Ga Chen Academia Sinica, Yu-Fang Chen Academia Sinica, Kai-Min Chung Academia Sinica, Lukáš Holík Brno University of Technology, Ondřej Lengál Brno University of Technology, Jyun-Ao Lin National Taipei University of Technology, Fang-Yi Lo Academia Sinica, Wei-Lun Tsai Academia Sinica, Di-De Yen Academia Sinica File Attached | ||
14:45 45mPoster | Poster Session PLanQC | ||
16:00 - 17:30 | |||
16:00 30mOther | Collaboration Time 2 WITS | ||
16:30 30mTalk | Formalizing locally nameless syntax with cofinite quantification WITS Elif Uskuplu Indiana University, Bloomington File Attached | ||
17:00 30mOther | Closing WITS | ||
16:00 - 17:30 | |||
16:00 22mTalk | Towards Automated Verification of LLM-Synthesized C Programs CoqPL File Attached | ||
16:22 22mTalk | Towards Mining Robust Coq Proof Patterns CoqPL Cezary Kaliszyk University of Melbourne, Xuan-Bach D. Le University of Melbourne, Christine Rizkallah University of Melbourne File Attached | ||
16:45 22mTalk | CoqNFU: Towards Formalizing NFU in Coq CoqPL File Attached | ||
17:07 22mTalk | Formal Verification of Quantum Stabilizer Code CoqPL File Attached | ||
16:00 - 17:30 | |||
16:00 22mTalk | Quantum Register Machine: Efficient Implementation of Quantum Recursive Programs (Extended Abstract)TalkRemote PLanQC Zhicheng Zhang University of Technology Sydney, Mingsheng Ying Institute of Software at Chinese Academy of Sciences; Tsinghua University File Attached | ||
16:22 22mTalk | Programming with Projective CliffordsTalk PLanQC File Attached | ||
16:45 22mTalk | Proto-Quipper with Reversing and ControlTalk PLanQC Peng Fu University of South Carolina, Kohei Kishida University of Illinois at Urbana-Champaign, Neil Julien Ross Dalhousie University, Peter Selinger Dalhousie University File Attached | ||
17:07 22mTalk | Imperative Quantum Programming with Ownership and Borrowing in GuppyTalk PLanQC Mark Koch Quantinuum, Agustin Borgna Quantinuum, Craig Roy Quantinuum, Alan Lawrence Quantinuum, Kartik Singhal Quantinuum, Seyon Sivarajah Quantinuum, Ross Duncan Quantinuum Media Attached File Attached | ||