Publikation
Verification Runtime Analysis: Get the Most Out of Partial Verification
Martin Ring; Fritjof Bornebusch; Christoph Lüth; Robert Wille; Rolf Drechsler
In: Design, Automation & Test in Europe. Design, Automation & Test in Europe (DATE-2020), March 9-13, Grenoble, France, IEEE, 2020.
Zusammenfassung
The design of modern systems has reached a complexity which makes it
inevitable to apply verification methods in order to guarantee its
correct and safe execution. The verification methods frequently
produce proof obligations that can not be solved any more due to
the huge search space. However, by setting enough variables to fixed
values, the search space is obviously reduced and solving engines
eventually may be able to complete the verification task. Although
this results in a \emph{partial verification}, the results may still
be valuable --- in particular as opposed to the alternative of no
verification at all. However, so far no systematic investigation has
been conducted on which variables to fix in order to reduce
verification runtime as much as possible while, at the same time,
still getting most coverage. This paper addresses this question by
proposing a corresponding verification runtime
analysis. Experimental evaluations confirm the potential of this
approach.