Continuous testing is widely used for facilitating fast and reliable software delivery. However, build-time configurability makes such testing harder for configurable software. As configurable software forms the basis of much of our computing infrastructure, there is even more need for better continuous testing for configurable software. In this dissertation, our goal is to improve the quality of configurable software. To this end, we tackle two, previously unsolved problems. The build system of configurable software is one of the biggest reasons why testing configurable software is hard. Therefore, in our solutions, we deal with the build system by using a comprehensive formal model of the build system. As the key insight of our dissertation, we hypothesize that comprehensive formal modeling of the build system can facilitate improving the quality of configurable software. We use our problems and solution approaches to provide evidence for our thesis. The first problem we tackle is finding unmet dependency bugs in a given configuration specifications in Kconfig language, which is used in the Linux kernel's build system. Unmet dependency bugs allow illegal configurations to pass through the build system, and can often cause broken builds, as much as 60% of the time. To address this problem, we created a verification-based bug finder, called kismet. kismet found hundreds of bugs and led to fixes committed into the Linux kernel's codebase. It was integrated into one of the most prolific continuous testing infrastructures for the Linux kernel. The second problem we look at is finding a small set of Kconfig configurations that build all lines of an input patch, while being close to the settings of an input configuration. Testing tools can only test changes from a patch when the changed code is built into the binary, which is not guaranteed with most configurations that developers use for testing. To this end, we created an algorithm, called krepair, that automatically updates Kconfig configurations with small changes to build code changes from a given patch, i.e., to cover patches, while keeping the specific benefits of configurations used for testing. krepair increased the patch coverage by up to 37 times for a variety of configurations used in testing the Linux kernel by incurring changes between 0.1% to 35.7% when compared to the original configurations. We expect our studies to provide a foundation for future development of studies in this direction.


If this is your thesis or dissertation, and want to learn how to access it or for more information about readership statistics, contact us at STARS@ucf.edu

Graduation Date





Gazzillo, Paul


Doctor of Philosophy (Ph.D.)


College of Engineering and Computer Science


Computer Science

Degree Program

Computer Science


CFE0009282; DP0026886





Release Date

August 2023

Length of Campus-only Access

1 year

Access Status

Doctoral Dissertation (Open Access)