ATVA 2025
Mon 27 - Fri 31 October 2025 Bengaluru, India

This program is tentative and subject to change.

Tue 28 Oct 2025 14:30 - 15:00 at R102 - Verification I Chair(s): Kartik Nagar

Parametric Markov chains (pMCs) are Markov chains (MCs) with symbolic probabilities. A pMC encodes a family of MCs, where each member is obtained by replacing parameters with constants. The parameters allow encoding dependencies between transitions, which sets pMCs apart from interval MCs. The verification problem for pMCs asks whether each MC in the corresponding family satisfies a given temporal specification. The state-of-the-art approach for this problem is parameter lifting (PL)—an abstraction-refinement loop that abstracts the pMC to a non-parametric model analyzed with standard probabilistic model checking techniques. This paper presents two key improvements to tackle the main limitations of PL. First, we introduce generalized parameter lifting (GPL) to lift various restrictive assumptions made by PL. Second, we present a big-step transformation algorithm that reduces parameter dependencies in pMCs and, therefore, results in tighter approximations. Experiments show that GPL is widely applicable and that the big-step transformation accelerates pMC verification by up to orders of magnitude.

This program is tentative and subject to change.

Tue 28 Oct

Displayed time zone: Chennai, Kolkata, Mumbai, New Delhi change

14:00 - 15:30
Verification IATVA Papers at R102
Chair(s): Kartik Nagar IIT Madras
14:00
30m
Paper
Data Structures for Finite Downsets of Natural Vectors: Theory and Practice
ATVA Papers
Michaël Cadilhac , Vanessa Fluegel University of Antwerp, Antwerp, Belgium, Guillermo A. Perez University of Antwerp, Shrisha Rao University of Antwerp, Antwerp, Belgium
14:30
30m
Paper
Generalized Parameter Lifting: Finer Abstractions for Parametric Markov Chains
ATVA Papers
Linus Heck Radboud University, Tim Quatmann RWTH Aachen University, Jip Spel RWTH Aachen University, Joost-Pieter Katoen RWTH Aachen University, Sebastian Junges Radboud University
15:00
30m
Paper
Antarbhukti: Verifying Correctness of PLC Software during System Evolution
ATVA Papers
Soumyadip Bandyopadhyay ACM Member, Santonu Sarkar BITS Pilani, India
Pre-print
Hide past events