TP-DejaVu: Combining Operational and Declarative Runtime Verification
summary
Extends DejaVu with a two-phase pipeline: an operational preprocessor (Lola-like) that computes comparisons and aggregations on recent events and augments them, followed by declarative past-time first‑order RV implemented in DejaVu. Core encoding uses BDDs and enumeration binary encoding for subformula relations. Evaluation processes traces up to 5 million events, showing TP-DejaVu continues where vanilla DejaVu times out and runs noticeably faster for properties that only need recent-value comparisons or running aggregates; it still cannot efficiently handle properties requiring scanning all past values.
AI-written summary · about
chapters (10)
- 0:00TP-DejaVu introduction
- 2:50Runtime verification basics
- 5:19BDD summary encoding
- 7:25Two-stage verification
- 9:14TP-DejaVu implementation
- 10:41Example properties
- 11:24Performance vs DejaVu
- 12:08Time model & satisfiability
- 13:11Motivation for properties
- 14:12Q&A
related talks
45mRV: where are we?
18mToward Repository-Level Program Verification with Large Language Models
14mScalability and Precision by Combining Expressive Type Systems and Deductive Verification
26mAutomatic Rollback Suggestions for Incremental Datalog Evaluation
52mThink Abstractly, Work Concretely
28mGradual Verification: Assuring Software Incrementally
23mSpecifying and Verifying Future Conditions
15mAbstract Interpretation of Temporal Safety Effects of Higher Order Programs