CPP 2024
Mon 15 - Tue 16 January 2024
London, United Kingdom
co-located with
POPL 2024
Toggle navigation
Attending
Venue: Institution of Engineering and Technology
Program
CPP Program
Your Program
Mon 15 Jan
Tue 16 Jan
Track/Call
Organization
CPP 2024 Committees
Track Committees
Organizing Committee
Program Committee
Steering Committee
Contributors
People Index
Search
Series
Series
CPP 2025
CPP 2024
CPP 2023
CPP 2022
CPP 2021
CPP 2020
CPP 2019
CPP 2018
CPP 2017
CPP 2016
Sign in
Sign up
POPL 2024
(
series
) /
CPP 2024 (
series
) /
Institution of Engineering and Technology
/
Room information: Marconi Room
Venue
Institution of Engineering and Technology
Room name
Marconi Room
Floor
0
Room Information
No extra information available
Program
Detailed Table
Session Timeline
Detailed Timeline
Program Display Configuration
Time Zone
The program is currently displayed in
(GMT) London
.
Use conference time zone: (GMT) London
Select other time zone
(GMT-12:00) AoE (Anywhere On Earth)
(GMT-11:00) Midway Island, Samoa
(GMT-10:00) Hawaii-Aleutian
(GMT-10:00) Hawaii
(GMT-09:30) Marquesas Islands
(GMT-09:00) Gambier Islands
(GMT-09:00) Alaska
(GMT-08:00) Tijuana, Baja California
(GMT-08:00) Pitcairn Islands
(GMT-08:00) Pacific Time (US & Canada)
(GMT-07:00) Mountain Time (US & Canada)
(GMT-06:00) Chihuahua, La Paz, Mazatlan
(GMT-07:00) Arizona
(GMT-06:00) Saskatchewan, Central America
(GMT-05:00) Guadalajara, Mexico City, Monterrey
(GMT-05:00) Easter Island
(GMT-06:00) Central Time (US & Canada)
(GMT-05:00) Eastern Time (US & Canada)
(GMT-05:00) Cuba
(GMT-05:00) Bogota, Lima, Quito, Rio Branco
(GMT-04:00) Caracas
(GMT-03:00) Santiago
(GMT-04:00) La Paz
(GMT-03:00) Faukland Islands
(GMT-04:00) Manaus, Amazonas, Brazil
(GMT-04:00) Atlantic Time (Goose Bay)
(GMT-04:00) Atlantic Time (Canada)
(GMT-03:30) Newfoundland
(GMT-03:00) UTC-3
(GMT-03:00) Montevideo
(GMT-03:00) Miquelon, St. Pierre
(GMT-03:00) Greenland
(GMT-03:00) Buenos Aires
(GMT-03:00) Brasilia, Distrito Federal, Brazil
(GMT-02:00) Mid-Atlantic
(GMT-01:00) Cape Verde Is.
(GMT-01:00) Azores
(UTC) Coordinated Universal Time
(GMT) Belfast
(GMT) Dublin
(GMT) Lisbon
(GMT) London
(GMT) Monrovia, Reykjavik
(GMT+01:00) Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna
(GMT+01:00) Belgrade, Bratislava, Budapest, Ljubljana, Prague
(GMT+01:00) Brussels, Copenhagen, Madrid, Paris
(GMT+01:00) West Central Africa
(GMT+02:00) Windhoek
(GMT+02:00) Athens
(GMT+02:00) Beirut
(GMT+02:00) Cairo
(GMT+02:00) Gaza
(GMT+02:00) Harare, Pretoria
(GMT+02:00) Jerusalem
(GMT+03:00) Minsk
(GMT+03:00) Syria
(GMT+03:00) Moscow, St. Petersburg, Volgograd
(GMT+03:00) Nairobi
(GMT+03:30) Tehran
(GMT+04:00) Abu Dhabi, Muscat
(GMT+04:00) Yerevan
(GMT+04:30) Kabul
(GMT+05:00) Ekaterinburg
(GMT+05:00) Tashkent
(GMT+05:30) Chennai, Kolkata, Mumbai, New Delhi
(GMT+05:45) Kathmandu
(GMT+06:00) Astana, Dhaka
(GMT+07:00) Novosibirsk
(GMT+06:30) Yangon (Rangoon)
(GMT+07:00) Bangkok, Hanoi, Jakarta
(GMT+07:00) Krasnoyarsk
(GMT+08:00) Beijing, Chongqing, Hong Kong, Urumqi
(GMT+08:00) Irkutsk, Ulaan Bataar
(GMT+08:00) Perth
(GMT+08:45) Eucla
(GMT+09:00) Osaka, Sapporo, Tokyo
(GMT+09:00) Seoul
(GMT+09:00) Yakutsk
(GMT+10:30) Adelaide
(GMT+09:30) Darwin
(GMT+10:00) Brisbane
(GMT+11:00) Hobart
(GMT+10:00) Vladivostok
(GMT+11:00) Lord Howe Island
(GMT+11:00) Solomon Is., New Caledonia
(GMT+11:00) Magadan
(GMT+12:00) Norfolk Island
(GMT+12:00) Anadyr, Kamchatka
(GMT+13:00) Auckland, Wellington
(GMT+12:00) Fiji, Kamchatka, Marshall Is.
(GMT+13:45) Chatham Islands
(GMT+13:00) Nuku'alofa
(GMT+14:00) Kiritimati
The GMT offsets shown reflect the offsets
at the moment of the conference
.
Time Band
By setting a time band, the program will dim events that are outside this time window. This is useful for (virtual) conferences with a continuous program (with repeated sessions).
The time band will also limit the events that are included in the personal iCalendar subscription service.
Display full program
Specify a time band
-
Save
×
You're viewing the program in a time zone which is different from your device's time zone
change time zone
Sun 14 Jan
Displayed time zone:
London
change
09:00 - 10:30
Morning Track 2
POPL TutorialFest
at
Marconi Room
09:00
90m
Talk
MetaCoq Tutorial
POPL TutorialFest
Yannick Forster
Inria
,
Meven Lennon-Bertrand
University of Cambridge
,
Matthieu Sozeau
Inria
,
Théo Winterhalter
INRIA Saclay
11:00 - 12:30
Morning Track 2
POPL TutorialFest
at
Marconi Room
11:00
90m
Talk
MetaCoq Tutorial
POPL TutorialFest
Yannick Forster
Inria
,
Meven Lennon-Bertrand
University of Cambridge
,
Matthieu Sozeau
Inria
,
Théo Winterhalter
INRIA Saclay
14:00 - 15:30
Afternoon Track 2
POPL TutorialFest
at
Marconi Room
14:00
90m
Tutorial
String Solving for Verification
POPL TutorialFest
Matthew Hague
Royal Holloway University of London
,
Artur Jez
University of Wroclaw
,
Anthony Widjaja Lin
TU Kaiserslautern; MPI-SWS
,
Philipp Ruemmer
University of Regensburg and Uppsala University
16:00 - 17:30
Afternoon Track 2
POPL TutorialFest
at
Marconi Room
16:00
90m
Tutorial
String Solving for Verification
POPL TutorialFest
Matthew Hague
Royal Holloway University of London
,
Artur Jez
University of Wroclaw
,
Anthony Widjaja Lin
TU Kaiserslautern; MPI-SWS
,
Philipp Ruemmer
University of Regensburg and Uppsala University
Mon 15 Jan
Displayed time zone:
London
change
09:00 - 10:30
Session 1: Openning, Keynote, SAT, SMT and Automated Reasoning
VMCAI
at
Marconi Room
Chair(s):
Rayna Dimitrova
CISPA Helmholtz Center for Information Security
09:00
5m
Day opening
Opening
VMCAI
09:05
60m
Keynote
Two Projects on Human Interaction with AI
VMCAI
David Harel
Weizmann Institute of Science, Israel
10:05
20m
Talk
Interpolation and Quantifiers in Ortholattices
VMCAI
Sankalp Gambhir
Ecole Polytechnique Federale de Lausanne (EPFL)
,
Simon Guilloud
École Polytechnique Fédérale de Lausanne
,
Viktor Kunčak
EPFL, Switzerland
11:00 - 12:30
Session 2: SAT, SMT and Automated Reasoning
VMCAI
at
Marconi Room
Chair(s):
David Monniaux
Université Grenoble Alpes - CNRS - Grenoble INP - Verimag
11:00
20m
Talk
Function synthesis for maximizing model counting
VMCAI
Thomas Vigouroux
VERIMAG - UGA
,
Marius Bozga
CNRS; Université Grenoble Alpes
,
Cristian Ene
Verimag, Grenoble
,
Laurent Mounier
Université Grenoble Alpes
Pre-print
11:20
20m
Talk
Boosting Constrained Horn Solving by Unsat Core Learning
VMCAI
Parosh Aziz Abdulla
Uppsala University, Sweden
,
Chencheng Liang
Uppsala University
,
Philipp Rümmer
University of Regensburg and Uppsala University
11:40
20m
Talk
On the Verification of a Subgraph Construction Algorithm
VMCAI
Lucas Böltz
Univerity of Koblenz
,
Viorica Sofronie-Stokkermans
University of Koblenz
,
Hannes Frey
University of Koblenz
12:00
20m
Talk
Efficient Local Search for Nonlinear Real Arithmetic
VMCAI
Zhonghan Wang
State Key Laboratory of Computer Science, Institute of Software, Chinese Academy of Sciences
,
Bohua Zhan
Institute of Software, Chinese Academy of Sciences
,
Bohan Li
State Key Laboratory of Computer Science Institute of Software, Chinese Academy of Sciences, Beijing, China
,
Shaowei Cai
Institute of Software at Chinese Academy of Sciences
14:00 - 15:30
Session 3: Security and Privacy, Model Checking and Synthesis
VMCAI
at
Marconi Room
Chair(s):
Caterina Urban
Inria & École Normale Supérieure | Université PSL
14:00
20m
Talk
Automatic and Incremental Repair for Speculative Information Leaks
VMCAI
Joachim Bard
CISPA Helmholtz Center for Information Security
,
Swen Jacobs
CISPA
,
Yakir Vizel
Technion—Israel Institute of Technology
14:20
20m
Talk
Sound Abstract Nonexploitability Analysis
VMCAI
Francesco Parolini
Sorbonne Université
,
Antoine Miné
Sorbonne Université
Pre-print
14:40
20m
Talk
Solving Two-Player Games under Progress Assumptions
VMCAI
Anne-Kathrin Schmuck
MPI-SWS
,
K. S. Thejaswini
The University of Warwick
,
Irmak Saglam
Max Planck Institute for Software Systems (MPI-SWS)
,
Satya Prakash Nayak
Max Planck Institute for Software Systems (MPI-SWS)
Pre-print
15:00
20m
Talk
Model-Guided Synthesis for LTL over Finite Traces
VMCAI
Shengping Xiao
East China Normal University
,
Yongkang Li
East China Normal University
,
Xinyue Huang
East China Normal University
,
Yicong Xu
East China Normal University
,
Jianwen Li
East China Normal University, China
,
Geguang Pu
East China Normal University
,
Ofer Strichman
Technion
,
Moshe Vardi
Rice University
15:20
10m
Talk
Generic Model Checking for Modal Fixpoint Logics in COOL-MC
VMCAI
Daniel Hausmann
University of Gothenburg
,
Merlin Humml
Friedrich-Alexander Universität Erlangen-Nürnberg
,
Simon Prucker
Friedrich-Alexander Universität Erlangen-Nürnberg
,
Lutz Schröder
University of Erlangen-Nuremberg
,
Aaron Strahlberger
Friedrich-Alexander-Universität Erlangen-Nürnberg
Pre-print
16:00 - 17:30
Session 4: Infinite State Systems, Runtime Verification
VMCAI
at
Marconi Room
Chair(s):
Helmut Seidl
Technische Universität München
16:00
20m
Talk
Project and Conquer: Fast Quantifier Elimination for Checking Petri Nets Reachability
VMCAI
Nicolas Amat
LAAS-CNRS
,
Silvano DAL ZILIO
LAAS-CNRS
,
Didier Le Botlan
LAAS-CNRS, INSA-Toulouse
Pre-print
16:20
20m
Talk
Parameterized Verification of Disjunctive Timed Networks
Recorded
VMCAI
Étienne André
Université Sorbonne Paris Nord; LIPN; CNRS
,
Paul Eichler
CISPA - Helmholtz Center for Information Security
,
Swen Jacobs
CISPA
,
Shyam Karra
CISPA
16:40
20m
Talk
Resilience and Home-Space for WSTS
VMCAI
Alain Finkel
ENS Paris Saclay
,
Mathieu Hilaire
ENS Paris Saclay
17:00
20m
Talk
Synthesizing Efficiently Monitorable Formulas in Metric Temporal Logic
VMCAI
Ritam Raha
University of Antwerp, Antwerp, Belgium
,
Rajarshi Roy
Max Planck Institute for Software Systems, Kaiserslautern, Germany
,
Nathanaël Fijalkow
CNRS, LaBRI, and Alan Turing Institute
,
Daniel Neider
Technical University of Dortmund, Germany
,
Guillermo A. Perez
University of Antwerp
Pre-print
17:20
10m
Talk
TP-DejaVu: Combining Operational and Declarative Runtime Verification
VMCAI
Klaus Havelund
NASA/Caltech Jet Propulsion Laboratory
,
Panagiotis Katsaros
Aristotle University of Thessaloniki
,
Moran Omer
Bar Ilan University, Israel
,
Doron Peled
Bar Ilan University
,
Anastasios Temperekidis
Aristotle University of Thessaloniki
Tue 16 Jan
Displayed time zone:
London
change
09:00 - 10:30
Session 5: keynote, Program and System Verification
VMCAI
at
Marconi Room
Chair(s):
Ori Lahav
Tel Aviv University
09:00
60m
Keynote
Automating Relational Verification of Infinite-State Programs
VMCAI
Hiroshi Unno
University of Tsukuba
10:00
20m
Talk
Deductive Verification of Parameterized Embedded Systems modeled in SystemC
VMCAI
Philip Tasche
University of Twente
,
Raúl E. Monti
University of Twente
,
Stefanie Eva Drerup
University of Münster
,
Pauline Blohm
Uni Münster
,
Paula Herber
University of Munster, Germany
,
Marieke Huisman
University of Twente
10:20
10m
Talk
Automatically Enforcing Rust Trait Properties
VMCAI
Twain Byrnes
Carnegie Mellon University
,
Yoshiki Takashima
Carnegie Mellon University
,
Limin Jia
Carnegie Mellon University
11:00 - 12:30
Session 6: Abstract Interpretation
VMCAI
at
Marconi Room
Chair(s):
Xavier Rival
Inria; ENS; CNRS; PSL University
11:00
20m
Talk
Formal Runtime Error Detection During Development in the Automotive Industry
VMCAI
Jesko Hecking-Harbusch
Bosch Research
,
Jochen Quante
Bosch Research
,
Maximilian Schlund
Bosch Research
Pre-print
11:20
20m
Talk
Abstract Interpretation-Based Feature Importance for Support Vector Machines
VMCAI
Abhinandan Pal
University of Birmingham
,
Francesco Ranzato
University of Padova
,
Caterina Urban
Inria & École Normale Supérieure | Université PSL
,
Marco Zanella
University of Padova, Italy
11:40
20m
Talk
Generation of Violation Witnesses by Under-Approximating Abstract Interpretation
VMCAI
Marco Milanese
Sorbonne University
,
Antoine Miné
Sorbonne Université
DOI
Pre-print
12:00
20m
Talk
Correctness Witness Validation by Abstract Interpretation
VMCAI
Simmo Saan
University of Tartu, Estonia
,
Michael Schwarz
Technische Universität München
,
Julian Erhard
Technical University of Munich
,
Helmut Seidl
Technische Universität München
,
Sarah Tilscher
Technische Universität München
,
Vesal Vojdani
University of Tartu
DOI
Pre-print
14:00 - 15:30
Session 7: Probabilistic and Quantum Programs, Neural Networks
VMCAI
at
Marconi Room
Chair(s):
Andreas Podelski
University of Freiburg
14:00
20m
Talk
Guaranteed inference for probabilistic programs: a parallelisable, small-step operational approach
VMCAI
Michele Boreale
Università di Firenze
,
Luisa Collodi
University of Florence
14:20
20m
Talk
Local Reasoning about Probabilistic Behaviour for Classical-Quantum Programs
VMCAI
Yuxin Deng
East China Normal University
,
Huiling Wu
East China Normal University
,
Ming Xu
East China Normal University
14:40
20m
Talk
Taming Reachability Analysis of DNN-Controlled Systems via Abstraction-Based Training
VMCAI
Jiaxu Tian
East China Normal University
,
Dapeng Zhi
East China Normal University
,
Si Liu
ETH Zurich
,
Peixin Wang
University of Oxford
,
Guy Katz
Hebrew University
,
Min Zhang
East China Normal University
15:00
20m
Talk
Verification of Neural Networks’ Local Differential Classification Privacy
VMCAI
Roie Reshef
Technion
,
Anan Kabaha
Technion, Israel Institute of Technology
,
Olga Seleznova
Technion
,
Dana Drachsler Cohen
Technion
15:20
10m
Talk
AGNES: Abstraction-guided Framework for Deep Neural Networks Security
VMCAI
Akshay Dhonthi Ramesh Babu
Audi AG
,
Marcello Eiermann
Utrecht University
,
Ernst Moritz Hahn
,
Vahid Hashemi
AUDI AG
16:00 - 17:30
Session 8: Concurrency, Program and System Verification, Closing
VMCAI
at
Marconi Room
Chair(s):
Viktor Kunčak
EPFL, Switzerland
16:00
20m
Talk
Petrification: Software Model Checking for Programs with Dynamic Thread Management
VMCAI
Matthias Heizmann
University of Freiburg, Germany
,
Dominik Klumpp
University of Freiburg
,
Lars Nitzke
University of Freiburg
,
Frank Schüssele
University of Freiburg
Pre-print
16:20
20m
Talk
A Fully Verified Persistency Library
VMCAI
Stefan Bodenmüller
University of Augsburg
,
John Derrick
,
Brijesh Dongol
University of Surrey
,
Gerhard Schellhorn
Universitaet Augsburg
,
Heike Wehrheim
University of Oldenburg
16:40
20m
Talk
A Navigation Logic for Recursive Programs with Dynamic Thread Creation
VMCAI
Roman Lakenbrink
University of Münster
,
Markus Müller-Olm
University of Münster
,
Christoph Ohrem
University of Münster
,
Jens Oliver Gutsfeld
Westfälische Wilhelm-Universität Münster (WWU), Germany
Pre-print
17:00
20m
Talk
Borrowable Fractional Ownership Types for Verification
VMCAI
Takashi Nakayama
The University of Tokyo
,
Yusuke Matsushita
The University of Tokyo
,
Ken Sakayori
University of Tokyo
,
Ryosuke Sato
University of Tokyo
,
Naoki Kobayashi
University of Tokyo
Pre-print
17:20
10m
Day closing
Closing (+ best paper award announcement)
VMCAI
Wed 17 Jan
Displayed time zone:
London
change
11:50 - 13:20
URM Lunch
POPL Diversity, Equity and Inclusion
at
Marconi Room
11:50
90m
Lunch
URM Lunch
POPL Diversity, Equity and Inclusion
Thu 18 Jan
Displayed time zone:
London
change
12:10 - 13:40
LGBTQ@POPL Lunch
POPL Diversity, Equity and Inclusion
at
Marconi Room
12:10
90m
Lunch
LGBTQ+ Lunch
POPL Diversity, Equity and Inclusion
Sat 20 Jan
Displayed time zone:
London
change
09:00 - 10:30
Quantum Types
PLanQC
at
Marconi Room
Chair(s):
Mathys Rennela
INRIA Paris
09:00
45m
Keynote
Monoidal Adventures
PLanQC
Conor McBride
University of Strathclyde
09:45
22m
Talk
Introducing BRAT
PLanQC
Ross Duncan
Quantinuum
,
Mark Koch
Quantinuum
,
Alan Lawrence
Quantinuum
,
Conor McBride
University of Strathclyde
,
Craig Roy
Quantinuum
File Attached
10:07
22m
Talk
Circuit Width Estimation via Effect Typing and Linear Dependency (Extended Abstract)
PLanQC
Andrea Colledan
University of Bologna & INRIA Sophia Antipolis
,
Ugo Dal Lago
University of Bologna & INRIA Sophia Antipolis
11:00 - 12:30
Compilation
PLanQC
at
Marconi Room
Chair(s):
Ross Duncan
Quantinuum
11:00
22m
Talk
Graphical Primitive Recursion For String Diagrams
PLanQC
Zhulien Zhelezchev
University of Bristol
,
Aleks Kissinger
University of Oxford
11:22
22m
Talk
Optimal compilation of parametrised quantum circuits
PLanQC
John van de Wetering
University of Amsterdam
,
Richie Yeung
University of Oxford
,
Tuomas Laakkonen
Quantinuum
,
Aleks Kissinger
University of Oxford
11:45
22m
Talk
Polynomial-time Classical Simulation of Roetteler’s Shifted Bent Function Algorithm
PLanQC
Lucas Stinchcombe
Simon Fraser University
,
Matthew Amy
Simon Fraser University
12:07
22m
Talk
Qadence: a differentiable interface for digital-analog programs
PLanQC
Dominik Seitz
PASQAL SAS
,
Niklas Heim
PASQAL SAS
,
João P. Moutinho
PASQAL SAS
,
Roland Guichard
PASQAL SAS
,
Vytautas Abramavicius
PASQAL SAS
,
Aleksander Wennersteen
PASQAL SAS
,
Gert-Jan Both
PASQAL SAS
,
Mario Dagrada
PASQAL SAS
,
Vincent Elfving
PASQAL SAS
Pre-print
File Attached
14:00 - 15:30
New Directions for Quantum Programming
PLanQC
at
Marconi Room
Chair(s):
Aleks Kissinger
University of Oxford
14:00
22m
Talk
A feasible and unitary programming language with quantum control
PLanQC
Alejandro Díaz-Caro
ICC (UBA-CONICET) & UNQ
,
Emmanuel Hainry
LORIA, Université de Lorraine
,
Romain Péchoux
Université de Lorraine; CNRS; Inria; LORIA
,
Mário Silva
LORIA, Université de Lorraine
14:22
22m
Talk
GUPPY: Pythonic Quantum-Classical Programming
PLanQC
Mark Koch
Quantinuum
,
Alan Lawrence
Quantinuum
,
Kartik Singhal
Quantinuum
,
Seyon Sivarajah
Quantinuum
,
Ross Duncan
Quantinuum
Media Attached
File Attached
14:44
22m
Talk
Quantum and Classical Control (work-in-progress)
remote
PLanQC
Kinnari Dave
Université Paris-Saclay, CNRS, ENS Paris-Saclay, Inria, Laboratoire Méthodes Formelles
,
Louis Lemonnier
Université Paris-Saclay, CNRS, ENS Paris-Saclay, Inria, Laboratoire Méthodes Formelles
,
Romain Péchoux
Université de Lorraine; CNRS; Inria; LORIA
,
Vladimir Zamdzhiev
Inria
16:00 - 17:30
Verification
PLanQC
at
Marconi Room
Chair(s):
Robert Rand
University of Chicago
16:00
22m
Talk
Effect Semantics for Quantum Protocols
PLanQC
Lorenzo Ceragioli
IMT Lucca, Italy
,
Fabio Gadducci
University of Pisa
,
Giuseppe Lomurno
University of Pisa, Italy
,
Gabriele Tedeschi
University of Pisa, Italy
16:22
22m
Talk
QbC: Quantum Correctness by Construction
remote
PLanQC
Anurudh Peduri
Ruhr University Bochum
,
Ina Schaefer
KIT
,
Michael Walter
Ruhr-Universität Bochum
Pre-print
16:45
22m
Talk
Quantum Controlled Measurements via Program Transformation
PLanQC
Kengo Hirata
University of Edinburgh
,
Takeshi Tsukada
Chiba University
File Attached
17:07
22m
Talk
QGAT: A Generate-and-Test Paradigm for Quantum Circuits
PLanQC
Ulrik de Muelenaere
University of Notre Dame
File Attached
Sun 14 Jan
Displayed time zone:
London
change
Room
9:00
30
10:00
30
11:00
30
12:00
30
13:00
30
14:00
30
15:00
30
16:00
30
17:00
30
Marconi Room
POPL TutorialFest
Morning Track 2
POPL TutorialFest
Morning Track 2
POPL TutorialFest
Afternoon Track 2
POPL TutorialFest
Afternoon Track 2
Mon 15 Jan
Displayed time zone:
London
change
Room
9:00
30
10:00
30
11:00
30
12:00
30
13:00
30
14:00
30
15:00
30
16:00
30
17:00
30
Marconi Room
VMCAI
Session 1: Openning, Keynote, SAT, SMT and Automated Reasoning
VMCAI
Session 2: SAT, SMT and Automated Reasoning
VMCAI
Session 3: Security and Privacy, Model Checking and Synthesis
VMCAI
Session 4: Infinite State Systems, Runtime Verification
Tue 16 Jan
Displayed time zone:
London
change
Room
9:00
30
10:00
30
11:00
30
12:00
30
13:00
30
14:00
30
15:00
30
16:00
30
17:00
30
Marconi Room
VMCAI
Session 5: keynote, Program and System Verification
VMCAI
Session 6: Abstract Interpretation
VMCAI
Session 7: Probabilistic and Quantum Programs, Neural Networks
VMCAI
Session 8: Concurrency, Program and System Verification, Closing
Wed 17 Jan
Displayed time zone:
London
change
Room
11:00
30
12:00
30
13:00
30
Marconi Room
POPL Diversity, Equity and Inclusion
URM Lunch
Thu 18 Jan
Displayed time zone:
London
change
Room
12:00
30
13:00
30
Marconi Room
POPL Diversity, Equity and Inclusion
LGBTQ@POPL Lunch
Sat 20 Jan
Displayed time zone:
London
change
Room
9:00
30
10:00
30
11:00
30
12:00
30
13:00
30
14:00
30
15:00
30
16:00
30
17:00
30
Marconi Room
PLanQC
Quantum Types
PLanQC
Compilation
PLanQC
New Directions for Quantum Programming
PLanQC
Verification
Sun 14 Jan
Displayed time zone:
London
change
Room
9:00
15
30
45
10:00
15
30
45
11:00
15
30
45
12:00
15
30
45
13:00
15
30
45
14:00
15
30
45
15:00
15
30
45
16:00
15
30
45
17:00
15
30
45
Marconi Room
POPL TutorialFest
MetaCoq Tutorial
09:00 - 10:30
POPL TutorialFest
MetaCoq Tutorial
11:00 - 12:30
POPL TutorialFest
String Solving for Verification
14:00 - 15:30
POPL TutorialFest
String Solving for Verification
16:00 - 17:30
Mon 15 Jan
Displayed time zone:
London
change
Room
9:00
15
30
45
10:00
15
30
45
11:00
15
30
45
12:00
15
30
45
13:00
15
30
45
14:00
15
30
45
15:00
15
30
45
16:00
15
30
45
17:00
15
30
45
Marconi Room
VMCAI
Opening
09:00 - 09:05
VMCAI
Two Projects on Human Interaction with AI
09:05 - 10:05
VMCAI
Interpolation and Quantifiers in Ortholattices
10:05 - 10:25
VMCAI
Function synthesis for maximizing model counting
11:00 - 11:20
VMCAI
Boosting Constrained Horn Solving by Unsat Core Learning
11:20 - 11:40
VMCAI
On the Verification of a Subgraph Construction Algorithm
11:40 - 12:00
VMCAI
Efficient Local Search for Nonlinear Real Arithmetic
12:00 - 12:20
VMCAI
Automatic and Incremental Repair for Speculative Information Leaks
14:00 - 14:20
VMCAI
Sound Abstract Nonexploitability Analysis
14:20 - 14:40
VMCAI
Solving Two-Player Games under Progress Assumptions
14:40 - 15:00
VMCAI
Model-Guided Synthesis for LTL over Finite Traces
15:00 - 15:20
VMCAI
Generic Model Checking for Modal Fixpoint Logics in COOL-MC
15:20 - 15:30
VMCAI
Project and Conquer: Fast Quantifier Elimination for Checking Petri Net ...
16:00 - 16:20
VMCAI
Recorded
Parameterized Verification of Disjunctive Timed Networks
16:20 - 16:40
VMCAI
Resilience and Home-Space for WSTS
16:40 - 17:00
VMCAI
Synthesizing Efficiently Monitorable Formulas in Metric Temporal Logic
17:00 - 17:20
VMCAI
TP-DejaVu: Combining Operational and Declarative Runtime Verification
17:20 - 17:30
Tue 16 Jan
Displayed time zone:
London
change
Room
9:00
15
30
45
10:00
15
30
45
11:00
15
30
45
12:00
15
30
45
13:00
15
30
45
14:00
15
30
45
15:00
15
30
45
16:00
15
30
45
17:00
15
30
45
Marconi Room
VMCAI
Automating Relational Verification of Infinite-State Programs
09:00 - 10:00
VMCAI
Deductive Verification of Parameterized Embedded Systems modeled in SystemC
10:00 - 10:20
VMCAI
Automatically Enforcing Rust Trait Properties
10:20 - 10:30
VMCAI
Formal Runtime Error Detection During Development in the Automotive Ind ...
11:00 - 11:20
VMCAI
Abstract Interpretation-Based Feature Importance for Support Vector Mac ...
11:20 - 11:40
VMCAI
Generation of Violation Witnesses by Under-Approximating Abstract Inter ...
11:40 - 12:00
VMCAI
Correctness Witness Validation by Abstract Interpretation
12:00 - 12:20
VMCAI
Guaranteed inference for probabilistic programs: a parallelisable, smal ...
14:00 - 14:20
VMCAI
Local Reasoning about Probabilistic Behaviour for Classical-Quantum Pro ...
14:20 - 14:40
VMCAI
Taming Reachability Analysis of DNN-Controlled Systems via Abstraction- ...
14:40 - 15:00
VMCAI
Verification of Neural Networks’ Local Differential Classification Privacy
15:00 - 15:20
VMCAI
AGNES: Abstraction-guided Framework for Deep Neural Networks Security
15:20 - 15:30
VMCAI
Petrification: Software Model Checking for Programs with Dynamic Thread ...
16:00 - 16:20
VMCAI
A Fully Verified Persistency Library
16:20 - 16:40
VMCAI
A Navigation Logic for Recursive Programs with Dynamic Thread Creation
16:40 - 17:00
VMCAI
Borrowable Fractional Ownership Types for Verification
17:00 - 17:20
VMCAI
Closing (+ best paper award announcement)
17:20 - 17:30
Wed 17 Jan
Displayed time zone:
London
change
Room
11:00
15
30
45
12:00
15
30
45
13:00
15
30
45
Marconi Room
POPL Diversity, Equity and Inclusion
URM Lunch
11:50 - 13:20
Thu 18 Jan
Displayed time zone:
London
change
Room
12:00
15
30
45
13:00
15
30
45
Marconi Room
POPL Diversity, Equity and Inclusion
LGBTQ+ Lunch
12:10 - 13:40
Sat 20 Jan
Displayed time zone:
London
change
Room
9:00
15
30
45
10:00
15
30
45
11:00
15
30
45
12:00
15
30
45
13:00
15
30
45
14:00
15
30
45
15:00
15
30
45
16:00
15
30
45
17:00
15
30
45
Marconi Room
PLanQC
Monoidal Adventures
09:00 - 09:45
PLanQC
Introducing BRAT
09:45 - 10:07
PLanQC
Circuit Width Estimation via Effect Typing and Linear Dependency (Exten ...
10:07 - 10:29
PLanQC
Graphical Primitive Recursion For String Diagrams
11:00 - 11:22
PLanQC
Optimal compilation of parametrised quantum circuits
11:22 - 11:45
PLanQC
Polynomial-time Classical Simulation of Roetteler’s Shifted Bent Functi ...
11:45 - 12:07
PLanQC
Qadence: a differentiable interface for digital-analog programs
12:07 - 12:30
PLanQC
A feasible and unitary programming language with quantum control
14:00 - 14:22
PLanQC
GUPPY: Pythonic Quantum-Classical Programming
14:22 - 14:44
PLanQC
remote
Quantum and Classical Control (work-in-progress)
14:44 - 15:06
PLanQC
Effect Semantics for Quantum Protocols
16:00 - 16:22
PLanQC
remote
QbC: Quantum Correctness by Construction
16:22 - 16:45
PLanQC
Quantum Controlled Measurements via Program Transformation
16:45 - 17:07
PLanQC
QGAT: A Generate-and-Test Paradigm for Quantum Circuits
17:07 - 17:30
x
Mon 30 Dec 18:21