POPL 2024 (series) / VMCAI 2024 (series) /
VMCAI 2024 Program
This is the VMCAI 2024 program - see the full program for POPL 2024 and all affiliated events.
Filter Program
Dates
Rooms
Tracks
Badges
Your Program
Sun 14 JanDisplayed time zone: London change
Sun 14 Jan
Displayed time zone: London change
10:30 - 11:00 | |||
10:30 30mCoffee break | Break Catering | ||
10:30 - 11:00 | |||
10:30 30mCoffee break | Break Catering | ||
12:30 - 14:00 | |||
12:30 90mLunch | Lunch Catering | ||
12:30 - 14:00 | |||
12:30 90mLunch | Lunch Catering | ||
15:30 - 16:00 | |||
15:30 30mCoffee break | Break Catering | ||
15:30 - 16:00 | |||
15:30 30mCoffee break | Break Catering | ||
Mon 15 JanDisplayed time zone: London change
Mon 15 Jan
Displayed time zone: London change
09:00 - 10:30 | Session 1: Openning, Keynote, SAT, SMT and Automated ReasoningVMCAI at Marconi Room Chair(s): Rayna Dimitrova CISPA Helmholtz Center for Information Security | ||
09:00 5mDay opening | Opening VMCAI | ||
09:05 60mKeynote | Two Projects on Human Interaction with AI VMCAI David Harel Weizmann Institute of Science, Israel | ||
10:05 20mTalk | Interpolation and Quantifiers in Ortholattices VMCAI Sankalp Gambhir Ecole Polytechnique Federale de Lausanne (EPFL), Simon Guilloud École Polytechnique Fédérale de Lausanne, Viktor Kunčak EPFL, Switzerland | ||
10:30 - 11:00 | |||
10:30 30mCoffee break | Break Catering | ||
11:00 - 12:30 | Session 2: SAT, SMT and Automated ReasoningVMCAI at Marconi Room Chair(s): David Monniaux Université Grenoble Alpes - CNRS - Grenoble INP - Verimag | ||
11:00 20mTalk | Function synthesis for maximizing model counting VMCAI Thomas Vigouroux VERIMAG - UGA, Marius Bozga CNRS; Université Grenoble Alpes, Cristian Ene Verimag, Grenoble, Laurent Mounier Université Grenoble Alpes Pre-print | ||
11:20 20mTalk | Boosting Constrained Horn Solving by Unsat Core Learning VMCAI Parosh Aziz Abdulla Uppsala University, Sweden, Chencheng Liang Uppsala University, Philipp Rümmer University of Regensburg and Uppsala University | ||
11:40 20mTalk | On the Verification of a Subgraph Construction Algorithm VMCAI Lucas Böltz Univerity of Koblenz, Viorica Sofronie-Stokkermans University of Koblenz, Hannes Frey University of Koblenz | ||
12:00 20mTalk | Efficient Local Search for Nonlinear Real Arithmetic VMCAI Zhonghan Wang Institute of Software/CAS China, 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 | ||
12:30 - 14:00 | |||
12:30 90mLunch | Lunch Catering | ||
14:00 - 15:30 | Session 3: Security and Privacy, Model Checking and SynthesisVMCAI at Marconi Room Chair(s): Caterina Urban Inria & École Normale Supérieure | Université PSL | ||
14:00 20mTalk | Automatic and Incremental Repair for Speculative Information Leaks VMCAI Joachim Bard CISPA Helmholtz Center for Information Security, Swen Jacobs CISPA, Yakir Vizel Technion—Israel Institute of Technology | ||
14:20 20mTalk | Sound Abstract Nonexploitability Analysis VMCAI Pre-print | ||
14:40 20mTalk | Solving Two-Player Games under Progress Assumptions VMCAI Anne-Kathrin Schmuck MPI-SWS, K. S. Thejaswini The University of Warwick, Irmak Saglam Max Planck Institute for Software Systems (MPI-SWS), Satya Prakash Nayak Max Planck Institute for Software Systems (MPI-SWS) Pre-print | ||
15:00 20mTalk | Model-Guided Synthesis for LTL over Finite Traces VMCAI Shengping Xiao East China Normal University, Yongkang Li East China Normal University, Xinyue Huang East China Normal University, Yicong Xu East China Normal University, Jianwen Li East China Normal University, China, Geguang Pu East China Normal University, Ofer Strichman Technion, Moshe Vardi Rice University | ||
15:20 10mTalk | Generic Model Checking for Modal Fixpoint Logics in COOL-MC VMCAI Daniel Hausmann University of Gothenburg, Merlin Humml Friedrich-Alexander Universität Erlangen-Nürnberg, Simon Prucker Friedrich-Alexander Universität Erlangen-Nürnberg, Lutz Schröder University of Erlangen-Nuremberg, Aaron Strahlberger Friedrich-Alexander-Universität Erlangen-Nürnberg Pre-print | ||
15:30 - 16:00 | |||
15:30 30mCoffee break | Break Catering | ||
16:00 - 17:30 | Session 4: Infinite State Systems, Runtime VerificationVMCAI at Marconi Room Chair(s): Helmut Seidl Technische Universität München | ||
16:00 20mTalk | Project and Conquer: Fast Quantifier Elimination for Checking Petri Nets Reachability VMCAI Pre-print | ||
16:20 20mTalk | Parameterized Verification of Disjunctive Timed NetworksRecorded VMCAI Étienne André Université Sorbonne Paris Nord; LIPN; CNRS, Paul Eichler CISPA - Helmholtz Center for Information Security, Swen Jacobs CISPA, Shyam Karra CISPA | ||
16:40 20mTalk | Resilience and Home-Space for WSTS VMCAI | ||
17:00 20mTalk | Synthesizing Efficiently Monitorable Formulas in Metric Temporal Logic VMCAI Ritam Raha University of Antwerp, Antwerp, Belgium, Rajarshi Roy Max Planck Institute for Software Systems, Kaiserslautern, Germany, Nathanaël Fijalkow CNRS, LaBRI, and Alan Turing Institute, Daniel Neider Technical University of Dortmund, Germany, Guillermo A. Perez University of Antwerp Pre-print | ||
17:20 10mTalk | TP-DejaVu: Combining Operational and Declarative Runtime Verification VMCAI Klaus Havelund NASA/Caltech Jet Propulsion Laboratory, Panagiotis Katsaros Aristotle University of Thessaloniki, Moran Omer Bar Ilan University, Israel, Doron Peled Bar Ilan University, Anastasios Temperekidis Aristotle University of Thessaloniki | ||
Tue 16 JanDisplayed time zone: London change
Tue 16 Jan
Displayed time zone: London change
09:00 - 10:30 | Session 5: keynote, Program and System VerificationVMCAI at Marconi Room Chair(s): Ori Lahav Tel Aviv University | ||
09:00 60mKeynote | Automating Relational Verification of Infinite-State Programs VMCAI Hiroshi Unno University of Tsukuba | ||
10:00 20mTalk | Deductive Verification of Parameterized Embedded Systems modeled in SystemC VMCAI Philip Tasche University of Twente, Raúl E. Monti University of Twente, Stefanie Eva Drerup University of Münster, Pauline Blohm Uni Münster, Paula Herber University of Munster, Germany, Marieke Huisman University of Twente | ||
10:20 10mTalk | Automatically Enforcing Rust Trait Properties VMCAI Twain Byrnes Carnegie Mellon University, Yoshiki Takashima Carnegie Mellon University, Limin Jia Carnegie Mellon University | ||
10:30 - 11:00 | |||
10:30 - 11:00 | |||
10:30 30mCoffee break | Break Catering | ||
12:30 - 14:00 | |||
12:30 90mLunch | Lunch Catering | ||
12:30 - 14:00 | |||
12:30 90mLunch | Lunch Catering | ||
15:30 - 16:00 | |||
15:30 30mCoffee break | Break Catering | ||
15:30 - 16:00 | |||
15:30 30mCoffee break | Break Catering | ||
16:00 - 17:30 | Session 8: Concurrency, Program and System Verification, ClosingVMCAI at Marconi Room Chair(s): Viktor Kunčak EPFL, Switzerland | ||
16:00 20mTalk | Petrification: Software Model Checking for Programs with Dynamic Thread Management VMCAI Matthias Heizmann University of Freiburg, Germany, Dominik Klumpp University of Freiburg, Lars Nitzke University of Freiburg, Frank Schüssele University of Freiburg Pre-print | ||
16:20 20mTalk | A Fully Verified Persistency Library VMCAI Stefan Bodenmüller University of Augsburg, John Derrick , Brijesh Dongol University of Surrey, Gerhard Schellhorn Universitaet Augsburg, Heike Wehrheim University of Oldenburg | ||
16:40 20mTalk | A Navigation Logic for Recursive Programs with Dynamic Thread Creation VMCAI Roman Lakenbrink University of Münster, Markus Müller-Olm University of Münster, Christoph Ohrem University of Münster, Jens Oliver Gutsfeld Westfälische Wilhelm-Universität Münster (WWU), Germany Pre-print | ||
17:00 20mTalk | Borrowable Fractional Ownership Types for Verification VMCAI Takashi Nakayama The University of Tokyo, Yusuke Matsushita The University of Tokyo, Ken Sakayori University of Tokyo, Ryosuke Sato University of Tokyo, Naoki Kobayashi University of Tokyo Pre-print | ||
17:20 10mDay closing | Closing (+ best paper award announcement) VMCAI | ||
Sat 20 JanDisplayed time zone: London change
Sat 20 Jan
Displayed time zone: London change
10:30 - 11:00 | |||
10:30 30mCoffee break | Break Catering | ||
10:30 - 11:00 | |||
10:30 30mCoffee break | Break Catering | ||
10:30 - 11:00 | |||
10:30 30mCoffee break | Break Catering | ||
12:30 - 14:00 | |||
12:30 90mLunch | Lunch Catering | ||
12:30 - 14:00 | |||
12:30 - 14:00 | |||
12:30 90mLunch | Lunch Catering | ||
15:30 - 16:00 | |||
15:30 30mCoffee break | Break Catering | ||
15:30 - 16:00 | |||
15:30 30mCoffee break | Break Catering | ||
15:30 - 16:00 | |||
15:30 30mCoffee break | Break Catering | ||