VMCAI 2025

21 papers

1. 1-2-3-Go! Policy Synthesis for Parameterized Markov Decision Processes via Decision-Tree Learning and Generalization · Muqsit Azeem, Debraj Chakraborty, Sudeep Kanav, Jan Kretínský, MohammadSadegh Mohagheghi, Stefanie Mohr + 1 more
2. A Real-Blasting Extension of cvc5 for Reasoning About Floating-Point Arithmetic · Daisuke Ishii
3. A Static Analysis of Entanglement · Nicola Assolini, Alessandra Di Pierro, Isabella Mastroeni
4. Abstract Local Completeness - A Local Form of Abstract Non-interference · Isabella Mastroeni
5. Affine Disjunctive Invariant Generation with Farkas' Lemma · Jingyu Ke, Hongfei Fu, Hongming Liu, Zhouyue Sun, Liqian Chen, Guoqiang Li
6. An Abstract Domain for Heap Commutativity · Jared Pincus, Eric Koskinen
7. Automated Flaw Detection for Industrial Robot RESTful Service · Yuncheng Wang, Puzhuo Liu, Yaowen Zheng, Dongliang Fang, Shuaizong Si, Zhiwen Pan + 2 more
8. Automatic Inference of Relational Object Invariants · Yusen Su, Jorge A. Navas, Arie Gurfinkel, Isabel Garcia-Contreras
9. Constructing Trustworthy Smart Contracts · Devora Chait-Roth, Kedar S. Namjoshi
10. Correctness Witnesses for Concurrent Programs: Bridging the Semantic Divide with Ghosts · Julian Erhard, Manuel Bentele, Matthias Heizmann, Dominik Klumpp, Simmo Saan, Frank Schüssele + 4 more
11. Discovering Likely Invariants for Distributed Systems Through Runtime Monitoring and Learning · Yuan Xia, Deepayan Sur, Aabha Shailesh Pingle, Jyotirmoy V. Deshmukh, Mukund Raghothaman, Srivatsan Ravi
12. ExpectAll: A BDD Based Approach for Link Failure Resilience in Elastic Optical Networks · Gustav S. Bruhns, Martin P. Hansen, Rasmus Hebsgaard, Frederik M. W. Hyldgaard, Jirí Srba
13. Formal Verification of Probabilistic Deep Reinforcement Learning Policies with Abstract Training · Junfeng Yang, Min Zhang, Xin Chen, Qin Li
14. Formally Verifiable Generated ASN.1/ACN Encoders and Decoders: A Case Study · Mario Bucev, Samuel Chassot, Simon Felix, Filip Schramka, Viktor Kuncak
15. LLOR: Automated Repair of OpenMP Programs · Utpal Bora, Saurabh Joshi, Gautam Muduganti, Ramakrishna Upadrasta
16. Parameterized Verification of Systems with Precise (0,1)-Counter Abstraction · Paul Eichler, Swen Jacobs, Chana Weil-Kennedy
17. Property-Agnostic Base Case Extension for Scalable Verification of Distributed Systems · Kyle Storey, Eric Mercer
18. Space-Efficient Model-Checking of Higher-Order Recursion Schemes · Florian Bruse
19. Synthesis of Controllers for Continuous Blackbox Systems · Benedikt Maderbacher, Felix Windisch, Alberto Larrauri, Roderick Bloem
20. Synthesis of Parametric Locally Symmetric Protocols from Abstract Temporal Specifications · Ruoxi Zhang, Richard J. Trefler, Kedar S. Namjoshi
21. Two-Way Collaboration Between Flow and Proof in SPARK · Claire Dross, Joffrey Huguet, Johannes Kanig