Symbolic Liveness Analysis of Real-World Software

Authors: Daniel Schemmel, Julian Büning, Oscar Soria Dustmann, Thomas Noll and Klaus Wehrle

Paper Information

Title:Symbolic Liveness Analysis of Real-World Software
Authors:Daniel Schemmel, Julian Büning, Oscar Soria Dustmann, Thomas Noll and Klaus Wehrle
Proceedings:CAV All Papers
Editors: Georg Weissenbacher, Hana Chockler and Igor Konnov
Keywords:Symbolic Execution, Liveness Analysis, Software Testing, Non-Termination Bugs

ABSTRACT. Liveness violation bugs are notoriously hard to detect, especially due to the difficulty inherent in applying formal methods to real-world programs. We present a generic and practically useful liveness property which defines a program as being live as long as it will eventually either consume more input or terminate. We show that this property naturally maps to many different kinds of real-world programs. To demonstrate the usefulness of our liveness property, we also present an algorithm that can be efficiently implemented to dynamically find fixed points of the target program during Symbolic Execution. This extends Symbolic Execution, a well known dynamic testing technique, to find a new class of program defects, namely liveness violations, while only incurring a small runtime and memory overhead, as evidenced by our evaluation. The implementation of our method found a total of five previously undiscovered software defects in BusyBox and the GNU Coreutils. All five defects have been confirmed and fixed by the respective maintainers after shipping for years, most of them well over a decade.

Talk:Jul 17 16:30 (Session 122A: CPS, Hardware, Industrial Applications)