Filter Program
Dates
Rooms
Tracks
Badges
Your Program
This program is tentative and subject to change.
Sun 11 JanDisplayed time zone: Brussels, Copenhagen, Madrid, Paris change
Sun 11 Jan
Displayed time zone: Brussels, Copenhagen, Madrid, Paris change
09:00 - 10:30 | |||
09:00 12mDay opening | Day opening Dafny | ||
09:12 60mKeynote | Software Verification meets Real-World Cryptography Dafny Karthikeyan Bhargavan Cryspen, France | ||
10:12 18mTalk | The Design of an Interactive Proof Mode for Dafny Dafny Ștefan Ciobâcă Alexandru Ioan Cuza University of Iasi, K. Rustan M. Leino Amazon, Ștefan Mercaș Alexandru Ioan Cuza University, Iasi, Romania, Roxana-Mihaela Timon Alexandru Ioan Cuza University, Iasi, Romania | ||
09:00 - 10:30 | |||
09:00 90mTutorial | Creusot: Formal verification of Rust programs Tutorials Li-yao Xia LMF, Inria, Université Paris-Saclay, Jacques-Henri Jourdan CNR, LMF, Arnaud Golfouse Université Paris-Saclay, CNRS, ENS Paris-Saclay, Inria, Laboratoire des méthodes formelles, 91190, Gif-sur-Yvette, France, Vincent Lafeychine Université Paris-Saclay | ||
09:00 - 10:30 | |||
09:00 90mTutorial | BINSEC: Adapting Symbolic Execution for Binary-level Security Tutorials Sébastien Bardin CEA LIST, University Paris-Saclay, Frédéric Recoules CEA, List, Yanis Sellami CEA, List, Univ. Grenoble Alpes | ||
09:00 - 10:00 | |||
09:00 20mDay opening | Day opening PriSC | ||
09:20 20mKeynote | The V8 Sandbox: From Compiler Correctness to Runtime Containment PriSC Samuel Groß Google | ||
09:40 20mTalk | Efficient Dependency Resolution in IFC-aware Decentralized Programming PriSC | ||
11:00 - 12:30 | |||
11:00 18mTalk | Diagnostics in Probabilistic Program Verification Dafny Philipp Schröer RWTH Aachen University, Darion Haase RWTH Aachen University, Joost-Pieter Katoen RWTH Aachen University | ||
11:18 18mTalk | Explicit Abstraction Barrier for Autoactive Verification Dafny Paul Patault Université Paris-Saclay - Laboratoire de Méthodes Formelles Pre-print | ||
11:36 18mTalk | Managing the Proof Context in SPARK Dafny | ||
11:54 18mTalk | Tunable Automation in Automated Program Verification Dafny Alexander Bai New York University, Chris Hawblitzel Microsoft Research, Andrea Lattuada VMware Research | ||
12:12 18mTalk | Velvet: A Multi-Modal Verifier for Effectful Programs Dafny Vladimir Gladshtein , George Pîrlea National University of Singapore, Qiyuan Zhao National University of Singapore, Vitaly Kurin Neapolis University Pafos, Ilya Sergey National University of Singapore Pre-print | ||
11:00 - 12:30 | |||
11:00 90mTutorial | Creusot: Formal verification of Rust programs Tutorials Li-yao Xia LMF, Inria, Université Paris-Saclay, Jacques-Henri Jourdan CNR, LMF, Arnaud Golfouse Université Paris-Saclay, CNRS, ENS Paris-Saclay, Inria, Laboratoire des méthodes formelles, 91190, Gif-sur-Yvette, France, Vincent Lafeychine Université Paris-Saclay | ||
11:00 - 12:30 | |||
11:00 90mTutorial | BINSEC: Adapting Symbolic Execution for Binary-level Security Tutorials Sébastien Bardin CEA LIST, University Paris-Saclay, Frédéric Recoules CEA, List, Yanis Sellami CEA, List, Univ. Grenoble Alpes | ||
14:00 - 15:30 | |||
14:00 18mTalk | Lessons from Building an Auto-Active Verifier in Lean Dafny George Pîrlea National University of Singapore, Vladimir Gladshtein , Qiyuan Zhao National University of Singapore, Ilya Sergey National University of Singapore Pre-print | ||
14:18 18mTalk | Formal Verification of Minimax Algorithms Dafny Wieger Wesselink Eindhoven University of Technology, Kees Huizing Eindhoven University of Technology, Huub van de Wetering Eindhoven University of Technology | ||
14:36 18mTalk | Teaching Automata Theory and Formal Languages with Dafny Dafny Ran Ettinger NVIDIA and Ben-Gurion University of the Negev and Israel Academic College in Ramat Gan | ||
14:54 18mTalk | Verification of E-Voting Algorithms in Dafny Dafny Robert Büttner University of Regensburg, Fabian Franz Dießl University of Regensburg, Patrick Janoschek University of Regensburg, Ivana Kostadinovic University of Regensburg, Henrik Oback University of Regensburg, Kilian Voß University of Regensburg, Franziska Alber University of Regensburg, Roland Herrmann University of Regensburg, Sibylle Möhle University of Regensburg, Philipp Rümmer University of Regensburg and Uppsala University | ||
15:12 18mTalk | A Correct-by-Construction Checker for Validation of Railway Data Dafny Benoît Boyer Mitsubishi Electric R&D Centre Europe, Rennes, France, Noé Canva Inria Saclay & Université Paris-Saclay, Matteo Manighetti Inria & École Polytechnique, Claude Marché Inria Saclay & Université Paris-Saclay | ||
14:00 - 15:30 | |||
14:00 90mTutorial | Verifying Probabilistic Programs Using Separation Logic Tutorials Alejandro Aguirre Aarhus University, Simon Oddershede Gregersen New York University, Philipp G. Haselwarter Aarhus University | ||
14:00 - 15:30 | |||
14:00 90mTutorial | Discrete and Continuous Models for Concurrent Systems: From Petri Nets to Directed Spaces Tutorials Uli Fahrenberg Université Paris-Saclay, CNRS, ENS Paris-Saclay, LMF | ||
14:00 - 15:30 | |||
14:00 18mTalk | Fun with flags: How Compilers Break and Fix Constant-Time Code PriSC | ||
14:18 18mTalk | GnuZero: A Compiler-Based Zeroization Static Detection Tool for the Masses PriSC Pierrick Philippe Univ Rennes, CNRS, IRISA, Mohamed Sabt Univ Rennes, CNRS, IRISA, Pierre-Alain Fouque Univ Rennes, CNRS, IRISA | ||
14:36 18mTalk | Tooling Design and Lessons Learned from Systematic Evaluations of the Preservation of Low-level Security Properties by Compilers with BinSec PriSC Yanis Sellami CEA, List, Univ. Grenoble Alpes, Frédéric Recoules CEA, List, Sébastien Bardin CEA LIST, University Paris-Saclay | ||
14:54 18mTalk | Decompiling for Constant-Time Analysis PriSC Sören van der Wall TU Braunschweig, 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, Youcef Bouzid , Zhiyuan Zhang | ||
15:12 18mTalk | Modular Verification of Probabilistic Constant-Time PriSC Xingyu Xie MPI-SP | ||
16:00 - 18:00 | |||
16:00 18mTalk | ATLAS: Automated Toolkit for Large-Scale Verified Code Synthesis Dafny Mantas Bakšys University of Cambridge, Stefan Zetzsche Amazon Web Services, Olivier Bouissou Amazon Web Services, Soonho Kong Amazon Web Services, Remi Delmas Amazon Web Services | ||
16:18 18mTalk | A benchmark for vericoding: formally verified program synthesis Dafny Sergiu Bursuc Beneficial AI Foundation, Theodore Ehrenborg Beneficial AI Foundation, Shaowei Lin Beneficial AI Foundation, Lăcrămioara Aștefănoaei Beneficial AI Foundation, Ionel Emilian Chiosa MIT, Jure Kukovec Beneficial AI Foundation, Alok Singh Beneficial AI Foundation, Oliver Butterley Beneficial AI Foundation, Adem Bizid MIT, Quinn Dougherty Beneficial AI Foundation, Miranda Zhao MIT, Max Tan MIT, Max Tegmark Massachusetts Institute of Technology | ||
16:36 18mTalk | DafnyPro: LLM-Assisted Automated Verification for Dafny Programs Dafny | ||
16:54 18mTalk | MiniF2F-Dafny: LLM-Guided Mathematical Theorem Proving via Auto-Active Verification Dafny Mantas Bakšys University of Cambridge, Stefan Zetzsche Amazon Web Services, Olivier Bouissou Amazon Web Services | ||
17:12 18mTalk | Specification-Guided Repair of Arithmetic Errors in Dafny Programs using LLMs Dafny Valentina Wu Faculdade de Engenharia, Universidade do Porto, Alexandra Mendes Faculty of Engineering, University of Porto & INESC TEC, Alexandre Abreu INESC TEC, Faculdade de Engenharia, Universidade do Porto | ||
17:30 18mTalk | Toward Automated, Contamination-free Dafny Benchmark Generation Dafny Changjie Wang KTH Royal Institute of Technology, Mariano Scazzariello RISE Research Institutes of Sweden, Dejan Kostic KTH Royal Institute of Technology, Marco Chiesa KTH Royal Institute of Technology | ||
17:48 12mDay closing | Day closing Dafny | ||
16:00 - 17:30 | |||
16:00 90mTutorial | Verifying Probabilistic Programs Using Separation Logic Tutorials Alejandro Aguirre Aarhus University, Simon Oddershede Gregersen New York University, Philipp G. Haselwarter Aarhus University | ||
16:00 - 17:30 | |||
16:00 90mTutorial | Discrete and Continuous Models for Concurrent Systems: From Petri Nets to Directed Spaces Tutorials Uli Fahrenberg Université Paris-Saclay, CNRS, ENS Paris-Saclay, LMF | ||
Mon 12 JanDisplayed time zone: Brussels, Copenhagen, Madrid, Paris change
Mon 12 Jan
Displayed time zone: Brussels, Copenhagen, Madrid, Paris change
09:00 - 10:30 | |||
09:00 60mKeynote | How can Machine Learning Helps Formal Proving ? CPP | ||
10:08 22mTalk | Higher order differential calculus in Mathlibdistinguished paper CPP Sebastien Gouezel CNRS and Rennes University | ||
09:00 - 10:30 | |||
09:00 60mKeynote | Current State of the Industrial-Strength Infer Static Analysis Platform VMCAI David Pichardie Meta | ||
10:00 30mTalk | Try-Mopsa: Relational Static Analysis in Your Pocket VMCAI Raphaël Monat Inria and University of Lille | ||
09:00 - 10:30 | |||
09:00 90mTutorial | Syntactically and Semantically Constraining LLMs with Guarantees using Structured LLM Generation Tutorials Sasa Misailovic University of Illinois at Urbana-Champaign, Gagandeep Singh University of Illinois at Urbana-Champaign; VMware Research, Shubham Ugare Meta, Debangshu Banerjee UIUC, Tarun Suresh University of Illinois, Urbana-Champaign, Adharsh Kamath UIUC | ||
11:00 - 12:50 | Formalized mathematicsCPP at Belvédère Chair(s): Marie Kerjean CNRS, Université Sorbonne Paris Nord, Filippo Alberto Edoardo Nuccio Mortarino Majno di Capriglio Inria, Université Jean Monnet Saint-Étienne | ||
11:00 22mTalk | Bar Inductive Predicates for Constructive Algebra in Rocq CPP Dominique Larchey-Wendling Université de Lorraine, CNRS, LORIA DOI Pre-print | ||
11:22 22mTalk | Computing Solutions for Systems of Multivariate Ordinary Differential Equations in Rocq CPP Holger Thies Kyoto University | ||
11:44 22mTalk | Cylindrical Algebraic Decomposition in Coq/Rocq CPP Quentin Vermande Université Côte d'Azur, Inria | ||
12:06 22mTalk | Adhesive Category Theory for Graph Rewriting in Rocq CPP | ||
12:28 22mTalk | Formalizing polynomial laws and the universal divided power algebra CPP | ||
11:00 - 12:30 | |||
11:00 30mTalk | Data Race Detection by Digest-Driven Abstract Interpretation VMCAI | ||
11:30 30mTalk | Termination Resilience Static Analysis VMCAI Naïm Moussaoui Remil Inria & ENS | PSL, Paris, France, Caterina Urban Inria Paris - ENS - Université PSL | ||
12:00 30mTalk | Forward Symbolic Execution for Trustworthy Automation of Binary Code Verification VMCAI Andreas Lindner Uppsala universitet, Karl Palmskog KTH Royal Institute of Technology, Scott Constable Intel Corporation, Mads Dam KTH, Roberto Guanciale KTH Royal Institute of Technology, Hamed Nemati KTH Royal Institute of Technology | ||
11:00 - 12:30 | |||
11:00 90mTutorial | Syntactically and Semantically Constraining LLMs with Guarantees using Structured LLM Generation Tutorials Sasa Misailovic University of Illinois at Urbana-Champaign, Gagandeep Singh University of Illinois at Urbana-Champaign; VMware Research, Shubham Ugare Meta, Debangshu Banerjee UIUC, Tarun Suresh University of Illinois, Urbana-Champaign, Adharsh Kamath UIUC | ||
14:00 - 15:30 | Proof assistantsCPP at Belvédère Chair(s): Sophie Tourret Inria and Max Planck Institute for Informatics | ||
14:00 22mTalk | A Certifying Proof Assistant for Synthetic Mathematics in Lean CPP Wojciech Nawrocki Carnegie Mellon University, Joseph Hua Carnegie Mellon University, Mario Carneiro Chalmers University of Technology, Yiming Xu LMU Munich, Spencer Woolfson Carnegie Mellon University, Shuge Rong Carnegie Mellon University, Sina Hazratpour Johns Hopkins University, Steve Awodey Carnegie Mellon University | ||
14:22 22mTalk | Adding Sorts to an Isabelle Formalization of Superposition CPP Balazs Toth Ludwig-Maximilians-Universität München, Martin Desharnais Ludwig-Maximilians-Universität München, Jasmin Blanchette Ludwig-Maximilians-Universität München | ||
14:45 22mTalk | A Lambda-Superposition Tactic for Isabelle/HOL CPP Massin Guerdi Ludwig-Maximilians-Universität München | ||
15:07 22mTalk | Certifying the decidability of the word problem in monoids at large CPP Reinis Cirpons St Andrews University, Florent Hivert Univ. Paris-Saclay, LISN, LMF, CNRS, INRIA, Assia Mahboubi INRIA, Guillaume Melquiond Université Paris-Saclay - CNRS - ENS Paris-Saclay - Inria, James Mitchell St Andrews University, Finn Smith St Andrews University | ||
14:00 - 15:30 | |||
14:00 60mKeynote | Understanding Transformers through the Lens of Logic and Automata VMCAI Anthony Widjaja Lin TU Kaiserslautern; MPI-SWS | ||
15:00 30mTalk | Proof Minimization in Neural Network Verification VMCAI Omri Isac The Hebrew University of Jerusalem, Idan Refaeli Hebrew University of Jerusalem, Haoze Wu Stanford University, Clark Barrett Stanford University, Guy Katz The Hebrew University of Jerusalem | ||
14:00 - 15:30 | |||
14:00 90mTutorial | A Guided Tour through Oxidized OCaml Tutorials Gavin Gray Brown University, Anil Madhavapeddy University of Cambridge, UK, KC Sivaramakrishnan IIT Madras and Tarides, Will Crichton Brown University, Shriram Krishnamurthi Brown University, Chris Casinghino Jane Street, Richard A. Eisenberg Jane Street | ||
14:00 - 15:30 | |||
14:00 90mTutorial | Veil: Automated and Interactive Verification of Transition Systems Tutorials | ||
16:00 - 17:30 | |||
16:00 22mTalk | Mechanized Dominator Tree Certificationdistinguished paper CPP Jean-Christophe Léchenet Université Côte d’Azur, Inria DOI Pre-print | ||
16:22 22mTalk | Brack: A Verified Compiler for Scheme via CakeML CPP Pascal Lasnier University of Cambridge, Jeremy Yallop University of Cambridge, Magnus O. Myreen Chalmers University of Technology | ||
16:45 22mTalk | Verified VCG and Verified Compiler for Dafny CPP Daniel Nezamabadi ETH Zurich, Magnus O. Myreen Chalmers University of Technology, Yong Kiam Tan Institute for Infocomm Research, A*STAR | ||
17:07 22mTalk | Foundational Verification of Running-Time Bounds for Interactive Programs CPP Thomas Carotti MIT, Andy Tockman Massachussetts Institute of Technology, Pratap Singh CMU, Andres Erbsen Google, Samuel Gruetter ETH Zurich, Adam Chlipala Massachusetts Institute of Technology | ||
16:00 - 17:30 | Models 1VMCAI at Horizons Chair(s): Mihaela Sighireanu University Paris-Saclay, ENS Paris-Saclay, CNRS, LMF | ||
16:00 30mTalk | Verification of Generic VHDL Designs and Their Translation to Rocq VMCAI Ocan Sankur University of Rennes, France / Inria, France / CNRS, France / IRISA, France, Benoît Boyer Mitsubishi Electric R&D Centre Europe, Rennes, France, Florian Faissole Mitsubishi Electric R&D Centre Europe | ||
16:30 30mTalk | A Formal Executable Semantics of PROMELA VMCAI | ||
17:00 30mTalk | Efficient Discovery of Actual Causality in Stochastic Systems VMCAI Arshia Rafieioskouei Michigan State University, Kenneth Rogale Michigan State University, Borzoo Bonakdarpour Michigan State University | ||
16:00 - 17:30 | |||
16:00 90mTutorial | A Guided Tour through Oxidized OCaml Tutorials Gavin Gray Brown University, Anil Madhavapeddy University of Cambridge, UK, KC Sivaramakrishnan IIT Madras and Tarides, Will Crichton Brown University, Shriram Krishnamurthi Brown University, Chris Casinghino Jane Street, Richard A. Eisenberg Jane Street | ||
16:00 - 17:30 | |||
16:00 90mTutorial | Veil: Automated and Interactive Verification of Transition Systems Tutorials | ||
Tue 13 JanDisplayed time zone: Brussels, Copenhagen, Madrid, Paris change
Tue 13 Jan
Displayed time zone: Brussels, Copenhagen, Madrid, Paris change
09:00 - 10:30 | |||
09:00 60mKeynote | TBA CPP Jennifer Paykin University of Vermont | ||
10:00 30mMeeting | Business Meeting CPP | ||
09:00 - 10:30 | |||
09:00 60mKeynote | TypedC: Spatial Memory Safety for Low Level Programs by Abstract Interpretation VMCAI Mihaela Sighireanu University Paris-Saclay, ENS Paris-Saclay, CNRS, LMF | ||
10:00 30mTalk | Input-based Three-Valued Abstraction Refinement VMCAI | ||
09:00 - 10:30 | |||
09:00 10mDay opening | Welcome from the Organizers RTFM Amal Ahmed Northeastern University, USA, Derek Dreyer MPI-SWS, Ilya Sergey National University of Singapore | ||
09:10 40mTalk | On long-term research vision RTFM Peter Sewell University of Cambridge | ||
09:50 40mTalk | On transitioning from academia to industry RTFM David Pichardie Meta | ||
09:00 - 10:30 | |||
09:00 90mTutorial | Analyzing Shell Scripts Tutorials Michael Greenberg Stevens Institute of Technology, Konstantinos Kallas University of California, Los Angeles, Nikos Vasilakis Brown University | ||
09:00 - 10:30 | |||
09:00 5mDay opening | Welcome PEPM | ||
11:00 - 12:30 | |||
11:00 30mTalk | Multi-variable Quantification of BDDs in External Memory using Nested Sweeping VMCAI | ||
11:30 30mTalk | Producing Shorter Congruence Closure Proofs in a State-of-the-Art SMT Solver VMCAI Bruno Andreotti Universidade Federal de Minas Gerais, Haniel Barbosa Universidade Federal de Minas Gerais | ||
12:00 30mTalk | SAT-Based Synthesis of Minimal Deterministic Real-Time Automata via 3DRTA Representation VMCAI Junjie Meng School of Computer Science and Technology, Tongji University, Jie An Institute of Software Chinese Academy of Sciences, Yong Li Institute of Software, Chinese Academy of Sciences, Andrea Turrini Institute of Software, Chinese Academy of Sciences, Miaomiao Zhang School of Computer Science and Technology, Tongji University | ||
11:00 - 12:30 | |||
11:00 40mTalk | On building a successful research group RTFM Stephanie Weirich University of Pennsylvania | ||
11:40 50mPanel | Panel: Promotion and tenure RTFM M: Derek Dreyer MPI-SWS, P: Amal Ahmed Northeastern University, USA, P: Steve Zdancewic University of Pennsylvania | ||
11:00 - 12:30 | |||
11:00 90mTutorial | Analyzing Shell Scripts Tutorials Michael Greenberg Stevens Institute of Technology, Konstantinos Kallas University of California, Los Angeles, Nikos Vasilakis Brown University | ||
14:00 - 15:30 | |||
14:00 22mTalk | Certified Symbolic Finite Transducers: Formalization and Applications to String Analysis CPP | ||
14:22 22mTalk | Enhancing Symbolic Execution with Machine-Checked Safety Proofs CPP | ||
14:45 22mTalk | Layers of Confluence for Actors CPP Ludovic Henrio University of Lyon - ENS Lyon - UCBL - CNRS - Inria - LIP, Einar Broch Johnsen University of Oslo, Åsmund Aqissiaq Arild Kløvstad University of Oslo (UiO), Violet Ka I Pun Western Norway University of Applied Sciences, Yannick Zakowski Inria | ||
15:07 22mTalk | Towards composable proofs of cache coherence protocols CPP | ||
14:00 - 15:30 | |||
14:00 30mTalk | Atomic Gliders and Cellular Automata as Language Generators VMCAI Dana Fisman Ben-Gurion University, Noa Izsak CISPA Helmholtz Center for Information Security, Germany | ||
14:30 30mTalk | Reachability in multi-agent transfer systems VMCAI Nathalie Bertrand INRIA Rennes, Loic Helouet INRIA, Engel Lefaucheux Université de Lorraine; CNRS; Inria; LORIA, Luca Paparazzo Inria, IRISA, Université de Rennes | ||
15:00 30mTalk | A Hybrid Meta-Learning Framework for Adaptive Safe Controller Synthesis of Dynamical Models VMCAI Rui Guo Zhejiang Sci-Tech University, Yang Li Zhejiang Sci-Tech University, Xiuqing Cao Zhejiang Sci-Tech University, Wang Lin | ||
14:00 - 15:30 | |||
14:00 40mTalk | On grant writing RTFM Suresh Jagannathan Purdue University | ||
14:40 50mPanel | Panel: Visibility and impact RTFM M: Ilya Sergey National University of Singapore, P: Xavier Leroy Collège de France - PSL University, P: Nikhil Swamy Microsoft Research, P: Derek Dreyer MPI-SWS | ||
14:00 - 15:30 | |||
14:00 90mTutorial | Is Program Synthesis Soluble in Large Language Models? Tutorials Nathanaël Fijalkow CNRS, LaBRI, University of Bordeaux | ||
16:00 - 17:30 | |||
16:00 22mTalk | A Recipe for Modular Verification of Generic Tree Traversals CPP Laila Elbeheiry MPI-SWS, Michael Sammler Institute of Science and Technology Austria, Robbert Krebbers Radboud University Nijmegen, Derek Dreyer MPI-SWS, Deepak Garg MPI-SWS | ||
16:22 22mTalk | Precise Reasoning about Container-Internal Pointers with Logical Pinningdistinguished paper CPP | ||
16:45 22mTalk | Modular Specifications and Implementations of Random Samplers in Higher-Order Separation Logic CPP Virgil Marionneau ENS Rennes, Félix Sassus-Bourda ENS Paris Saclay, Alejandro Aguirre Aarhus University, Lars Birkedal Aarhus University | ||
17:07 22mTalk | Using Ghost Ownership to Verify Union-Find and Persistent Arrays in Rust CPP Arnaud Golfouse Université Paris-Saclay, CNRS, ENS Paris-Saclay, Inria, Laboratoire des méthodes formelles, 91190, Gif-sur-Yvette, France, Armaël Guéneau Université Paris-Saclay - CNRS - ENS Paris-Saclay - Inria, Jacques-Henri Jourdan CNR, LMF | ||
16:00 - 17:30 | Quantum and Probabilistic VerificationVMCAI at Horizons Chair(s): Jyun-Ao Lin National Taipei University of Technology | ||
16:00 30mTalk | Efficiently Verifying Quantum Programs with Few T Gates VMCAI | ||
16:30 30mTalk | Finding Photonics Circuits via δ-weakening SMT VMCAI | ||
17:00 30mTalk | Probabilistic Verification for Modular Network-on-Chip Systems VMCAI Nick Waddoups nick.waddoups@usu.edu, Jonah Boe Hill Air Force Base, Utah, Arnd Hartmanns University of Twente, Prabal Basu Utah State University, Sanghamitra Roy Utah State University, Koushik Chakraborty Utah State University, Zhen Zhang Utah State University | ||
16:00 - 17:30 | |||
16:00 60mPanel | Panel: Work-life balance, service, and teaching RTFM M: Amal Ahmed Northeastern University, USA, P: Sebastian Erdweg KIT, P: Robbert Krebbers Radboud University Nijmegen, P: Sharon Shoham Tel Aviv University | ||
16:00 - 17:30 | |||
16:00 90mTutorial | Is Program Synthesis Soluble in Large Language Models? Tutorials Nathanaël Fijalkow CNRS, LaBRI, University of Bordeaux | ||
Wed 14 JanDisplayed time zone: Brussels, Copenhagen, Madrid, Paris change
Wed 14 Jan
Displayed time zone: Brussels, Copenhagen, Madrid, Paris change
09:00 - 10:00 | |||
09:00 60mKeynote | Medium-scale automation for proof assistants POPL Damien Pous CNRS | ||
10:30 - 12:10 | |||
10:30 25mTalk | A Modular Static Cost Analysis for GPU Warp-Level Parallelism POPL Gregory Blike University of Massachusetts at Boston, Hannah Zicarelli University of Massachusetts at Boston, Udaya Sathiyamoorthy University of Massachusetts at Boston, Julien Lange Royal Holloway University of London, Tiago Cogumbreiro University of Massachusetts at Boston DOI | ||
10:55 25mTalk | ChiSA: Static Analysis for Lightweight Chisel Verification POPL Jiacai Cui Nanjing University, Qinlin Chen Nanjing University, Zhongsheng Zhan Nanjing University, Tian Tan Nanjing University, Yue Li Nanjing University DOI | ||
11:20 25mTalk | Miri: Practical Undefined Behavior Detection for Rust POPL Ralf Jung ETH Zurich, Benjamin Kimock Lansweeper NV, Christian Poveda Unaffiliated, Eduardo Sánchez Muñoz Unaffiliated, Oli Scherer Unaffiliated, Qian (Andy) Wang ETH Zurich and Imperial College London DOI | ||
11:45 25mTalk | Piecewise Analysis of Probabilistic Programs via k-Induction POPL Tengshun Yang Institute of Software at Chinese Academy of Sciences, Shenghua Feng Institute of Software at Chinese Academy of Sciences, Hongfei Fu Shanghai Jiao Tong University, Naijun Zhan Peking University; Zhongguancun Lab, Jingyu Ke Shanghai Jiao Tong University, Shiyang Wu Shanghai Jiao Tong University DOI | ||
10:30 - 12:10 | |||
10:30 25mTalk | Domain-Theoretic Semantics for Functional Logic Programming POPL Eddie Jones University of Bristol, Samson Main University of Bristol, Celia Mengyue Li University of Bristol, Jonathan Marriott University of Bristol, Alex Kavvos University of Bristol DOI | ||
10:55 25mTalk | Handling Scope Checks: A Comparative Framework for Dynamic Scope Extrusion Checks POPL Michael Lee University of Cambridge, UK, Ningning Xie University of Toronto, Oleg Kiselyov Tohoku University, Jeremy Yallop University of Cambridge DOI | ||
11:20 25mTalk | Hyperfunctions: Communicating Continuations POPL DOI Pre-print | ||
11:45 25mTalk | Lazy Linearity for a Core Functional Language POPL DOI Pre-print | ||
10:30 - 12:10 | |||
10:30 25mTalk | Bounded Treewidth, Multiple Context-Free Grammars, and Downward Closures POPL C. Aiswarya Chennai Mathematical Institute, Pascal Baumann MPI-SWS, Prakash Saivasan Institute of Mathematical Sciences, Lia Schütze MPI-SWS, Georg Zetzsche MPI-SWS DOI | ||
10:55 25mTalk | Formal Verification for JavaScript Regular Expressions: A Proven Mechanized Semantics and Its Applications POPL Aurèle Barrière EPFL, Victor Deng EPFL; École Normale Supérieure - PSL - CNRS, Clément Pit-Claudel EPFL DOI | ||
11:20 25mTalk | Network Change Validation with Relational NetKAT POPL Han Xu Princeton University, Zachary Kincaid Princeton University, Ratul Mahajan University of Washington, Intentionet, David Walker DOI | ||
11:45 25mTalk | Parameterized Verification of Quantum Circuits POPL Parosh Aziz Abdulla Uppsala University; Mälardalen University, Yu-Fang Chen Academia Sinica, Michal Hečko Brno University of Technology, Lukáš Holík Brno University of Technology; Aalborg University, Ondřej Lengál Brno University of Technology, Jyun-Ao Lin National Taipei University of Technology, Ramanathan S. Thinniyam Uppsala University DOI | ||
14:00 - 15:40 | |||
14:00 25mTalk | An Expressive Assertion Language for Quantum Programs POPL Bonan Su Tsinghua University, Yuan Feng Tsinghua University, Mingsheng Ying Institute of Software at Chinese Academy of Sciences; Tsinghua University, Li Zhou Institute of Software at Chinese Academy of Sciences DOI | ||
14:25 25mTalk | Hadamard-Pi: Equational Quantum Programming POPL Wang Fang University of Edinburgh, Chris Heunen University of Edinburgh, Robin Kaarsgaard University of Southern Denmark DOI | ||
14:50 25mTalk | Qudit Quantum Programming with Projective Cliffords POPL DOI | ||
15:15 25mTalk | RapunSL: Untangling Quantum Computing with Separation, Linear Combination and Mixing POPL Yusuke Matsushita Kyoto University, Kengo Hirata University of Edinburgh, Ryo Wakizaka Kyoto University, Emanuele D'Osualdo University of Konstanz DOI Pre-print | ||
14:00 - 15:40 | |||
14:00 25mTalk | Extensible Data Types with Ad-Hoc Polymorphism POPL Matthew Toohey University of Toronto, Yanning Chen University of Toronto, Ara Jamalzadeh University of Toronto, Ningning Xie University of Toronto DOI | ||
14:25 25mTalk | Let Generalization, Polymorphic Recursion, and Variable Minimization in Boolean-Kinded Type Systems POPL Joseph Zullo Purdue University DOI | ||
14:50 25mTalk | Local Contextual Type Inference POPL Xu Xue University of Hong Kong, Chen Cui University of Hong Kong, Shengyi Jiang The University of Hong Kong, Bruno C. d. S. Oliveira University of Hong Kong DOI | ||
15:15 25mTalk | Typing Strictness POPL Daniel Sainati University of Pennsylvania, Joseph W. Cutler University of Pennsylvania, Benjamin C. Pierce University of Pennsylvania, Stephanie Weirich University of Pennsylvania DOI | ||
16:10 - 17:25 | |||
16:10 25mTalk | Characterizing Sets of Theories That Can Be Disjointly Combined POPL DOI | ||
16:35 25mTalk | Context-Free-Language Reachability for Almost-Commuting Transition Systems POPL Nikhil Pimpalkhare Princeton University, Zachary Kincaid Princeton University, Thomas Reps University of Wisconsin-Madison DOI | ||
17:00 25mTalk | Determination Problems for Orbit Closures and Matrix Groups POPL Rida Ait El Manssour University of Oxford, George Kenison Liverpool John Moores University, Mahsa Shirmohammadi CNRS, Anton Varonka TU Wien, James Worrell University of Oxford DOI | ||
16:10 - 17:25 | |||
16:10 25mTalk | Accelerating Syntax-Guided Program Synthesis by Optimizing Domain-Specific Languages POPL Zhentao Ye Peking University, Ruyi Ji Peking University, Yingfei Xiong Peking University, Xin Zhang Peking University DOI | ||
16:35 25mTalk | Inductive Program Synthesis by Meta-Analysis-Guided Hole Filling POPL Doyoon Lee Seoul National University, Woosuk Lee Hanyang University, Kwangkeun Yi Seoul National University DOI | ||
17:00 25mTalk | Oriented Metrics for Bottom-Up Enumerative Synthesis POPL DOI | ||
16:10 - 17:25 | |||
16:10 25mTalk | ChopChop: A Programmable Framework for Semantically Constraining the Output of Language Models POPL Shaan Nagy University of California at San Diego, Timothy Zhou , Nadia Polikarpova University of California at San Diego, Loris D'Antoni University of California at San Diego DOI | ||
16:35 25mTalk | Compiling to Linear Neurons POPL Joey Velez-Ginorio , Nada Amin Harvard University, Konrad Kording University of Pennsylvania, Steve Zdancewic University of Pennsylvania DOI | ||
17:00 25mTalk | Fuzzing Guided by Bayesian Program Analysis POPL DOI | ||
Thu 15 JanDisplayed time zone: Brussels, Copenhagen, Madrid, Paris change
Thu 15 Jan
Displayed time zone: Brussels, Copenhagen, Madrid, Paris change
10:20 - 12:00 | |||
10:20 25mTalk | (TOPLAS) Will it Fit? Verifying Heap Space Bounds of Concurrent Programs under Garbage Collection POPL | ||
10:45 25mTalk | Verifying Almost-Sure Termination for Randomized Distributed Algorithms POPL Constantin Enea LIX, CNRS, Ecole Polytechnique, Rupak Majumdar MPI-SWS, Harshit Jitendra Motwani MPI-SWS, V.R. Sathiyanarayana MPI-SWS DOI | ||
11:10 25mTalk | Zoo: A Framework for the Verification of Concurrent OCaml 5 Programs using Separation Logic POPL DOI | ||
11:35 25mTalk | The Complexity of Testing Message-Passing Concurrency POPL Zheng Shi National University of Singapore, Lasse Møldrup Aarhus University, Umang Mathur National University of Singapore, Andreas Pavlogiannis Aarhus University DOI Pre-print | ||
10:20 - 12:00 | |||
10:20 25mTalk | A Relational Separation Logic for Effect Handlers POPL Paulo Emílio de Vilhena Imperial College London, Simcha van Collem Radboud University Nijmegen, Ines Wright Aarhus University, Robbert Krebbers Radboud University Nijmegen DOI | ||
10:45 25mTalk | Bayesian Separation Logic POPL Shing Hin Ho Imperial College London, Nicolas Wu Imperial College London, Azalea Raad Imperial College London DOI Pre-print | ||
11:10 25mTalk | Cryptis: Cryptographic Reasoning in Separation Logic POPL Arthur Azevedo de Amorim Rochester Institute of Technology, Amal Ahmed Northeastern University, USA, Marco Gaboardi Boston University DOI | ||
11:35 25mTalk | Separating the Wheat from the Chaff: Understanding (In-)Completeness of Proof Mechanisms for Separation Logic with Inductive Definitions POPL Neta Elad Tel Aviv University, Adithya Murali University of Wisconsin, Sharon Shoham Tel Aviv University DOI | ||
14:00 - 15:40 | |||
14:00 25mTalk | Classical Notions of Computation and the Hasegawa-Thielecke Theorem POPL Éléonore Mangel Univ. Paris Cité - CNRS - Inria, Paul-André Melliès Univ. Paris Cité - CNRS - Inria, Guillaume Munch-Maccagnoni INRIA DOI | ||
14:25 25mTalk | From Semantics to Syntax: A Type Theory for Comprehension Categories POPL Niyousha Najmaei École Polytechnique, Niels van der Weide Radboud University, Benedikt Ahrens Delft University of Technology, Paige Randall North Utrecht University DOI | ||
14:50 25mTalk | Higher-Order Behavioural Conformances via Fibrations POPL Henning Urbat Friedrich-Alexander-University Erlangen-Nürnberg DOI | ||
15:15 25mTalk | What Is a Monoid? POPL DOI | ||
14:00 - 15:40 | |||
14:00 25mTalk | A Lazy, Concurrent Convertibility Checker POPL DOI | ||
14:25 25mTalk | Canonicity for Indexed Inductive-Recursive Types POPL András Kovács University of Gothenburg and Chalmers University of Technology DOI | ||
14:50 25mTalk | Coco: Corecursion with Compositional Heterogeneous Productivity POPL Jaewoo Kim Seoul National University, Yeonwoo Nam Seoul National University, Chung-Kil Hur Seoul National University DOI | ||
15:15 25mTalk | Towards Pen-and-Paper-Style Equational Reasoning in Interactive Theorem Provers by Equality Saturation POPL Marcus Rossel Barkhausen Institut; TU Darmstadt, Rudi Schneider TU Berlin, Thomas Koehler ICube Lab - CNRS - Université de Strasbourg, Michel Steuwer TU Berlin, Andrés Goens TU Darmstadt DOI | ||
14:00 - 15:40 | |||
14:00 25mTalk | A Logic for the Imprecision of Abstract Interpretations POPL Marco Campion Inria Paris - ENS - Université PSL, Mila Dalla Preda University of Verona, Roberto Giacobazzi University of Arizona, Caterina Urban Inria Paris - ENS - Université PSL DOI | ||
14:25 25mTalk | Big-Stop Semantics: Small-Step Semantics in a Big-Step Judgment POPL David M. Kahn Carnegie Mellon University, Jan Hoffmann Carnegie Mellon University, Runming Li Carnegie Mellon University DOI | ||
14:50 25mTalk | JAX Autodiff from a Linear Logic Perspective POPL DOI | ||
15:15 25mTalk | U-Turn: Enhancing Incorrectness Analysis by Reversing Direction POPL Flavio Ascari University of Konstanz, Roberto Bruni University of Pisa, Roberta Gori Diaprtimento di Informatica, Universita' di Pisa, Italy, Azalea Raad Imperial College London DOI | ||
16:10 - 17:00 | |||
16:10 25mTalk | Nice to Meet You: Synthesizing Practical MLIR Abstract Transformers POPL Xuanyu Peng University of California at San Diego, Dominic Kennedy University of Utah, Yuyou Fan University of Utah, Ben Greenman University of Utah, USA, John Regehr University of Utah, Loris D'Antoni University of California at San Diego DOI | ||
16:35 25mTalk | Parameterized Infinite-State Reactive Synthesis POPL DOI | ||
16:10 - 17:00 | |||
16:10 25mTalk | A Family of Sims with Diverging Interests POPL Nicolas Chappe CNRS - Verimag DOI | ||
16:35 25mTalk | Endangered by the Language But Saved by the Compiler: Robust Safety via Semantic Back-Translation POPL Niklas Mück MPI-SWS, Aina Linn Georges Max Planck Institute for Software Systems (MPI-SWS), Derek Dreyer MPI-SWS, Deepak Garg MPI-SWS, Michael Sammler Institute of Science and Technology Austria DOI Pre-print | ||
16:10 - 17:00 | |||
16:10 25mTalk | Dependent Coeffects for Local Sensitivity Analysis POPL Victor Sannier Univ. Lille - CNRS - Inria - Centrale Lille - UMR 9189 CRIStAL, Patrick Baillot Univ. Lille - CNRS - Inria - Centrale Lille - UMR 9189 CRIStAL DOI | ||
16:35 25mTalk | Security Reasoning via Substructural Dependency Tracking POPL Hemant Gouni Carnegie Mellon University, Frank Pfenning Carnegie Mellon University, USA, Jonathan Aldrich Carnegie Mellon University DOI Pre-print | ||
Fri 16 JanDisplayed time zone: Brussels, Copenhagen, Madrid, Paris change
Fri 16 Jan
Displayed time zone: Brussels, Copenhagen, Madrid, Paris change
09:00 - 10:00 | |||
09:00 60mKeynote | Hardware-Software Contracts for High Assurance with Applications to Side-Channel Security POPL Caroline Trippel Stanford University | ||
10:30 - 12:10 | |||
10:30 25mTalk | Abstraction Functions as Types POPL Harrison Grodin Carnegie Mellon University, Runming Li Carnegie Mellon University, Robert Harper Carnegie Mellon University DOI | ||
10:55 25mTalk | Foundational Multi-Modal Program Verifiers POPL Vladimir Gladshtein , George Pîrlea National University of Singapore, Qiyuan Zhao National University of Singapore, Vitaly Kurin Neapolis University Pafos, Ilya Sergey National University of Singapore DOI | ||
11:20 25mTalk | Stateful Differential Operators for Incremental Computing POPL DOI | ||
11:45 25mTalk | The Ghosts of Empires: Extracting Modularity from Interleaving-Based Proofs POPL Frank Schüssele University of Freiburg, Matthias Zumkeller University of Freiburg, Miriam Lagunes-Rochin University of Freiburg, Dominik Klumpp LIX - CNRS - École Polytechnique; University of Freiburg DOI | ||
10:30 - 12:10 | |||
10:30 25mTalk | Di- is for Directed: First-Order Directed Type Theory via Dinaturality POPL Andrea Laretto Tallinn University of Technology, Fosco Loregian Tallinn University of Technology, Niccolò Veltri IT University of Copenhagen DOI | ||
10:55 25mTalk | Quotient Polymorphism POPL DOI | ||
11:20 25mTalk | The Simple Essence of Boolean-Algebraic Subtyping: Semantic Soundness for Algebraic Union, Intersection, Negation, and Equi-recursive Types POPL Chun Yin Chau HKUST (The Hong Kong University of Science and Technology), Lionel Parreaux Hong Kong University of Science and Technology DOI | ||
11:45 25mTalk | Welterweight Go: Boxing, Structural Subtyping, and Generics POPL Raymond Hu Queen Mary University of London, Julien Lange Royal Holloway University of London, Bernardo Toninho Instituto Superior Técnico - University of Lisbon, Philip Wadler University of Edinburgh, Robert Griesemer Google, Keith Randall Google DOI | ||
14:00 - 15:40 | |||
14:00 25mTalk | An Equational Axiomatization of Dynamic Threads via Algebraic Effects: Presheaves on Finite Relations, Labelled Posets, and Parameterized Algebraic Theories POPL Ohad Kammar University of Edinburgh, Jack Liell-Cock University of Oxford, Sam Lindley University of Edinburgh, Cristina Matache University of Edinburgh, Sam Staton University of Oxford DOI | ||
14:25 25mTalk | Handling Higher-Order Effectful Operations with Judgemental Monadic Laws POPL DOI | ||
14:50 25mTalk | Rows and Capabilities as Modal Effects POPL DOI | ||
15:15 25mTalk | The Relative Monadic Metalanguage POPL Jack Liell-Cock University of Oxford, Zev Shirazi University of Oxford, Sam Staton University of Oxford DOI | ||
14:00 - 15:40 | |||
14:00 25mTalk | AdapTT: Functoriality for Dependent Type Casts POPL Arthur Adjedj ENS Paris Saclay, Université Paris-Saclay, Meven Lennon-Bertrand Inria – Université Paris Cité, Thibaut Benjamin Université Paris-Saclay, CEA, List, Kenji Maillard Inria DOI | ||
14:25 25mTalk | Algorithmic Conversion with Surjective Pairing: A Syntactic and Untyped Approach POPL DOI | ||
14:50 25mTalk | Encode the Cake and Eat It Too: Controlling Computation in Type Theory, Locally POPL DOI | ||
15:15 25mTalk | Normalisation for First-Class Universe Levels POPL Nils Anders Danielsson University of Gothenburg, Naïm Camille Favier Chalmers University of Technology and University of Gothenburg, Ondřej Kubánek Chalmers University of Technology DOI | ||
16:10 - 17:25 | |||
16:10 25mTalk | A Complementary Approach to Incorrectness Typing POPL Celia Mengyue Li University of Bristol, Sophie Pull University of Bristol, Steven Ramsay University of Bristol DOI | ||
16:35 25mTalk | A Synthetic Reconstruction of Multiparty Session Types POPL David Castro-Perez University of Kent, Francisco Ferreira Royal Holloway, University of London, Sung-Shik Jongmans University of Groningen DOI | ||
17:00 25mTalk | Bounded Sort Polymorphism with Elimination Constraints POPL Johann Rosain ENS Lyon, Tomás Diaz University of Chile, Kenji Maillard Inria, Matthieu Sozeau Inria, Nicolas Tabareau Inria, Éric Tanter University of Chile, Théo Winterhalter INRIA DOI | ||
16:10 - 17:25 | |||
16:10 25mTalk | Counting and Sampling Traces in Regular Languages POPL Alexis de Colnet TU Wien, Kuldeep S. Meel University of Toronto, Umang Mathur National University of Singapore DOI Pre-print | ||
16:35 25mTalk | Parametrised Verification of Intel-x86 Programs POPL Parosh Aziz Abdulla Uppsala University; Mälardalen University, Mohamed Faouzi Atig Uppsala University, Ahmed Bouajjani Université Paris Cité, K Narayan Kumar Chennai Mathematical Institute, Prakash Saivasan Institute of Mathematical Sciences DOI | ||
17:00 25mTalk | General Decidability Results for Systems with Continuous Counters POPL A. R. Balasubramanian Technical University of Munich, Matthew Hague Royal Holloway University of London, Rupak Majumdar MPI-SWS, Ramanathan S. Thinniyam Uppsala University, Georg Zetzsche MPI-SWS DOI | ||
16:10 - 17:25 | |||
16:10 25mTalk | Generating Compilers for Qubit Mapping and Routing POPL Abtin Molavi University of Wisconsin-Madison, Amanda Xu University of Wisconsin-Madison, Ethan Cecchetti University of Wisconsin-Madison, Swamit Tannu University of Wisconsin-Madison, Aws Albarghouthi University of Wisconsin-Madison DOI | ||
16:35 25mTalk | On Circuit Description Languages, Indexed Monads, and Resource Analysis POPL Ken Sakayori University of Tokyo, Andrea Colledan University of Bologna; Centre Inria d’Université Côte d’Azur, Ugo Dal Lago University of Bologna; Centre Inria d’Université Côte d’Azur DOI | ||
17:00 25mTalk | Quantum Circuits Are Just a Phase POPL Chris Heunen University of Edinburgh, Louis Lemonnier University of Edinburgh, Christopher McNally Massachusetts Institute of Technology, Alex Rice University of Edinburgh DOI | ||
Sat 17 JanDisplayed time zone: Brussels, Copenhagen, Madrid, Paris change
Sat 17 Jan
Displayed time zone: Brussels, Copenhagen, Madrid, Paris change
09:00 - 10:30 | |||
09:00 60mKeynote | Lean4Lean: Mechanizing the Metatheory of Lean WITS Mario Carneiro Chalmers University of Technology | ||
10:00 22mTalk | Observing Definitional Equality WITS András Kovács University of Gothenburg and Chalmers University of Technology | ||
11:00 - 12:30 | |||
11:00 22mTalk | Decoupling Resolution from Type Inference WITS Lionel Parreaux Hong Kong University of Science and Technology | ||
11:22 22mTalk | First-Class Refinement Types in Scala WITS Matt Bovel EPFL | ||
11:45 22mTalk | Types as grammars WITS Gil Silva LASIGE, University of Lisbon, Bernardo Almeida LASIGE, Faculty of Sciences, University of Lisbon, Diana Costa LASIGE, University of Lisbon, Andreia Mordido University of Lisbon, Diogo Poças Instituto de Telecomunicações, University of Lisbon, Vasco T. Vasconcelos LASIGE, University of Lisbon | ||
12:07 22mTalk | Omnidirectional type inference for ML WITS Alistair O'Brien University of Cambridge, Didier Rémy Inria, Gabriel Scherer Université Paris Cité - Inria - CNRS | ||
14:00 - 15:30 | |||
14:00 22mTalk | A Dependent Language with Type-Safe Program Extraction WITS Greg Brown University of Edinburgh | ||
14:22 22mTalk | Code Generation via Meta-programming in Dependently Typed Proof Assistants WITS | ||
14:45 22mTalk | Garbage Collection for Higher Inductive Types WITS | ||
15:07 22mTalk | Type Inference Techniques: Implementation and Formalization, Better Together WITS | ||
16:00 - 18:00 | |||
16:00 40mKeynote | Verifying Dependent Type-checkers WITS Meven Lennon-Bertrand Inria – Université Paris Cité | ||
17:00 22mTalk | Type Narrowing the Hard Way WITS | ||
17:23 2mOther | Closing WITS Niki Vazou IMDEA Software Institute | ||