POPL 2025 (series) / VMCAI 2025 (series) /
VMCAI 2025 Program
This is the VMCAI 2025 program - see the full program for POPL 2025 and all affiliated events.
Filter Program
Dates
Rooms
Tracks
Badges
Your Program
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 | Keynote Talk and Cyber-Physical SystemsVMCAI 2025 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 2025 Jyotirmoy Deshmukh University of Southern California | ||
10:00 30mTalk | Synthesis of Controllers for Continuous Blackbox Systems VMCAI 2025 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 |
11:00 - 12:30 | |||
11:00 30mTalk | Affine Disjunctive Invariant Generation with Farkas’ Lemma VMCAI 2025 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 2025 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 2025 Nicola Assolini University of Verona, Alessandra Di Pierro University of Verona, Isabella Mastroeni University of Verona |
14:00 - 15:30 | |||
14:00 30mTalk | Space-Efficient Model-Checking of Higher-Order Recursion Schemes VMCAI 2025 Florian Bruse University of Kassel | ||
14:30 30mTalk | Parameterized Verification of Systems with Precise (0,1)-Counter Abstraction VMCAI 2025 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 2025 |
16:00 - 17:30 | |||
16:00 30mTalk | ExpectAll: A BDD Based Approach for Link Failure Resilience in Elastic Optical Networks VMCAI 2025 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 2025 | ||
17:00 30mTalk | Automated Flaw Detection for Industrial Robot RESTful ServiceRecorded VMCAI 2025 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 Media Attached |
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 | Keynote Talk (Tuesday) and LearningVMCAI 2025 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 2025 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 2025 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 |
11:00 - 12:30 | |||
11:00 30mTalk | A Real-Blasting Extension of Cvc5 for Reasoning about Floating-Point Arithmetic VMCAI 2025 Daisuke Ishii JAIST | ||
11:30 30mTalk | Formally Verifiable Generated ASN.1/ACN Encoders and Decoders: A Case Study VMCAI 2025 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 2025 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 |
14:00 - 15:30 | |||
14:00 30mTalk | Abstract Local Completeness: A Local form of Abstract Non-Interference VMCAI 2025 Isabella Mastroeni University of Verona | ||
14:30 30mTalk | An Abstract Domain for Heap Commutativity VMCAI 2025 | ||
15:00 30mTalk | Two-way collaboration between flow and proof in SPARK VMCAI 2025 |
16:00 - 17:30 | ConcurrencyVMCAI 2025 at Hopscotch Chair(s): Sriram Sankaranarayanan University of Colorado, Boulder | ||
16:00 30mTalk | LLOR: Automated Repair of OpenMP Programs VMCAI 2025 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 2025 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 2025 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 |