Gesellschaft für Informatik e.V.

Lecture Notes in Informatics

Software Engineering 2016 P-252, 67-68 (2016).

Gesellschaft für Informatik, Bonn

Copyright © Gesellschaft für Informatik, Bonn


Empirical software metrics for benchmarking of verification tools

Yulia Demyanova , Thomas Pani , Helmut Veith and Florian Zuleger


In recent work [De15, PVZ15, DVZ13], we study empirical metrics for software (SW) source code, which can predict the performance of verification tools on specific types of SW. Our metrics comprise variable usage patterns, loop patterns, as well as indicators of control-flow complexity and are extracted by simple data-flow analyses. We demonstrate that our metrics are powerful enough to devise a machine-learning based portfolio solver for SW verification. We show that this portfolio solver would be the (hypothetical) overall winner of both the 2014 and 2015 International Competition on Software Verification (SV-COMP). This gives strong empirical evidence for the predictive power of our metrics and demonstrates the viability of portfolio solvers for SW verification.

Full Text: PDF

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

Last changed 25.02.2016 18:39:07