Paper Info
Title
BDDs on the Run.
Abstract
Runtime verification (RV) of first-order temporal logic must handle a potentially large amount of data, accumulated during the monitoring of an execution. The DejaVu RV system represents data elements and relations using BDDs. This achieves a compact representation, which allows monitoring long executions. However, the potentially unbounded, and frequently very large amounts of data values can, ultimately, limit the executions that can be monitored. We present an automatic method for “forgetting” data values when they no longer affect the RV verdict on an observed execution. We describe the algorithm and illustrate its operation through an example.
Year
Venue
Field
2018
ISoLA
Forgetting,Computer science,Parallel computing,Runtime verification,Temporal logic
DocType
Citations 
PageRank 
Conference
1
0.35
References 
Authors
11
2
Name
Order
Citations
PageRank
Klaus Havelund13522254.55
Doron Peled23357273.18