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

This program is tentative and subject to change.

Mon 27 Oct 2025 11:00 - 11:30 at R102 - NIER 2

Complex systems often exhibit multiple behavioural requirements that span different contexts, safety goals, and performance metrics. However, not all requirements share the same level of criticality or compatibility. Some must always be satisfied to ensure safety or correctness, while others may be only desirable under certain conditions. This diversity in importance and compatibility must be carefully considered when designing the system and during its execution. These behavioural requirements are commonly expressed as formal properties. Runtime verification and enforcement frameworks are employed to monitor whether these properties hold over system executions. When violations are detected, enforcement mechanisms must intervene by correcting the system’s executions to bring the execution in line with the specified properties before it is passed on to other components or subsystems. This ensures that the system continues to function within acceptable bounds, even in the presence of deviations or unforeseen behaviours.

Runtime enforcement strategies exhibit a broad design space, capable of handling multiple properties. A common approach is to treat all properties as equally important and enforce them simultaneously. However, depending on the application’s requirements, it may be necessary to adopt alternative enforcement methods that account for the criticality or compatibility of properties. This prevents enforcement conflicts and reduces computational inefficiencies. In this work, we introduce categories of properties based on their enforcement requirements and propose tailored, practical enforcement strategies for each category, thereby improving enforcement efficiency. Thus, when presented with multiple properties, organized in categories, we are able to generate a customized enforcer that respects the context of each category, ensuring that the properties are enforced in a manner aligned with their individual enforcement semantics. We call this framework Context-Aware Runtime Enforcement framework.

This program is tentative and subject to change.

Mon 27 Oct

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

11:00 - 12:30
NIER 2NIER at R102
11:00
30m
Talk
Property Grouping and Context-Aware Runtime Enforcement
NIER
Saumya Shankar International Institute of Information Technology Bangalore, Srinivas Pinisetty Indian Institute of Technology Bhubaneswar, Thierry Jéron INRIA
11:30
30m
Talk
Compositional Probabilistic Model Checking with String Diagrams of MDPs 
NIER
Ichiro Hasuo National Institute of Informatics, Japan
12:00
30m
Talk
PhantomDrive: A Privacy-Focused Navigation System for Concealing User Movements
NIER
Inzemamul Haque Indian Institute of Technology Kanpur, Pankaj Siwan , Indranil Saha IIT Kanpur
Hide past events