Pötzl, D. (2012). Achieving high coverage and finding bugs in sequential and concurrent software [Diploma Thesis, Technische Universität Wien]. reposiTUm. http://hdl.handle.net/20.500.12708/160601
Concolic Testing ist eine Methode zum automatisierten Testen von Software. Dabei werden konkrete und symbolische Programmausführung kombiniert. Wir haben einige Erweiterungen des Concolic Testing Tools CREST implementiert. Zum Beispiel wurden Anbindungen für die SMT Solver MathSAT, Yices und Z3 implementiert. Des Weiteren beschäftigt sich die Arbeit mit dem Lösen von bei der Programmausführung generierten Constraints. Ein zweiter Teil der Arbeit behandelt das Finden von Fehlern in nebenläufiger Software. Es wurde eine umfassende Zusammenstellung von Fehlermustern in nebenläufiger Software erstellt, und ein Überblick über vorhandene Tools zum Finden von Fehlern gegeben.
Concolic testing is an automated software testing method that combines concrete and symbolic execution to achieve high code coverage and expose bugs in the program under test. We implemented several extensions to the openly available concolic testing tool CREST, and evaluated several aspects of it on the programs replace, grep, sed and Vim. We further describe a procedure to effectively solve constraints during concolic testing by using the push and pop operations commonly provided by SMT solvers. We implemented the procedure in C for the SMT solvers Z3, MathSAT, Yices and STP. In an experimental evaluation on constraints generated by CREST during concolic execution on grep and Vim, the push-pop method outperformed all other methods we tried in most cases. In the second part of this thesis, we discuss the issue of exposing concurrency bugs. We survey several existing tools for finding such bugs, and describe 22 different concurrency bug patterns. Concurrency bug patterns are bug patterns that arise in the context of concurrent programming, and are typically obtained as abstractions of concrete bugs. The study of bug patterns can prevent programmers from making similar mistakes, and can provide guidance for developers of bug exposing techniques and designers of programming languages and APIs.
