Software is everywhere, and going back to a life without software is unimaginable. Unfortunately, software does not always behave as expected, even though during the development cycle, software is usually tested to verify its correctness. To aid in testing, methods such as fuzzing or symbolic execution are used for automatic verification software systems. These methods are able to quickly find inputs to the systems that cover large portions of the code base. However, both of these methods struggle to find inputs that cover code which requires many iterations through loops. In symbolic execution, loops are a large contributing factor to the path explosion problem and therefore the overall runtime. For loops containing conditional branches, each iteration is a new decision point. This leads to an exponential number of possible paths through a loop in comparison to the number of iterations. In this work, we investigate the use of loops in symbolic execution to reach portions of the code which require numerous iterations through loops with conditional branches. We propose a novel technique for symbolic execution that uses the effects of one or more iterations through a loop to reach new parts of the code. By implementing this technique and applying it to a set of challenges designed to stress current tools and methods for software verification, we show that our technique is able to efficiently reach new parts of these challenges. These areas are not reached by state-of-the-art methods within the same time budget. Another method for verifying software behavior is active learning, where simple models are learned from a system. These models capture the behavior of the system at a high level, allowing easier analysis to verify the behavior of a system. During the automatic learning of these models, loops are not handled separately. This leads to models where the behavior of a system is not captured fully, leading to incomplete analysis. We propose new methods for finding changes in behavior after executing these loops numerous times. We have compared our techniques to existing methods and show that this produces more complete models of a system.

The M.O.R.S.E. system is a tool for creating and managing large escape events, mainly used for local escape events. The tool is designed for only a limited range of puzzle types and styling options because most of the puzzles require physical items in order to solve a puzzle and only the answers have to be entered in M.O.R.S.E. Because of this design, it is really difficult to create online escape experiences, especially rich and immersive ones. It also requires a lot of programming outside of the M.O.R.S.E. system to do so. Raccoon Serious Games , the client, does not have many employees with programming experience and, therefore, it is not feasible for them to create the rich and immersive online escape experiences they want. To be able to create such immersive experiences, we are extending M.O.R.S.E. with editable domains and web pages. Game designers can add domains and web pages to the existing event schedule and then puzzles can be created for web pages. Players can view one or multiple of these domains and for each domain, the active web page will be served. Web pages can be created and stored in the domains, but the actual contents of the web pages still have to be made. Because making web pages is often a programming intensive task, a page builder has been created in M.O.R.S.E. This page builder allows the user to load and save web pages created in the M.O.R.S.E. system. It uses a drag-and-drop system to place building-block elements inside the web pages and allows for directly visible styling of those elements. Because of this, the user does not need programming knowledge of the underlying implementation of the web pages. It also facilitates the linking between M.O.R.S.E. features and the domains such as puzzles and triggers for buttons. Using the import and export functionality, users can easily copy previous web pages created with the page builder. This is not only limited to internal web pages but can also be used to import external code from outside the page builder. With user-friendly features such as the ability to undo and redo changes, the page builder tries to make creating web pages as easy as possible. An important aspect of the escape games hosted by Raccoon Serious Games is team building. We extend upon this notion by adding roles and a leaderboard screen to M.O.R.S.E., both of which increase the need and opportunity for interaction between players. The addition of roles allows game designers to enforce cooperation in their escape events, by restricting the access to resources required for solving a puzzle to only a subset of the players in a team. This way they have to cooperate and combine their information and resources to solve all puzzles. The addition of leaderboards is also an extra incentive for a player in a team to work together efficiently because this will positively impact their score and, therefore, ranking on the leaderboard.