In: Design, Automation & Test in Europe. Design, Automation & Test in Europe (DATE-2020) March 9-13 Grenoble France IEEE 2020.
Abstract
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.
@inproceedings{pub11457,
author = {
Ring, Martin
and
Bornebusch, Fritjof
and
Lüth, Christoph
and
Wille, Robert
and
Drechsler, Rolf
},
title = {Verification Runtime Analysis: Get the Most Out of Partial Verification},
booktitle = {Design, Automation & Test in Europe. Design, Automation & Test in Europe (DATE-2020), March 9-13, Grenoble, France},
year = {2020},
publisher = {IEEE}
}
German Research Center for Artificial Intelligence Deutsches Forschungszentrum für Künstliche Intelligenz
