Gesellschaft für Informatik e.V.

Lecture Notes in Informatics

Software Engineering 2016 P-252, 17-18 (2016).

Gesellschaft für Informatik, Bonn

Copyright © Gesellschaft für Informatik, Bonn


Just test what you cannot verify!

Mike Czech , Marie-Christine Jakobs and Heike Wehrheim


Software verification is an established method to ensure software safety. Nevertheless, verification still often fails, either because it consumes too much resources, e.g., time or memory, or the technique is not mature enough to verify the property. Often then discarding the partial verification, the validation process proceeds with techniques like testing. To enable standard testing to profit from previous, partial verification, we use a summary of the verification effort to simplify the program for subsequent testing. Our techniques use this summary to construct a residual program which only contains program paths with unproven assertions. Afterwards, the residual program can be used with standard testing tools. Our first experiments show that testing profits from the partial verification. The test effort is reduced and combined verification and testing is faster than a complete verification.

Full Text: PDF

Gesellschaft für Informatik, Bonn
ISBN 978-3-88579-646-6

Last changed 25.02.2016 18:38:57