VMCAI 2025
Mon 20 - Tue 21 January 2025 Denver, Colorado, United States
co-located with POPL 2025
You're viewing the program in a time zone which is different from your device's time zone change time zone

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
60m
Talk
Keynote Talk: Formal methods in a model-free, data-driven world
VMCAI 2025
Jyotirmoy Deshmukh University of Southern California
10:00
30m
Talk
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
Abstract Interpretation # 1VMCAI 2025 at Hopscotch
Chair(s): Kedar Namjoshi Nokia Bell Labs
11:00
30m
Talk
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
30m
Talk
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
30m
Talk
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
Model CheckingVMCAI 2025 at Hopscotch
Chair(s): Arie Gurfinkel University of Waterloo
14:00
30m
Talk
Space-Efficient Model-Checking of Higher-Order Recursion Schemes
VMCAI 2025
Florian Bruse University of Kassel
14:30
30m
Talk
Parameterized Verification of Systems with Precise (0,1)-Counter AbstractionRemote
VMCAI 2025
Paul Eichler CISPA - Helmholtz Center for Information Security, Swen Jacobs CISPA, Chana Weil-Kennedy IMDEA Software Institute
15:00
30m
Talk
Property-agnostic base case extension for scalable verification of distributed systems
VMCAI 2025
Kyle Storey Brigham Young University, Eric Mercer Brigham Young University
16:00 - 17:30
ApplicationsVMCAI 2025 at Hopscotch
Chair(s): Jyotirmoy Deshmukh University of Southern California
16:00
30m
Talk
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
30m
Talk
Constructing Trustworthy Smart Contracts
VMCAI 2025
Devora Chait-Roth New York University, Kedar Namjoshi Nokia Bell Labs
17:00
30m
Talk
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 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
60m
Talk
Keynote Talk: Outcome Logic: a foundational framework for concurrent and probabilistic program analysis
VMCAI 2025
Alexandra Silva Cornell University
10:00
30m
Talk
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
VerificationVMCAI 2025 at Hopscotch
Chair(s): Isabella Mastroeni University of Verona
11:00
30m
Talk
A Real-Blasting Extension of Cvc5 for Reasoning about Floating-Point Arithmetic
VMCAI 2025
11:30
30m
Talk
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
30m
Talk
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
Abstract Interpretation # 2VMCAI 2025 at Hopscotch
Chair(s): Alexandra Silva Cornell University
14:00
30m
Talk
Abstract Local Completeness: A Local form of Abstract Non-Interference
VMCAI 2025
Isabella Mastroeni University of Verona
14:30
30m
Talk
An Abstract Domain for Heap Commutativity
VMCAI 2025
Jared Pincus Boston University, Eric Koskinen Stevens Institute of Technology
15:00
30m
Talk
Two-way collaboration between flow and proof in SPARK
VMCAI 2025
Claire Dross AdaCore, Joffrey Huguet AdaCore, Johannes Kanig AdaCore
16:00 - 17:30
ConcurrencyVMCAI 2025 at Hopscotch
Chair(s): Sriram Sankaranarayanan University of Colorado, Boulder
16:00
30m
Talk
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
30m
Talk
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
30m
Talk
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