Doctor of Philosophy / Department of Computing and Information Sciences / Matthew Dwyer / John M. Hatcliff / To analyze an open system, one needs to close it with a definition of its environment, i.e., its execution context. Environment modeling is a significant challenge: environment models should be general enough to permit analysis of large portions of a system's possible behaviors, yet sufficiently precise to enable cost-effective reasoning. This thesis presents the Bandera Environment Generator (BEG), a toolset that automates generation of environment models to provide a restricted form of modular model checking of Java programs, where the module's source code is the subject of analysis along with an abstract model of the environment's behavior. Since the most general environments do not allow for tractable model checking, BEG has support for restricting the environment behavior based on domain-specific knowledge and assumptions about the environment behavior, which can be acquired from a variety of sources. When the environment code is not available, developers can encode their assumptions as an explicit formal specification. When the environment code is available, BEG employs static analyses to extract environment assumptions. Both specifications and static analyses can be tuned to reflect domain-specific knowledge, i.e., to describe domain-specific aspects of the environment behavior. Initially, BEG was implemented to handle general Java applications; later, it was extended to handle two specific domains: Graphical User Interfaces (GUI) implemented using the Swing/AWT libraries and web applications implemented using the J2EE framework. BEG was evaluated on several non-trivial case studies, including industrial applications from NASA, SUN, and Fujitsu. This thesis presents the domain-specific environment generation for GUI and web applications and describes BEG, its extensible architecture, usage, and how it can be extended to handle new domains.

Model checking is a technique used to verify whether a model meets a given specification by exhaustively and automatically checking each reachable state in the model. It is a well-developed technique, but it suffers from some issues, perhaps most importantly the state space explosion problem. Models may contain so many states that must be checked means that the model checking procedure may be intractable. In this thesis we investigate whether procedure summaries can be used to improve the performance of model checking. Procedure summaries are concise representations of parts of a program, such as a function or method. We present a design and an implementation of dynamically generated summaries as an extension of Java PathFinder, a virtual machine executing Java bytecode that is able to model check programs written in Java by backtracking execution, to explore different schedulings etc. We find that our summaries incur an overhead that outweighs the benefits in most cases, but the approach shows promise in certain cases, in particular when stateless model checking is used. We also provide some statistics related to cases when our summaries are applicable that could provide guidance for future work within this field. / Model checking, eller modellkontroll, är en välkänd teknik inom programverifikation som används för att verifiera att en modell, ofta av ett program, uppfyller en given specifikation genom att undersöka alla nåbara tillstånd i modellen. Det är en välutvecklad teknik som lider av några brister, en av de viktigaste är det så kallade state space explosion-problemet. Modellerna kan bestå av så många olika tillstånd att \textit{model checking} inte går att använda. I den här rapporten undersöker vi om vi kan tillämpa så kallade procedur-sammanfattningar för att förbättra prestandan av model checking. Procedur-sammanfattningar är representationer av delar av program, till exempel metoder eller funktioner. Vi presenterar en design och implementation av dynamiskt genererade sammanfattningar i form av ett tillägg till Java PathFinder, en virtuell maskin som exekverar Java bytecode som kan utföra model checking genom att backa körningar för att till exempel utforska olika schemaläggningar. Våra procedur-sammanfattningar har i många fall en negativ effekt på körtid, men visar på lovande resultat i vissa fall, i synnerhet när så kallad stateless model checking används. Vi presenterar också resultat kopplat till fall när våra sammanfattningar är applicerbara som kan leda vägen för fortsatt arbete inom området.

The thesis presents xavier, a novel tool-set for model checking of concurrent x86-64 assembly programs, via Partial Order Reduction (POR). xavier{} presents a realistic platform for systematically exploring and analyzing the state-space of concurrent x86 assembly programs, with the aim of detecting bugs via assertion failures in mainstream programs. Recently, a number of state-of-the-art model checking solutions have been introduced to efficiently explore the state-space of concurrent programs, using POR algorithms. However, such solutions are inefficient while analyzing stateful programming languages, such as the x86 assembly language, due to their low level of abstraction. To this end, xavier{} makes two contributions: i) a novel order-sensitivity based POR algorithm, that is applicable to concurrent x86 assembly, ii) an x86 machine-model that can accurately perform relaxed-consistency emulation of concurrent x86 assembly, without the need for any translations. We demonstrate the applicability of xavier{} through an evaluation on several classical mutual-exclusion benchmarks and mainstream benchmarks from the Userspace Read-Copy-Update (URCU) concurrency library, where the benchmarks range from $250-3700$ lines of x86 assembly. The framework is the first that supports systematic model checking of concurrent x86 assembly programs, and the effectiveness of xavier{} is demonstrated by reproducing a concurrency issue of threads accessing intermediate states in the URCU library, which stems from an assumption violation. / Master of Science / Sound verification of multi-threaded programs necessitate a systematic analysis of program state-spaces that result from thread interactions. Consequently, model-checking cite{godefroid1997model, Clarke2018} has been one of the prominent methods used to tackle the verification of multi-threaded programs. However, existing model-checking solutions are inefficient while analyzing stateful programming languages, such as the x86 assembly language, due to the solutions' higher level of abstraction. Therefore, the thesis presents xavier, a novel tool-set and a realistic platform for systematically exploring and analyzing the state-space of mainstream concurrent x86 assembly programs, with the aim of detecting bugs via assertion failures. To this end, xavier{} makes two contributions: i) a novel order-sensitivity based Partial Order Reduction algorithm, which efficiently explores the state space of concurrent x86 assembly, ii) an x86 machine-model that can accurately emulate the execution of concurrent x86 assembly, without the need for any translations. We demonstrate the applicability of xavier{} through an evaluation on several classical mutual-exclusion and mainstream benchmarks from the Userspace Read-Copy-Update (URCU) concurrency library, where the benchmarks range from $250-3700$ lines of x86 assembly. Moreover, we demonstrate the effectiveness of xavier{} by reproducing a concurrency issue in the URCU library, which manifests as a result of an assumption violation.

State explosion in model checking continues to be the primary obstacle to widespread use of software model checking. The large input ranges of variables used in software is the main cause of state explosion. As software grows in size and complexity the problem only becomes worse. As such, model checking research into data abstraction as a way of mitigating state explosion has become more and more important. Data abstractions aim to reduce the effect of large input ranges. This work focuses on a static program analysis technique called dead variable analysis. The goal of dead variable analysis is to discover variable assignments that are not used. When applied to model checking, this allows us to ignore the entire input range of dead variables and thus reduce the size of the explored state space. Prior research into dead variable analysis for model checking does not make full use of dynamic run-time information that is present during model checking. We present an algorithm for intraprocedural dead variable analysis that uses dynamic run-time information to find more dead variables on-the-fly and further reduce the size of the explored state space. We introduce a definition for the maximal state space reduction possible through an on-the-fly dead variable analysis and then show that our algorithm produces a maximal reduction in the absence of non-determinism.