POPL 2024
Sun 14 - Sat 20 January 2024 London, United Kingdom

Runtime verification (RV) facilitates monitoring the executions of a system, comparing them against a formal specification. A main challenge is to keep the incremental complexity of updating its internal structure, each time a new event is inspected, to a minimum. There is a tradeoff between achieving a low incremental complexity and the expressive power of the used specification formalism. We seek an RV tool that allows us to specify properties of executions that include data, with the possibility to apply arithmetic operations and comparisons on the data values. In order to be able to apply efficient RV for specifications with these capabilities we combine two RV methodologies: the first one is capable of performing arithmetic operations and comparisons based on the most recent events; the second is capable of handling many events with data and relating between events that occur at arbitrary distance in the observed execution. This is done by two phase RV, where the first phase makes the arithmetic calculations and comparisons and feeds the second phase with augmented events for further processing. This is implemented as a tool called TP-DejaVu (where TP stands for two phase), which extends the DejaVu tool.

Mon 15 Jan

Displayed time zone: London change

16:00 - 17:30
Session 4: Infinite State Systems, Runtime VerificationVMCAI at Marconi Room
Chair(s): Helmut Seidl Technische Universität München
16:00
20m
Talk
Project and Conquer: Fast Quantifier Elimination for Checking Petri Nets Reachability
VMCAI
Nicolas Amat LAAS-CNRS, Silvano DAL ZILIO LAAS-CNRS, Didier Le Botlan LAAS-CNRS, INSA-Toulouse
Pre-print
16:20
20m
Talk
Parameterized Verification of Disjunctive Timed NetworksRecorded
VMCAI
Étienne André Université Sorbonne Paris Nord; LIPN; CNRS, Paul Eichler CISPA - Helmholtz Center for Information Security, Swen Jacobs CISPA, Shyam Karra CISPA
16:40
20m
Talk
Resilience and Home-Space for WSTS
VMCAI
Alain Finkel ENS Paris Saclay, Mathieu Hilaire ENS Paris Saclay
17:00
20m
Talk
Synthesizing Efficiently Monitorable Formulas in Metric Temporal Logic
VMCAI
Ritam Raha University of Antwerp, Antwerp, Belgium, Rajarshi Roy Max Planck Institute for Software Systems, Kaiserslautern, Germany, Nathanaël Fijalkow CNRS, LaBRI, and Alan Turing Institute, Daniel Neider Technical University of Dortmund, Germany, Guillermo A. Perez University of Antwerp
Pre-print
17:20
10m
Talk
TP-DejaVu: Combining Operational and Declarative Runtime Verification
VMCAI
Klaus Havelund NASA/Caltech Jet Propulsion Laboratory, Panagiotis Katsaros Aristotle University of Thessaloniki, Moran Omer Bar Ilan University, Israel, Doron Peled Bar Ilan University, Anastasios Temperekidis Aristotle University of Thessaloniki